From 5378eec141fa8fad8ab1f7e2a786c9b738f866b8 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 11 Jun 2026 22:39:40 +0100
Subject: [PATCH 1/2] feat(lean): migrate + repair tropical proofs; unify
 min-max/max-plus duality
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Bring the min-max transport semiring (TropicalAdapterPath) in beside its
max-plus twin (TropicalSessionTypes) and make both compile clean under a
pinned Lean 4.13.0 toolchain via Lake. The min-max file's source is the
frozen provenance archive in protocol-squisher; that copy is left untouched.

Both files previously did NOT compile on any installed toolchain (the headers'
"Verified" claims were never true — corroborating protocol-squisher's
PROVENANCE.adoc finding). Repairs:

TropicalSessionTypes.lean (max-plus twin):
- import ordering (module doc must follow `import`)
- max-distributivity helpers: Nat.max_def + split + omega (was a looping simp)
- local `One` class + OfNat shim (Lean 4.13.0 core has Zero but not One)
- spec_par QTT-refinement case: split on Nat.max before omega
- header version claim corrected to 4.13.0

TropicalAdapterPath.lean (min-max twin):
- import ordering; dangling doc-comment fixed
- push_neg (Mathlib-only) -> core Nat.max_def + split + omega
- AdapterPath def -> abbrev (so List ++/foldl/membership lemmas apply)
- pathCost_append reproved via a uniform pathCost_cons lemma
- pathCost_le_sequential reproved (removed non-existent Nat.max_le_add)
- corrected a FALSE theorem: dual_tcMul_bounded claimed
  dual(max m n) = dual m + dual n - maxGrade, false at m=1,n=2 (1 vs 0).
  Replaced with the true De Morgan dual dual_tcMul_is_min:
  dual(max m n) = min(dual m, dual n), completing the duality pair.

Build/config:
- lean-toolchain pinned to leanprover/lean4:v4.13.0
- lakefile.lean (lean_lib over both roots) + lake-manifest.json
- .gitignore for Lake/Julia/Isabelle artefacts

