Lean 4 Formalization

Lean 4 Formalization

Two order-reversing twins and the duality connecting them, at the repository root. Authoritative source doc: docs/LEAN-FORMALIZATION.adoc.

TL;DR

• 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.
• Connected by the order-reversing involution g ↦ maxGrade − g, proved as a lattice anti-isomorphism (De Morgan: it swaps min and max).
• lake build is green; every headline theorem depends only on propext (+ Quot.sound) — no sorry, no Classical.choice.

Build and verify

lake build          # toolchain auto-read from ./lean-toolchain; no network deps

# axiom audit
lake env lean /dev/stdin <<'EOF'
import TropicalSessionTypes
import TropicalAdapterPath
#print axioms Hyperpolymath.Tropical.soundness
#print axioms Hyperpolymath.ProtocolSquisher.Tropical.hub_ceiling
EOF

CI (.github/workflows/lean.yml) runs lake build + this audit and fails on any sorry/Classical.choice.

File 1 — TropicalSessionTypes.lean (max-plus)

Namespace Hyperpolymath.Tropical. Grades speculative session types so the static type-level cost equals the dynamic wall-clock cost.

Construct	Meaning
Tropical	carrier val n | bot; bot = −∞ (identity of max)
tAdd / tMul	⊕ = max, ⊗ = +
CommSemiring Tropical	all 13 laws wired
Session / grade / Span	sessions; static grade; dynamic span
soundness	grade s = val (Span s)
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 + OfNat _ 1 bridge to keep 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).

Construct	Meaning
TransportClass / grade / maxGrade	4 classes embedded as 0..3 (0 = best)
tcJoin + lemmas	worst-of-two join semilattice
AdapterPath (abbrev) / pathCost	path and its bottleneck cost
min-max semiring (tcAdd/tcMul/…)	⊕ = min, ⊗ = max (a dioid)
minimax_path_optimal	foldl-min over alternatives = optimal path
hub_ceiling	the no-go corollary (below)

hub_ceiling — the closing result

hub_ceiling : e ∈ path → grade e ≤ pathCost path. Any path through an edge of grade g costs at least g, so one shared hub caps the fidelity of every format passing through it: "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 closes Protocol Squisher's universal-interoperability claim using its own algebra.

The duality: g ↦ maxGrade − g

dualGrade n = maxGrade − min n maxGrade — the order-reversing involution on [0, maxGrade].

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)

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,+).

Correction (2026-06-11). The inherited file contained dual_tcMul_bounded asserting dual (max m n) = dual m + dual n − maxGrade, which is false (m=1, n=2: LHS 1, RHS 0). It is replaced by the true De Morgan dual dual_tcMul_is_min. The migration repaired theorems; it did not force-prove the false one.

Provenance & 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.

Theorem index (axioms audited 2026-06-11, Lean 4.13.0)

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

See also: Formal Verification Status · Home