feat(lean): migrate + repair tropical proofs; unify the min-max ⇄ max-plus duality

.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://github.com/ghraw/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

.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

.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 = [

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

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.