Axiom audit: all headline theorems depend only on propext (+ Quot.sound);
no sorryAx, no Classical.choice. `lake build` is green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 .gitignore                |  19 ++
 TropicalAdapterPath.lean  | 427 ++++++++++++++++++++++++++++++++++++++
 TropicalSessionTypes.lean |  27 ++-
 lake-manifest.json        |   5 +
 lakefile.lean             |  16 ++
 lean-toolchain            |   1 +
 6 files changed, 486 insertions(+), 9 deletions(-)
 create mode 100644 .gitignore
 create mode 100644 TropicalAdapterPath.lean
 create mode 100644 lake-manifest.json
 create mode 100644 lakefile.lean
 create mode 100644 lean-toolchain

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..ccef718
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,19 @@
+# Lean / Lake build artefacts
+/.lake/
+/build/
+/lake-packages/
+*.olean
+*.ilean
+*.trace
+
+# Julia
+/Manifest-generated.toml
+
+# Isabelle
+*.thy~
+/output/
+/heaps/
+
+# Editor / OS
+*.swp
+.DS_Store
diff --git a/TropicalAdapterPath.lean b/TropicalAdapterPath.lean
new file mode 100644
index 0000000..df1dc89
--- /dev/null
+++ b/TropicalAdapterPath.lean
@@ -0,0 +1,427 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+import Init
+
+/-!
+  # Transport Semilattice — Tropical Connection (v1.0)
+
+  Author: Jonathan D.A. Jewell (hyperpolymath)
+  Date:   2026-04-11
+
+  ## The claim being formalised
+
+  Protocol Squisher's 4-class transport semilattice
+  (Concorde / Business / Economy / Wheelbarrow) is formally a **tropical
+  optimisation problem**: adapter path search is Dijkstra over a tropical
+  (idempotent) semiring.
+
+  This file makes that claim precise.
+
+  ## Structure of this file
+
+  1. `TransportGrade` — an Nat embedding for the 4 classes (0=best)
+  2. `TransportSemilattice` — the join semilattice (max=worst of two classes)
+  3. `PathCost` — the grade of a composed adapter path (bottleneck = max of steps)
+  4. The **path optimisation semiring**: ⊕ = min, ⊗ = max
+     This is the "min-max" or "bottleneck" semiring — a tropical semiring
+     dual to the max-plus semiring used in `TropicalSessionTypes.lean`.
+  5. `semiring_laws_*` — the 8 semiring axioms verified for this structure
+  6. `OptimalPath` — the minimax path theorem: optimal = min over paths of max(grades)
+  7. `TropicalDuality` — the relationship between min-max and max-plus tropical semirings
+
+  ## Relationship to TropicalSessionTypes.lean
+
+  `TropicalSessionTypes.lean` (in `tropical-resource-typing`) proves a
+  max-plus CommSemiring instance where ⊕=max and ⊗=+.  The transport path
+  semiring here has ⊕=min and ⊗=max.  Both are **dioids** (semirings with
+  idempotent addition):
+  - max-plus:  max is idempotent (max(n,n)=n)
+  - min-max:   min is idempotent (min(n,n)=n)
+
+  The formal duality: grade_path(P) in the min-max semiring corresponds to
+  the grade_session(S) QTT refinement in the max-plus semiring via the map
+  g ↦ (maxGrade − g), which is an order-reversing isomorphism on the
+  bounded lattice [0, maxGrade].
+
+  ## Open items (no sorry here — these are documented future work)
+
+  1. ~~Prove the Dijkstra correctness theorem for min-max semirings~~ **DONE**:
+     `foldl_tcAdd_le_init` + `foldl_tcAdd_le_mem` + `minimax_path_optimal`
+     prove the optimal-path property for the foldl-min formulation.
+     Full graph-algorithmic Dijkstra correctness (generalised to arbitrary graphs)
+     remains future work; the classical result is Mohri 2002.
+  2. Formalise the order-reversing isomorphism explicitly as a semiring
+     homomorphism (not just stated in comments).
+  3. Connect to `TropicalSessionTypes.lean` CommSemiring instance directly
+     by constructing a functor between the two structures in Lean.
+-/
+
+namespace Hyperpolymath.ProtocolSquisher.Tropical
+
+-- ============================================================================
+-- 1.  Transport classes and their grade embedding
+-- ============================================================================
+
+/-- The 4-class transport quality ordering.
+    Concorde = perfect fidelity; Wheelbarrow = significant loss. -/
+inductive TransportClass where
+  | Concorde    -- perfect: lossless, zero overhead
+  | Business    -- good: near-lossless, minor overhead
+  | Economy     -- lossy: schema-level adaptation required
+  | Wheelbarrow -- fallback: JSON, maximum loss
+  deriving DecidableEq, Repr
+
+/-- Natural number grade: 0 = best (Concorde), 3 = worst (Wheelbarrow).
+    Lower grade = higher fidelity. -/
+def grade : TransportClass → Nat
+  | .Concorde    => 0
+  | .Business    => 1
+  | .Economy     => 2
+  | .Wheelbarrow => 3
+
+/-- The maximum possible grade (used for the duality isomorphism). -/
+def maxGrade : Nat := 3
+
+/-- `grade` is injective — distinct classes have distinct grades. -/
+theorem grade_injective : ∀ c1 c2, grade c1 = grade c2 → c1 = c2 := by
+  intro c1 c2 h
+  cases c1 <;> cases c2 <;> simp [grade] at h ⊢ <;> exact h
+
+/-- The class ordering is total: any two classes are comparable. -/
+theorem grade_total : ∀ c1 c2, grade c1 ≤ grade c2 ∨ grade c2 ≤ grade c1 := by
+  intro c1 c2
+  exact Nat.le_or_le (grade c1) (grade c2)
+
+-- ============================================================================
+-- 2.  The transport semilattice (worst-of-two)
+-- ============================================================================
+
+/-- The join of two transport classes: the worse of the two.
+    "If I need to go through two adapters, the quality is the worse one." -/
+def tcJoin (c1 c2 : TransportClass) : TransportClass :=
+  if grade c1 ≥ grade c2 then c1 else c2
+
+/-- `tcJoin` corresponds to `Nat.max` on grades. -/
+theorem tcJoin_grade (c1 c2 : TransportClass) :
+    grade (tcJoin c1 c2) = Nat.max (grade c1) (grade c2) := by
+  unfold tcJoin
+  -- `push_neg` is Mathlib-only; `Nat.max_def` + `split` + `omega` is core-clean.
+  split <;> simp only [Nat.max_def] <;> split <;> omega
+
+/-- Join is commutative. -/
+theorem tcJoin_comm (c1 c2 : TransportClass) : tcJoin c1 c2 = tcJoin c2 c1 := by
+  apply grade_injective
+  simp [tcJoin_grade, Nat.max_comm]
+
+/-- Join is associative. -/
+theorem tcJoin_assoc (c1 c2 c3 : TransportClass) :
+    tcJoin (tcJoin c1 c2) c3 = tcJoin c1 (tcJoin c2 c3) := by
+  apply grade_injective
+  simp [tcJoin_grade, Nat.max_assoc]
+
+/-- Join is idempotent: a class composed with itself is unchanged. -/
+theorem tcJoin_idem (c : TransportClass) : tcJoin c c = c := by
+  apply grade_injective
+  simp [tcJoin_grade, Nat.max_self]
+
+/-- Concorde is the identity of join (best quality is neutral). -/
+theorem tcJoin_concorde_left (c : TransportClass) : tcJoin .Concorde c = c := by
+  apply grade_injective
+  rw [tcJoin_grade]
+  simp only [grade, Nat.max_def]
+  split <;> omega
+
+theorem tcJoin_concorde_right (c : TransportClass) : tcJoin c .Concorde = c := by
+  rw [tcJoin_comm]; exact tcJoin_concorde_left c
+
+-- ============================================================================
+-- 3.  Adapter path cost
+-- ============================================================================
+
+/-- An adapter path is a list of transport classes (one per adapter step).
+    `abbrev` (not `def`) so `List` operations (`++`, `foldl`, membership) and
+    their lemmas apply through the alias without manual unfolding. -/
+abbrev AdapterPath := List TransportClass
+
+/-- The cost of a path is the worst step grade (bottleneck quality). -/
+def pathCost : AdapterPath → Nat
+  | []      => 0                             -- empty path: free / Concorde
+  | [c]     => grade c
+  | c :: cs => Nat.max (grade c) (pathCost cs)
+
+/-- A single-step path has the grade of that step. -/
+@[simp]
+theorem pathCost_single (c : TransportClass) : pathCost [c] = grade c := rfl
+
+/-- Uniform cons rule: the cost of `c :: cs` is `max (grade c) (pathCost cs)`.
+    Subsumes the `[c]` special case via `max (grade c) 0 = grade c`. -/
+theorem pathCost_cons (c : TransportClass) (cs : AdapterPath) :
+    pathCost (c :: cs) = Nat.max (grade c) (pathCost cs) := by
+  cases cs with
+  | nil => simp only [pathCost, Nat.max_def]; split <;> omega
+  | cons c2 rest => rfl
+
+/-- Path cost is monotone: extending a path can only make it worse or equal. -/
+theorem pathCost_mono (c : TransportClass) (path : AdapterPath) :
+    pathCost path ≤ pathCost (c :: path) := by
+  cases path with
+  | nil  => simp [pathCost]
+  | cons c2 rest => simp [pathCost, Nat.le_max_right]
+
+/-- Concatenating two paths: cost = max of the two costs. -/
+theorem pathCost_append (p1 p2 : AdapterPath) :
+    pathCost (p1 ++ p2) = Nat.max (pathCost p1) (pathCost p2) := by
+  induction p1 with
+  | nil => simp [pathCost, Nat.zero_max]
+  | cons c rest ih =>
+      rw [List.cons_append, pathCost_cons, ih, pathCost_cons]
+      exact (Nat.max_assoc _ _ _).symm
+
+-- ============================================================================
+-- 4.  The path-optimisation semiring (min-max tropical semiring)
+-- ============================================================================
+--
+-- To find the *optimal* adapter path between two schemas:
+--   - "Adding" two paths means choosing the better one: ⊕ = min
+--   - "Multiplying" (composing) two paths means taking the bottleneck: ⊗ = max
+--
+-- This (Nat, min, max, ∞, 0) is a semiring called the "min-max semiring"
+-- or "bottleneck semiring".  It is an idempotent semiring (dioid) because
+-- min(n, n) = n.
+--
+-- In the tropical literature this is the dual of the (Nat, max, +) max-plus
+-- semiring: substituting n ↦ (K − n) for a bound K converts one to the other.
+
+/-- Additive operation: choose the better (lower-cost) path. -/
+def tcAdd (m n : Nat) : Nat := Nat.min m n
+
+/-- Multiplicative operation: compose paths — bottleneck cost. -/
+def tcMul (m n : Nat) : Nat := Nat.max m n
+
+/-- Additive identity: ⊤ (infinity — a path that costs everything is neutral
+    for "choose the better one": min(∞, n) = n). -/
+def tcZero : Nat := 1000000  -- ∞ represented as a large bound; see note below
+-- Note: a cleaner treatment would use `WithTop Nat` or a custom type.
+-- Using a concrete bound here keeps the proof accessible without Mathlib.
+-- The bound 1_000_000 is safe: all actual grades are in {0,1,2,3}.
+
+/-- Multiplicative identity: 0 (Concorde grade — neutral for bottleneck: max(0,n)=n). -/
+def tcOne : Nat := 0
+
+-- ─── Semiring axioms ────────────────────────────────────────────────────────
+
+theorem tcAdd_comm (m n : Nat) : tcAdd m n = tcAdd n m := Nat.min_comm m n
+
+theorem tcAdd_assoc (m n p : Nat) : tcAdd (tcAdd m n) p = tcAdd m (tcAdd n p) :=
+  Nat.min_assoc m n p
+
+theorem tcAdd_zero_left (n : Nat) (h : n ≤ tcZero) : tcAdd tcZero n = n := by
+  unfold tcAdd tcZero
+  exact Nat.min_eq_right h
+
+/-- Grades are in {0,1,2,3} ≤ tcZero, so tcZero is a true additive identity
+    for all realistic path costs. -/
+theorem grade_le_tcZero (c : TransportClass) : grade c ≤ tcZero := by
+  cases c <;> simp [grade, tcZero]
+
+theorem pathCost_le_tcZero (path : AdapterPath) : pathCost path ≤ tcZero := by
+  induction path with
+  | nil       => simp [pathCost, tcZero]
+  | cons c cs ih =>
+    cases cs with
+    | nil  => exact grade_le_tcZero c
+    | cons c2 rest =>
+        simp [pathCost]
+        exact Nat.max_le.mpr ⟨grade_le_tcZero c, ih⟩
+
+theorem tcMul_comm (m n : Nat) : tcMul m n = tcMul n m := Nat.max_comm m n
+
+theorem tcMul_assoc (m n p : Nat) : tcMul (tcMul m n) p = tcMul m (tcMul n p) :=
+  Nat.max_assoc m n p
+
+/-- tcOne (0) is the multiplicative identity: max(0, n) = n. -/
+theorem tcMul_one_left (n : Nat) : tcMul tcOne n = n := by
+  simp [tcMul, tcOne]
+
+theorem tcMul_one_right (n : Nat) : tcMul n tcOne = n := by
+  simp [tcMul, tcOne]
+
+/-- Distributivity: min(max(a,b), max(a,c)) = max(a, min(b,c)). -/
+theorem tcMul_add_distrib_left (a b c : Nat) :
+    tcMul a (tcAdd b c) = tcAdd (tcMul a b) (tcMul a c) := by
+  simp [tcMul, tcAdd, Nat.max_min_distrib_left]
+
+/-- Idempotency of tcAdd: min(n, n) = n.
+    This is what makes the semiring "tropical" / a dioid. -/
+theorem tcAdd_idem (n : Nat) : tcAdd n n = n := Nat.min_self n
+
+-- ============================================================================
+-- 5.  Optimal path theorem
+-- ============================================================================
+
+-- The set of all paths between two nodes (modelled as a list of paths).
+-- In a real implementation this would be a graph algorithm; here we state
+-- the property that the optimal path is defined by the minimax principle.
+
+/-- A path P is optimal (in the bottleneck sense) if no alternative path has
+    a strictly lower cost. -/
+def IsOptimalPath (P : AdapterPath) (alternatives : List AdapterPath) : Prop :=
+  ∀ Q ∈ alternatives, pathCost P ≤ pathCost Q
+
+/-- If two paths P and Q have costs n and m respectively, and we "add" them
+    (choose the better), the result has cost min(n, m). -/
+theorem best_of_two (P Q : AdapterPath) :
+    tcAdd (pathCost P) (pathCost Q) =
+    Nat.min (pathCost P) (pathCost Q) := rfl
+
+-- ─── Helper lemmas for foldl min ────────────────────────────────────────────
+
+/-- The result of foldl tcAdd is always ≤ the initial accumulator.
+    Induction: each step replaces acc with (min acc (pathCost Q)) ≤ acc. -/
+private theorem foldl_tcAdd_le_init :
+    ∀ (acc : Nat) (xs : List AdapterPath),
+    xs.foldl (fun a Q => tcAdd a (pathCost Q)) acc ≤ acc
+  | _,   []         => Nat.le_refl _
+  | acc, Q :: rest  =>
+      -- foldl on (Q::rest) = foldl on rest with new acc = tcAdd acc (pathCost Q)
+      -- IH: foldl_on_rest ≤ tcAdd acc (pathCost Q)
+      -- And: tcAdd acc (pathCost Q) = min acc _ ≤ acc
+      Nat.le_trans
+        (foldl_tcAdd_le_init (tcAdd acc (pathCost Q)) rest)
+        (Nat.min_le_left acc (pathCost Q))
+
+/-- The result of foldl tcAdd is ≤ the pathCost of every list member.
+    This is the core lemma: foldl min gives the global minimum. -/
+private theorem foldl_tcAdd_le_mem :
+    ∀ (acc : Nat) (xs : List AdapterPath) (Q : AdapterPath),
+    Q ∈ xs → xs.foldl (fun a R => tcAdd a (pathCost R)) acc ≤ pathCost Q
+  | _,   [],          _, hQ  => absurd hQ (List.not_mem_nil _)
+  | acc, R :: rest,   Q, hQ  =>
+      match List.mem_cons.mp hQ with
+      | Or.inl h =>
+          -- Q is the head R.  Cost = foldl on rest with acc' = tcAdd acc (pathCost R).
+          -- foldl_tcAdd_le_init: foldl_on_rest ≤ tcAdd acc (pathCost R)
+          -- And: tcAdd acc (pathCost R) = min acc (pathCost R) ≤ pathCost R = pathCost Q
+          h ▸ Nat.le_trans
+                (foldl_tcAdd_le_init (tcAdd acc (pathCost Q)) rest)
+                (Nat.min_le_right acc (pathCost Q))
+      | Or.inr h =>
+          -- Q is in the tail.  Apply IH with updated accumulator.
+          foldl_tcAdd_le_mem (tcAdd acc (pathCost R)) rest Q h
+
+/-- The path whose cost equals the foldl-min over all alternatives is optimal.
+    Proof: substitute h, then apply foldl_tcAdd_le_mem directly. -/
+theorem minimax_path_optimal
+    (P : AdapterPath) (alts : List AdapterPath)
+    (h : pathCost P = alts.foldl (fun acc Q => tcAdd acc (pathCost Q)) tcZero) :
+    IsOptimalPath P alts := by
+  intro Q hQ
+  rw [h]
+  exact foldl_tcAdd_le_mem tcZero alts Q hQ
+
+-- ============================================================================
+-- 6.  Tropical duality: connecting to TropicalSessionTypes
+-- ============================================================================
+
+/-- The dual of a grade: maps 0 ↦ 3, 1 ↦ 2, 2 ↦ 1, 3 ↦ 0.
+    This is the order-reversing involution on [0, maxGrade]. -/
+def dualGrade (n : Nat) : Nat := maxGrade - Nat.min n maxGrade
+
+/-- dualGrade is an involution: dual(dual(n)) = n for n ≤ maxGrade. -/
+theorem dualGrade_invol (n : Nat) (h : n ≤ maxGrade) : dualGrade (dualGrade n) = n := by
+  simp only [dualGrade, maxGrade, Nat.min_def] at h ⊢
+  repeat' split
+  all_goals omega
+
+/-- `dualGrade` is an order-reversing **lattice anti-isomorphism** on `[0, maxGrade]`.
+    It therefore exchanges the two idempotent operations by De Morgan:
+
+    * `dual (min a b) = max (dual a) (dual b)`   (`dual_tcAdd_is_max`)
+    * `dual (max a b) = min (dual a) (dual b)`   (`dual_tcMul_is_min`)
+
+    This is the precise, *provable* connection between the min-max transport
+    semiring here (⊕=min, ⊗=max) and the max-plus semiring in
+    `TropicalSessionTypes.lean` (⊕=max, ⊗=+).
+
+    It is NOT a semiring homomorphism from (min,max) to (max,+).  The previous
+    `dual_tcMul_bounded` claimed `dual (max m n) = dual m + dual n - maxGrade`,
+    which is **false**: for `m = 1, n = 2` the LHS is `dual 2 = 1` but the RHS is
+    `2 + 1 - 3 = 0`.  That stub is replaced by the correct min/max De Morgan dual
+    below. -/
+theorem dual_tcAdd_is_max (m n : Nat) (hm : m ≤ maxGrade) (hn : n ≤ maxGrade) :
+    dualGrade (tcAdd m n) = Nat.max (dualGrade m) (dualGrade n) := by
+  simp only [dualGrade, tcAdd, maxGrade, Nat.min_def, Nat.max_def] at hm hn ⊢
+  repeat' split
+  all_goals omega
+
+/-- De Morgan dual of `dual_tcAdd_is_max`: the dual sends the bottleneck (`max`)
+    of the min-max semiring to the `min` of the duals.  This is the corrected,
+    true replacement for the former (false) `dual_tcMul_bounded`. -/
+theorem dual_tcMul_is_min (m n : Nat) (hm : m ≤ maxGrade) (hn : n ≤ maxGrade) :
+    dualGrade (tcMul m n) = Nat.min (dualGrade m) (dualGrade n) := by
+  simp only [dualGrade, tcMul, maxGrade, Nat.min_def, Nat.max_def] at hm hn ⊢
+  repeat' split
+  all_goals omega
+
+/-- `foldl (· + grade ·)` shifts its accumulator: starting from `k` adds `k` to
+    the result of starting from `0`.  Lets the bound below reduce to the `0` case. -/
+private theorem foldl_add_grade (path : AdapterPath) (k : Nat) :
+    path.foldl (fun acc c => acc + grade c) k
+      = k + path.foldl (fun acc c => acc + grade c) 0 := by
+  induction path generalizing k with
+  | nil => simp
+  | cons c cs ih =>
+      simp only [List.foldl_cons]
+      rw [ih (k + grade c), ih (0 + grade c)]
+      omega
+
+/-- Analogue of `tropical_grade_le_sequentialTotal` from TropicalSessionTypes:
+    the bottleneck cost of a path is always ≤ the naive sequential total (sum of grades).
+    This justifies why minimax optimisation strictly improves over sequential cost. -/
+theorem pathCost_le_sequential (path : AdapterPath) :
+    pathCost path ≤ path.foldl (fun acc c => acc + grade c) 0 := by
+  induction path with
+  | nil => simp [pathCost]
+  | cons c cs ih =>
+      rw [pathCost_cons]
+      simp only [List.foldl_cons, Nat.zero_add]
+      rw [foldl_add_grade cs (grade c)]
+      simp only [Nat.max_def]
+      split <;> omega
+
+-- ============================================================================
+-- 7.  Hub ceiling — the no-go corollary
+-- ============================================================================
+
+/-- **Hub ceiling** — corollary of `pathCost_mono`.
+
+    Any adapter path that routes through an edge `e` (a transport step of
+    grade `g = grade e`) has `pathCost` at least `g`.  The bottleneck of a
+    whole path is floored by every individual step it contains.
+
+    Read as a no-go result for universal, high-fidelity interoperability:
+    if every conversion is forced through a single common hub, and the hub's
+    best embedding of some format is graded `g`, then no path through that
+    hub can carry that format at fidelity better than `g`.  One hub therefore
+    caps the fidelity of every format that must pass through it.  "Universal"
+    (one hub serving all formats) and "high fidelity" (grade 0 for all
+    formats) are contradictory the moment any format embeds into the hub at
+    grade > 0.  Universal *low* fidelity is the achievable point — that is
+    what JSON already is.
+
+    This corollary was never stated during the v1.x development.  It closes
+    Protocol Squisher's universal-interoperability claim using the project's
+    own algebra: transport-class composition is `max` (the bottleneck), and
+    `max` over a path can only be raised, never lowered, by the steps in it. -/
+theorem hub_ceiling (e : TransportClass) (path : List TransportClass)
+    (h : e ∈ path) : grade e ≤ pathCost path := by
+  induction path with
+  | nil => exact absurd h (List.not_mem_nil e)
+  | cons c cs ih =>
+    rcases List.mem_cons.mp h with rfl | h'
+    · cases cs with
+      | nil          => simp [pathCost]
+      | cons c2 rest => simp [pathCost, Nat.le_max_left]
+    · exact Nat.le_trans (ih h') (pathCost_mono c cs)
+
+end Hyperpolymath.ProtocolSquisher.Tropical
diff --git a/TropicalSessionTypes.lean b/TropicalSessionTypes.lean
index cac6545..0fcac24 100644
--- a/TropicalSessionTypes.lean
+++ b/TropicalSessionTypes.lean
@@ -1,10 +1,12 @@
 -- SPDX-License-Identifier: MPL-2.0
+import Init
+
 /-!
   # Tropical Session Types — v6.0
 
   Author: Jonathan D.A. Jewell (hyperpolymath)
   Date:   2026-04-11
-  Verified: Lean 4.29.0, `import Init` (no Mathlib dependency)
+  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), `import Init` (no Mathlib dependency)
 
   ## The unsolved problem
 
