An earlier draft of this course closed with a “1080-Proofs Programme,” framing a numerical coincidence between critDim_monotone and \(\tau=2\) as evidence of a grand closing structure. That framing depended on the same removed Navrátil-sourced axioms and is dropped here. What replaces it is better: AXLE v6.1’s own bilingual (PT/EN) audit chapter, which states its status plainly rather than dramatically — 9 sorrys total, all honestly named (each with a comment specifying exactly what library lemma or construction is missing, not left as a bare placeholder), 8 verified constants (Week 14), 0 axioms beyond Mathlib4, across 794 lines of Lean 4.
dm3_euler_preservation, dm3_volume_invariant, g6_lattice_invariant, g6_symmetry_preservation, regeneration_hierarchy_mahlo_unconditional, collective_threshold_structural, g7_representation, and two others — each one is a real, findable line in the AXLE source, not a rhetorical gesture. “0 axioms beyond Mathlib4” is the more load-bearing claim here: it means AXLE’s proved results (Theorem C.1, tau_embodiment, the η/Cardano files, gronwall_outer) don’t quietly smuggle in unverified assumptions the way the removed critDim material did.
This is the honest-accounting standard this course has tried to model throughout — from CollatzDescent.lean’s self-correcting §7 in 102, to the r* proved-value-vs-open-theorem split, to this week’s G⁵/G⁶ correction. A named, bounded list of 9 gaps is a stronger closing claim than an unverified “1080” ever was.
-- dm³ 103 · Week 15 · The 9 Honest Sorrys (replaces "1080-Proofs") -- AXLE v6.1 audit (chV-sorrys.html), 794 lines Lean 4: -- 9 sorrys total, ALL honestly named (comment states missing lemma) -- 8 verified constants (Week 14 table) -- 0 axioms beyond Mathlib4 -- -- Sample named sorrys: -- dm3_euler_preservation, dm3_volume_invariant, -- g6_lattice_invariant, g6_symmetry_preservation, -- regeneration_hierarchy_mahlo_unconditional, -- collective_threshold_structural, g7_representation, (+2 more) -- -- REMOVED: "1080-Proofs Programme" — depended on critDim_monotone, -- scrubbed in 102. A bounded, named list of 9 beats an unverified -- large number. example : True := trivial