-
-
Notifications
You must be signed in to change notification settings - Fork 0
Formal Verification Status
Honest cross-prover snapshot. The guiding rule for this repo (and the estate) is truth before vision: a green badge means a machine actually checked it.
| Prover | Artefacts | Status (2026-06-11) |
|---|---|---|
| Lean 4 |
TropicalSessionTypes.lean, TropicalAdapterPath.lean
|
✅ Green. lake build clean under pinned 4.13.0; axiom-audited (propext / Quot.sound only; no sorry, no Classical.choice). |
| Isabelle/HOL |
Tropical*.thy, ROOT
|
sorry). See the in-repo build status. |
| Julia | impl/ |
Reference checker — illustrative, not a verifier. |
-
Soundness (
soundness): static tropical grade = dynamic wall-clock cost, exactly. -
QTT refinement (
tropical_grade_le_sequentialTotal): tropical budget ≤ sequential billing (max ≤ sum). -
Hub ceiling (
hub_ceiling): the no-go corollary closing the universal-interop claim. -
Duality (
dualGrade_invol,dual_tcAdd_is_max,dual_tcMul_is_min): the min-max ⇄ max-plus De Morgan anti-isomorphism.
Full detail and the theorem/axiom table: Lean 4 Formalization.
The Isabelle development (5,600+ LOC of Isar, no sorry/oops in proof bodies) regressed
under Isabelle 2025-1 due to version drift (e.g. a HOL.Permutations/HOL.Bij
class-instance change and a hypothesis weakness in path_weight_cycle_excise). The body
of work is intact; the failures are mechanical version reconciliation. Authoritative
detail:
docs/BUILD-STATUS-2026-04-26.adoc-
docs/FORMAL-PROOFS.adoc(errata) docs/SESSION-REPORT-2026-05-11.adoc
The Lean migration found and corrected a false theorem inherited from the source
(dual_tcMul_bounded). This is recorded openly in the changelog, the source comments,
and the Lean 4 Formalization page — consistent with the repo's documented preference
for closing claims honestly rather than re-narrating them.
See also: Home · Lean 4 Formalization