@@ -72,8 +74,6 @@
     addition; a machine-checked type checker backed by `floyd_warshall`.
 -/
 
-import Init
-
 namespace Hyperpolymath.Tropical
 
 -- ============================================================================
@@ -155,11 +155,11 @@ theorem mul_bot (a : Tropical) : tMul a .bot = .bot := by
 
 private theorem nat_mul_add_max_left (k m n : Nat) :
     k + Nat.max m n = Nat.max (k + m) (k + n) := by
-  simp [Nat.max_def]; omega
+  simp only [Nat.max_def]; split <;> split <;> omega
 
 private theorem nat_mul_add_max_right (k m n : Nat) :
     Nat.max m n + k = Nat.max (m + k) (n + k) := by
-  simp [Nat.max_def]; omega
+  simp only [Nat.max_def]; split <;> split <;> omega
 
 -- ---- Distributivity ---------------------------------------------------------
 
@@ -179,6 +179,15 @@ theorem right_distrib_trop (a b c : Tropical) :
 -- 4. CommSemiring Typeclass (local definition, Mathlib-compatible interface)
 -- ============================================================================
 
+/-- Lean 4.13.0 core provides `Zero` but not `One` (the latter landed in a
+    later toolchain).  We supply a minimal local `One` plus its `OfNat` bridge
+    so the Mathlib-compatible interface and `1` notation work under the pinned
+    toolchain without any Mathlib dependency. -/
+class One (α : Type) where
+  one : α
+
+instance [One α] : OfNat α (nat_lit 1) := ⟨One.one⟩
+
 /-- A commutative semiring.
     Defined locally (no Mathlib dependency) with a Mathlib-compatible interface.
     Wiring `Tropical` here enables `ring`-style proofs once Mathlib is added. -/
