Tropical Resource Typing — Max-Plus Algebra for Worst-Case Bounds

A Lean 4 formalization and technical note applying max-plus (tropical) algebra to resource-aware type systems, yielding compositional worst-case bounds for latency, stack usage, and adversarial round-counts.

Contents

• Overview
• The twin formalizations
  • TropicalSessionTypes.lean
  • TropicalAdapterPath.lean
  • The connection
• What is standard and what is ours
• The resource-grade axis (Resource.*)
• Proof purity
• Known scope boundaries
• Build
• Repository Layout
• Documentation
• Companion repositories
• License
• Build

Overview

Conventional resource-aware type systems track resources additively (e.g., linear logic’s !A ⊗ B). The tropical / max-plus semiring replaces sum with max — so type-system operations naturally compose to the worst-case bound rather than a probabilistic or average-case figure.

The max-plus semiring is standard mathematics. What this repo contributes:

• Typing rules applying tropical algebra to speculative session types and adapter paths.

• A no-go theorem (hub_ceiling) refuting the universal-interoperability claim of Protocol Squisher.

• A reusable resource-grade axis (Resource.*) with a parametric transport theorem for downstream languages.

• A separation proof that resource algebras measure Echo residues but are not Echo instances.

• Dependency-free Lean 4 proofs — no Mathlib, no sorry, no Classical.choice.

The twin formalizations

Two Lean 4 proofs sit at the repository root, connected by an order-reversing involution:

TropicalSessionTypes.lean

The max-plus semiring (⊕ = max, ⊗ = +) grading speculative session types.

• Soundness: static grade equals dynamic wall-clock cost.

• QTT refinement (tropical_grade_le_sequentialTotal): max ≤ sum.

TropicalAdapterPath.lean

The min-max / bottleneck semiring (⊕ = min, ⊗ = max) grading adapter paths.

• hub_ceiling: the no-go corollary closing Protocol Squisher’s universal-interoperability claim.

The connection

The two are related by the involution g ↦ maxGrade − g, proved here as a lattice anti-isomorphism (De Morgan: exchanges min and max). It is explicitly not a semiring homomorphism — this is a structural fact about the duality, not a weakness.

What is standard and what is ours

Concept	Status	Home in this repo
Max-plus / min-max semirings	Standard (tropical geometry)	TropicalSessionTypes.lean, TropicalAdapterPath.lean
Dioid / idempotent semiring ordering	Standard	Resource.Algebra.*
De Morgan involution between max-plus and min-max	Standard (lattice theory)	Root proofs
Tropical grading of speculative session types	Novel application	TropicalSessionTypes.lean
hub_ceiling no-go theorem	Novel theorem (refutes Protocol Squisher)	TropicalAdapterPath.lean
Parametric transport theorem for resource laws	Novel mechanisation	Resource.Algebra.*
Proving tropical carriers are infinite (not {0,1,ω})	Novel separation proof	Resource.Stress
Echo is not a resource instance	Novel separation proof (matches echo-types)	Resource.EchoBridge

The resource-grade axis (Resource.*)

A reusable, consumer-facing Lean library for downstream languages. import Resource provides:

Resource.Algebra.*

The interface: ResourceSemiring (ops + laws) and ordered ResourceAlgebra (preorder + monotone ops), bundled with the canonical dioid-order builder and parametric_resource_transport over ConsumerLawBundle.

Resource.Instances.*

Concrete instances satisfying the one interface: Linear, Affine ({0,1,ω} usage, differing only in order), MaxPlus, MinPlus, MinMax.

Resource.Stress

Proves the tropical carriers are infinite — the stress test that the abstraction is not a finite {0,1,ω} reification.

Resource.EchoBridge

A resource algebra may measure Echo residues (direction E → R); Echo is not a resource instance. No echo-types dependency.

Vocabulary and contract are in FOUNDATION_CONTRACT.md; full detail in docs/RESOURCE-ALGEBRA.adoc.

Proof purity

Property	Status
Lean 4.13.0, lake build green	Yes
Depends only on Init	Yes (no Mathlib)
Every headline theorem depends only on propext + Quot.sound	Yes
sorry	None
Classical.choice	None

Full detail, build/verify recipe, theorem index, and provenance: docs/LEAN-FORMALIZATION.adoc.

Known scope boundaries

Caution

Research note, not production checker. The impl/ directory is a small reference implementation exercising the type-system rules from the note. It is intentionally not a production-ready type checker.

Caution

Worst-case only. The tropical semiring yields worst-case (max) bounds. It does not track average-case, probabilistic, or expected-cost figures. This is by design; a different algebraic structure is required for those.

Caution

EchoBridge is one-directional. Resource algebras measure Echo residues (E → R), but Echo is not a resource instance. The bridge does not import the echo-types library; it establishes the vocabulary boundary.

Build

# Lean formalization
lake build

# Reference implementation
cd impl/
just build
just test

# Render technical note
cd document/
asciidoctor -o /tmp/note.html main.adoc

Repository Layout

Path	Purpose
TropicalSessionTypes.lean	Max-plus grading of speculative session types
TropicalAdapterPath.lean	Min-max grading of adapter paths + hub_ceiling no-go
Resource/	Reusable resource-grade axis (Algebra, Instances, Stress, EchoBridge)
document/	Technical note (AsciiDoc source)
impl/	Reference implementation of type-system rules
docs/	Supplementary material, Lean formalization detail, resource algebra docs
audits/	Estate-wide review logs (Hypatia scan, governance checks)

Documentation

• EXPLAINME — claim-by-claim receipts and known gaps

• Lean formalization detail — theorem index, build recipe, provenance

• Resource algebra detail — contract, vocabulary, instances

• Foundation contract — stable API for downstream languages

• Glossary — terminology reference

Companion repositories

• echo-types — sibling formal-foundations work in Agda

• typed-wasm — target where resource-typing rules may be deployed

• standards — canonical estate standards

License

SPDX-License-Identifier: MPL-2.0 — see LICENSE.====

Build

# Lean formalization
lake build

# Reference implementation
cd impl/
just build