@@ -229,8 +238,8 @@ instance : CommSemiring Tropical where
 
 example : (0 : Tropical) = .bot            := rfl
 example : (1 : Tropical) = .val 0          := rfl
-example : (.val 2 + .val 5 : Tropical) = .val 5 := by simp [HAdd.hAdd, Add.add, tAdd]
-example : (.val 2 * .val 5 : Tropical) = .val 7 := by simp [HMul.hMul, Mul.mul, tMul]
+example : (.val 2 + .val 5 : Tropical) = .val 5 := by decide
+example : (.val 2 * .val 5 : Tropical) = .val 7 := by decide
 
 -- ============================================================================
 -- 6. Session Types
@@ -328,7 +337,7 @@ theorem tropical_grade_le_sequentialTotal (s : Session) :
   | send s ih             => simp [Span, sequentialTotal]; omega
   | recv s ih             => simp [Span, sequentialTotal]; exact ih
   | spec_par s1 s2 ih1 ih2 =>
-      simp [Span, sequentialTotal]
-      omega
+      simp only [Span, sequentialTotal, Nat.max_def]
+      split <;> omega
 
 end Hyperpolymath.Tropical
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..24f7c67
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "«tropical-resource-typing»",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..05c2544
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,16 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+
+import Lake
+open Lake DSL
+
+/-- Pure core Lean 4 proofs (no Mathlib dependency).
+    Toolchain is pinned to `leanprover/lean4:v4.13.0` in `lean-toolchain`. -/
+package «tropical-resource-typing» where
+
+@[default_target]
+lean_lib Tropical where
+  srcDir := "."
+  -- The two order-reversing twins: max-plus session grading and the
+  -- min-max (bottleneck) transport semiring.
+  roots := #[`TropicalSessionTypes, `TropicalAdapterPath]
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..4f86f95
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.13.0

From a2267b53c74563df52215bba5ee315bf710f9267 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 11 Jun 2026 22:50:13 +0100
Subject: [PATCH 2/2] docs(lean): authoritative Lean docs, README/CHANGELOG,
 machine-readable + CI
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- docs/LEAN-FORMALIZATION.adoc: authoritative reference for both twins — the
  min-max/max-plus duality, build/verify recipe, theorem index, axiom audit,
  and provenance.
- README.adoc: add a "Lean 4 formalization" section.
- docs/FORMAL-PROOFS.adoc: flag that its Lean code listings predate the v6.0
  source (illustrative API) and point to the authoritative doc.
- CHANGELOG.md: record the migration, the duality bridge, the false-lemma
  correction, the docs, and the CI.
- .machine_readable/6a2/ECOSYSTEM.a2ml: add TropicalAdapterPath, lakefile,
  lean-toolchain and the new doc as artefacts; bump 0.2.1 -> 0.2.2.
- .github/workflows/lean.yml: lake build + axiom audit (fails on
  sorry/Classical.choice) on push/PR.

Adds the owner's canonical SPDX-FileCopyrightText attribution to README.adoc and
CHANGELOG.md to satisfy the strict pre-commit owner-string gate (attribution
only; no SPDX-License-Identifier touched).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 .github/workflows/lean.yml           |  60 +++++++++
 .machine_readable/6a2/ECOSYSTEM.a2ml |  12 +-
 CHANGELOG.md                         |   9 +-
 README.adoc                          |  31 +++++
 docs/FORMAL-PROOFS.adoc              |  12 ++
 docs/LEAN-FORMALIZATION.adoc         | 190 +++++++++++++++++++++++++++
 6 files changed, 309 insertions(+), 5 deletions(-)
 create mode 100644 .github/workflows/lean.yml
 create mode 100644 docs/LEAN-FORMALIZATION.adoc

diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
new file mode 100644
index 0000000..a452896
--- /dev/null
+++ b/.github/workflows/lean.yml
@@ -0,0 +1,60 @@
+# SPDX-License-Identifier: MPL-2.0
+# lean.yml — build the Lean 4 tropical proofs and audit their axioms.
+#
+# Load-bearing build workflow (kept standalone in-repo, not in the shared
+# governance bundle): `lake build` over both order-reversing twins, then a
+# `#print axioms` audit asserting no `sorry`/`Classical.choice` crept in.
+# Toolchain is pinned by ./lean-toolchain (leanprover/lean4:v4.13.0); no Mathlib.
+
+name: Lean
+
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  lake-build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install elan (Lean toolchain manager)
+        run: |
+          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o elan-init.sh
+          sh elan-init.sh -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Show toolchain (pinned via lean-toolchain)
+        run: lean --version
+
+      - name: lake build
+        run: lake build
+
+      - name: Axiom audit — no sorry; propext/Quot.sound only
+        run: |
+          cat > /tmp/axcheck.lean <<'EOF'
+          import TropicalSessionTypes
+          import TropicalAdapterPath
+          #print axioms Hyperpolymath.Tropical.soundness
+          #print axioms Hyperpolymath.Tropical.tropical_grade_le_sequentialTotal
+          #print axioms Hyperpolymath.ProtocolSquisher.Tropical.pathCost_mono
+          #print axioms Hyperpolymath.ProtocolSquisher.Tropical.hub_ceiling
+          #print axioms Hyperpolymath.ProtocolSquisher.Tropical.dualGrade_invol
+          #print axioms Hyperpolymath.ProtocolSquisher.Tropical.dual_tcAdd_is_max
+          #print axioms Hyperpolymath.ProtocolSquisher.Tropical.dual_tcMul_is_min
+          EOF
+          out="$(lake env lean /tmp/axcheck.lean 2>&1)"
+          echo "$out"
+          if echo "$out" | grep -qiE 'sorry|Classical\.choice'; then
+            echo "::error::axiom audit failed — sorry or Classical.choice present"
+            exit 1
+          fi
diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml
index f66c1bc..b71d2cb 100644
--- a/.machine_readable/6a2/ECOSYSTEM.a2ml
+++ b/.machine_readable/6a2/ECOSYSTEM.a2ml
@@ -4,8 +4,8 @@
 # ECOSYSTEM.a2ml — tropical-resource-typing ecosystem position
 
 [metadata]
-version = "0.2.1"
-last-updated = "2026-04-26"
+version = "0.2.2"
+last-updated = "2026-06-11"
 
 [project]
 name = "tropical-resource-typing"
@@ -45,10 +45,14 @@ isabelle = [
   { file = "Tropical_CNO.thy", description = "CNO (Construction from Neutral Objects) tropical connection" },
 ]
 lean4 = [
-  { file = "TropicalSessionTypes.lean", description = "Speculative tropical session types; soundness + QTT refinement" },
+  { file = "TropicalSessionTypes.lean", description = "Max-plus semiring (⊕=max,⊗=+); speculative session types; soundness + QTT refinement. Lean 4.13.0, Init only." },
+  { file = "TropicalAdapterPath.lean", description = "Min-max/bottleneck semiring (⊕=min,⊗=max); adapter-path optimisation; hub_ceiling no-go; the De Morgan duality bridge to the max-plus twin. Source: protocol-squisher frozen provenance." },
+  { file = "lakefile.lean", description = "Lake package; lean_lib over both roots. `lake build` is green." },
+  { file = "lean-toolchain", description = "Pins leanprover/lean4:v4.13.0 (no Mathlib)." },
 ]
 docs = [
-  { file = "docs/FORMAL-PROOFS.adoc", description = "Formal proofs documentation" },
+  { file = "docs/LEAN-FORMALIZATION.adoc", description = "AUTHORITATIVE Lean reference: both twins, duality, build/verify recipe, theorem index, axiom audit (propext/Quot.sound only), provenance." },
+  { file = "docs/FORMAL-PROOFS.adoc", description = "Formal proofs documentation (NOTE: Lean code listings predate v6.0 — see LEAN-FORMALIZATION.adoc)." },
   { file = "docs/HANDOVER.adoc", description = "Handover guide for continuing the research" },
 ]
 pdf = [
diff --git a/CHANGELOG.md b/CHANGELOG.md
index b012970..1620f2b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,6 @@
 <!--
 SPDX-License-Identifier: MPL-2.0
-SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> (hyperpolymath)
 -->
 
 # Changelog
@@ -20,6 +20,10 @@ this project aims to follow [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 
+- feat(lean4): migrate the min-max transport semiring (TropicalAdapterPath) in beside the max-plus twin; pin Lean 4.13.0 via lean-toolchain; add lakefile + lake-manifest; `lake build` green
+- feat(lean4): prove the De Morgan duality bridge — dualGrade_invol, dual_tcAdd_is_max (dual of min = max), dual_tcMul_is_min (dual of max = min)
+- docs(lean4): add docs/LEAN-FORMALIZATION.adoc (authoritative Lean reference: build/verify recipe, theorem index, axiom audit, provenance) + README section
+- ci(lean4): add lean.yml — lake build + axiom audit (propext/Quot.sound only, no sorry) on push/PR
 - feat(isabelle): close all sorries in Tropical_Kleene and Tropical_Matrices_Clean
 - feat(isabelle): close all sorries in Tropical_CNO.thy
 - feat(determinants): add Tropical_Determinants.thy — optimal assignment theorem
@@ -33,6 +37,8 @@ this project aims to follow [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Fixed
 
+- fix(lean4): repair TropicalSessionTypes + TropicalAdapterPath to compile clean under core Lean 4.13.0 — import ordering, Mathlib-only `push_neg`→core tactics, `AdapterPath` def→abbrev, local `One` shim (4.13.0 core lacks One), `pathCost_append`/`pathCost_le_sequential` reproved; the inherited "Verified" headers were never true
+- fix(lean4): replace the FALSE `dual_tcMul_bounded` (`dual(max m n)=dual m+dual n−maxGrade`, wrong at m=1,n=2) with the correct De Morgan dual `dual_tcMul_is_min`
 - fix(ci): sync hypatia-scan.yml to canonical (413: env.HOME+Phase-2+SARIF) (#1)
 - fix(Tropical_Semirings): close all 16 sites + ~10 doc drifts — session GREEN under Isabelle 2025-1
 - fix(Tropical_CNO): close 4 more sites — triangle NegInf cases, CNO close conditional, ge_id 1=Fin0
@@ -44,6 +50,7 @@ this project aims to follow [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Documentation
 
+- docs(lean4): note that docs/FORMAL-PROOFS.adoc's code listings predate the v6.0 source (illustrative API); point to LEAN-FORMALIZATION.adoc as authoritative
 - docs(swarm): SWARM-SESSION 2026-04-26 + 6a2 sextet completion + STATE update
 - docs(afp): update HANDOVER_v2 — all sorries closed, AFP submission ready
 - docs: add arXiv paper outline for Rigorous Tropical Session Types
diff --git a/README.adoc b/README.adoc
index bea4476..d822744 100644
--- a/README.adoc
+++ b/README.adoc
@@ -3,6 +3,7 @@
 :icons: font
 :revdate: 2026-05-26
 // SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 A short technical note introducing a **max-plus (tropical) algebraic
 approach to resource-aware type systems**, with applications to
@@ -69,6 +70,36 @@ just test
 * **Audit findings**: see `docs/tech-debt-2026-05-26.md` if present
   (added by the 2026-05-26 estate tech-debt scan).
 
+== Lean 4 formalization
+
+Two dependency-free Lean 4 proofs sit at the repository root — the
+*order-reversing twins* of one tropical duality, built together by Lake and
+pinned to **Lean 4.13.0** (`lean-toolchain`, `import Init` only, no Mathlib):
+
+`TropicalSessionTypes.lean`::
+The **max-plus** semiring (⊕ = max, ⊗ = +) grading speculative session types:
+`soundness` (static grade = dynamic wall-clock cost) and
+`tropical_grade_le_sequentialTotal` (the QTT refinement, `max ≤ sum`).
+
+`TropicalAdapterPath.lean`::
+The **min-max** / bottleneck semiring (⊕ = min, ⊗ = max) grading adapter paths.
+Home of `hub_ceiling`, the no-go corollary that closes Protocol Squisher's
+universal-interoperability claim. (Source: the frozen provenance archive in
+`protocol-squisher`, left unchanged there.)
+
+The two are connected by the order-reversing involution `g ↦ maxGrade − g`,
+proved here as a lattice *anti-isomorphism* (De Morgan: it exchanges min and
+max), not a semiring homomorphism.
+
+[source,bash]
+----
+lake build          # green; no network deps
+----
+
+`lake build` is green and every headline theorem depends only on `propext`
+(+ `Quot.sound`) — no `sorry`, no `Classical.choice`. Full detail, build/verify
+recipe, theorem index and provenance: link:docs/LEAN-FORMALIZATION.adoc[`docs/LEAN-FORMALIZATION.adoc`].
+
 == Reading order
 
 . Start with `document/` for the conceptual content.
diff --git a/docs/FORMAL-PROOFS.adoc b/docs/FORMAL-PROOFS.adoc
index 3858d82..f717e53 100644
--- a/docs/FORMAL-PROOFS.adoc
+++ b/docs/FORMAL-PROOFS.adoc
@@ -5,6 +5,18 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 :toc:
 :icons: font
 
+[IMPORTANT]
+====
+*Lean API drift 2026-06-11.* The Lean code listings below
+(`tropicalGrade`, `EvaluatesTo`, `spec_branch`, `linearBilling`,
+`TropicalBudget`) are *illustrative* and predate the v6.0 source. They do
+**not** match the file on disk, whose live, compiling definitions are `grade`,
+`Span`, `spec_par`, `sequentialTotal`, and the `Tropical` carrier. For the
+authoritative Lean reference — both twins, the duality, the build/verify recipe,
+the theorem index and the axiom audit — see
+link:LEAN-FORMALIZATION.adoc[`docs/LEAN-FORMALIZATION.adoc`].
+====
+
 [NOTE]
 ====
 *Errata 2026-04-26 (revised).* This document and `HANDOVER_v2.adoc`
diff --git a/docs/LEAN-FORMALIZATION.adoc b/docs/LEAN-FORMALIZATION.adoc
new file mode 100644
index 0000000..61e513e
--- /dev/null
+++ b/docs/LEAN-FORMALIZATION.adoc
@@ -0,0 +1,190 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+= Lean 4 Formalisation: the Tropical Duality (min-max ⇄ max-plus)
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+2026-06-11
+:toc:
+:toc-placement: preamble
+:icons: font
+:sectnums:
+
+This is the authoritative reference for the Lean 4 development that lives at the
+repository root: two *order-reversing twins* and the duality connecting them,
+plus how to build and independently re-verify them.
+
+[NOTE]
+====
+The older `docs/FORMAL-PROOFS.adoc` predates the v6.0 source: its Lean code
+listings (`tropicalGrade`, `EvaluatesTo`, `spec_branch`, `linearBilling`) show
+an earlier, *illustrative* API that does not match the file on disk. The live,
+compiling definitions are the ones described **here**.
+====
+
+== TL;DR
+
+* Two files, one Lake library, pinned to **Lean 4.13.0** (`lean-toolchain`),
+  **no Mathlib** (`import Init` only).
+* `TropicalSessionTypes.lean` — the **max-plus** semiring (⊕ = max, ⊗ = +),
+  grading speculative session types.
+* `TropicalAdapterPath.lean` — the **min-max** (bottleneck) semiring
+  (⊕ = min, ⊗ = max), grading adapter paths; home of the `hub_ceiling` no-go.
+* The twins are connected by the order-reversing involution `g ↦ maxGrade − g`,
+  proved here as a lattice **anti-isomorphism** (De Morgan): it exchanges
+  `min` and `max`.
+* `lake build` is green; every headline theorem depends only on `propext`
+  (+ `Quot.sound`) — no `sorry`, no `Classical.choice`.
+
+== Build and verify
+
+[source,bash]
+----
+# The toolchain is pinned in ./lean-toolchain (leanprover/lean4:v4.13.0);
+# elan reads it automatically. No network deps — Init only.
+lake build
+
+# Independent axiom audit of the headline theorems:
+lake env lean /dev/stdin <<'EOF'
+import TropicalSessionTypes
+import TropicalAdapterPath
+#print axioms Hyperpolymath.Tropical.soundness
+#print axioms Hyperpolymath.Tropical.tropical_grade_le_sequentialTotal
+#print axioms Hyperpolymath.ProtocolSquisher.Tropical.pathCost_mono
+#print axioms Hyperpolymath.ProtocolSquisher.Tropical.hub_ceiling
+#print axioms Hyperpolymath.ProtocolSquisher.Tropical.dualGrade_invol
+EOF
+----
+
+Expected: each prints `depends on axioms: [propext]` or `[propext, Quot.sound]`.
+CI runs exactly this (`.github/workflows/lean.yml`).
+
+== File 1 — `TropicalSessionTypes.lean` (max-plus)
+
+Namespace `Hyperpolymath.Tropical`. Grades speculative session types so that the
+*static* type-level cost equals the *dynamic* wall-clock cost.
+
+[cols="1,3"]
+|===
+| Construct | Meaning
+
+| `Tropical` | carrier `val n \| bot`; `bot` is −∞ (additive identity of `max`)
+| `tAdd` / `tMul` | `⊕ = max`, `⊗ = +` (nat addition)
+| `CommSemiring Tropical` | all 13 laws wired from the individually-proved theorems
+| `Session` | `end_session \| send \| recv \| spec_par` (speculative parallel branch)
+| `grade : Session → Tropical` | static cost; `spec_par` uses `tAdd` (= max over branches)
+| `Span : Session → Nat` | dynamic wall-clock cost
+| `soundness` | `grade s = val (Span s)` — static = dynamic, exactly
+| `grade_ne_bot` | every session has finite cost
+| `sequentialTotal` | the naïve QTT billing (sum over branches)
+| `tropical_grade_le_sequentialTotal` | `Span s ≤ sequentialTotal s` (QTT refinement)
+|===
+
+Toolchain note: Lean 4.13.0 core ships `Zero` but **not** `One`, so the file
+defines a minimal local `One` class plus an `OfNat _ 1` bridge to keep the
+Mathlib-compatible interface and `1` notation working without Mathlib.
+
+== File 2 — `TropicalAdapterPath.lean` (min-max / bottleneck)
+
+Namespace `Hyperpolymath.ProtocolSquisher.Tropical`. Grades adapter paths in
+Protocol Squisher's 4-class transport semilattice (Concorde / Business /
+Economy / Wheelbarrow), where path cost is the *bottleneck* (worst step).
+
+[cols="1,3"]
+|===
+| Construct | Meaning
+
+| `TransportClass`, `grade`, `maxGrade` | 4 classes; `grade` embeds them as `0..3` (0 = best)
+| `tcJoin` + `tcJoin_*` | the worst-of-two join semilattice (comm/assoc/idem, Concorde identity)
+| `AdapterPath` (`abbrev`) | `List TransportClass`; `abbrev` so List lemmas apply through the alias
+| `pathCost`, `pathCost_cons`, `pathCost_mono`, `pathCost_append` | bottleneck cost and its algebra
+| `tcAdd`/`tcMul`/`tcZero`/`tcOne` + axioms | the min-max semiring (`⊕ = min`, `⊗ = max`), a dioid
+| `minimax_path_optimal` | the foldl-min over alternatives is the optimal (lowest-bottleneck) path
+| `pathCost_le_sequential` | bottleneck ≤ naïve sequential total (the min-max analogue of QTT refinement)
+| `hub_ceiling` | *the no-go corollary* (see below)
+|===
+
+=== `hub_ceiling` — the closing result
+
+`hub_ceiling : e ∈ path → grade e ≤ pathCost path`. Any path routing through an
+edge of grade `g` costs at least `g`. Read as interop policy: one shared hub
+caps the fidelity of every format that must pass through it, so "universal" and
+"high fidelity" are contradictory the moment any format embeds at grade > 0;
+universal *low* fidelity is the achievable point (that is what JSON already is).
+This corollary closes Protocol Squisher's universal-interoperability claim using
+the project's own algebra. Machine-checked, depends only on `propext`.
+
+== The duality: `g ↦ maxGrade − g`
+
+`dualGrade n = maxGrade − min n maxGrade` is the order-reversing involution on
+`[0, maxGrade]`.
+
+[cols="1,2"]
+|===
+| Theorem | Statement
+
+| `dualGrade_invol` | `dualGrade (dualGrade n) = n` for `n ≤ maxGrade`
+| `dual_tcAdd_is_max` | `dual (min a b) = max (dual a) (dual b)`
+| `dual_tcMul_is_min` | `dual (max a b) = min (dual a) (dual b)`
+|===
+
+These are the precise, *provable* statements of the connection between the
+min-max transport semiring and the max-plus session semiring: `dualGrade` is a
+lattice **anti-isomorphism** that swaps `min` and `max` by De Morgan. It is
+**not** a semiring homomorphism from (min,max) to (max,+).
+
+[WARNING]
+====
+The inherited file contained a theorem `dual_tcMul_bounded` asserting
+`dual (max m n) = dual m + dual n − maxGrade`. That statement is *false*
+(`m = 1, n = 2`: LHS `dual 2 = 1`, RHS `2 + 1 − 3 = 0`) — its own comment
+admitted as much. It is replaced by the true De Morgan dual `dual_tcMul_is_min`
+above. The migration repaired theorems; it did not force-prove the false one.
+====
+
+== Provenance and honesty
+
+The min-max file's *source* is the frozen provenance archive in the sibling
+repo: `protocol-squisher/provenance/proofs/tropical/TropicalAdapterPath.lean`.
+That copy is evidence and is left **unchanged**. As inherited, neither twin
+compiled on any installed toolchain (the headers' "Verified" claims were never
+true — corroborating protocol-squisher's `PROVENANCE.adoc`). Only `pathCost_mono`
+and `hub_ceiling` had previously been machine-checked, in isolation. The repair
+inventory is recorded verbatim in the migration commit and in `CHANGELOG.md`.
+
+== Relationship to the rest of the repo and the estate
+
+* *Isabelle/HOL* (`Tropical*.thy`, `ROOT`): the matrix-algebra / Kleene /
+  determinant development of the same max-plus and min-plus semirings. The Lean
+  files are the lightweight, dependency-free, executable core; the Isabelle
+  files are the heavyweight algebra. See `docs/HANDOVER_v2.adoc` and
+  `docs/BUILD-STATUS-2026-04-26.adoc` for the Isabelle build state.
+* *protocol-squisher*: `hub_ceiling` is the result that closes its universal
+  claim; the min-max file originated there.
+* *typed-wasm*, *echo-types*: downstream target and sibling formal-foundations
+  work (see README "Companion repositories").
+
+== Theorem index (axioms audited 2026-06-11, Lean 4.13.0)
+
+[cols="2,1,1"]
+|===
+| Theorem | File | Axioms
+
+| `soundness` | SessionTypes | propext
+| `tropical_grade_le_sequentialTotal` | SessionTypes | propext, Quot.sound
+| `grade_ne_bot` | SessionTypes | propext
+| `pathCost_mono` | AdapterPath | propext
+| `hub_ceiling` | AdapterPath | propext
+| `pathCost_append` | AdapterPath | propext, Quot.sound
+| `pathCost_le_sequential` | AdapterPath | propext, Quot.sound
+| `dualGrade_invol` | AdapterPath | propext, Quot.sound
+| `dual_tcAdd_is_max` | AdapterPath | propext, Quot.sound
+| `dual_tcMul_is_min` | AdapterPath | propext, Quot.sound
+|===
+
+== Open items (carried from the file headers)
+
+* Generalise `minimax_path_optimal` to full graph-algorithmic Dijkstra
+  correctness (Mohri 2002).
+* State the QTT quotient morphism explicitly (currently proved via the
+  refinement theorem, not stated as a morphism).
+* Add recursion / choice to `Session`; multiparty extension.
+* Cross-verify the Lean duality against the Isabelle `Tropical_Ordinal_Bridge`.