Final assessment for dm³ 103, and for the three-course sequence: assemble one table covering every named constant and theorem from 101, 102, and 103, each with its precise status (proved / certified numerically / structure data / open axiom / open conjecture), and submit it alongside a one-page reflection on the single largest correction this sequence made to its own earlier drafts (candidates: r*’s precise value, the critDim/Navrátil removal, or this course’s G⁵/G⁶ correction) and why holding that standard mattered more than the material that got removed.
| Constant / Result | Value | Status |
|---|---|---|
| \(\varphi\) (n=2) | 1.618… | Proved (closed form); no dedicated AXLE Lean file |
| \(\mu_{{\max}}\) | −2 | Proved (two independent derivations agree) |
| \(\varepsilon_0\) | 1/3 | Proved (gronwall_outer) |
| \(r^*\) | 0.77594059 | Certified numerically (8dp); general theorem still an axiom |
| \(\eta\) (n=3) | 1.839… | Proved (Cardano); 3 Lean files, 0 sorry |
| \(\Delta\) (n=4) | 1.928… | Proved (root) |
| Theorem C.1 (\(c^*=3\)) | — | Proved in full (102 Wks 7–8) |
Collatz descent | — | Even case + n∈{{3,5,7}} proved; 2 open sorries |
| \(\Sigma\) (n=5) | 1.966… | Proved via IVT bracketing; no closed radical form (Abel–Ruffini) |
| \(\Omega\) (n=6) | 1.984… | Proved (root); no closed radical form |
| Theorem Ω.1 (ladder→τ) | 2 | Proved (geometric-series limit, in full) |
| \(\rho(P_M)\) | \(1/2^{{M-1}}\) | Proved exactly (fixed-point eigenvalue) |
| \(\rho(\mathcal{{L}})\) | ≈0.751 | Numeric (weighted drift); Bridge 0 to \(\rho(P_M)\) is open |
| \(\tau=2\) reached at | \(G^5\) | Corrected this course (source: chV-g6.html), not \(G^9\) |
| \(G^6\) conjecture (\(\chi=33\)) | — | Explicitly open (AXLE Issue 6), numerically motivated only |
| AXLE v6.1 audit | — | 9 named sorrys, 8 verified constants, 0 axioms beyond Mathlib4 |
This closes the three-course dm³ sequence (101→102→103). Every removal made along the way — the critDim/Navrátil material, the Galilean Confluence claim, the 1080-Proofs framing, the G⁵ naming error — was made because a primary source either didn’t support the claim or explicitly contradicted it, and each removal was replaced with real, verifiable material rather than left as a gap.
-- dm³ 103 · Week 16 · Milestone VIII — full series table, final -- 101 → 102 → 103, one honest table (see prose for full version). -- Every correction made in this sequence was source-driven: -- r* : 0.80 (wrong) → 0.77594059 (certified, 8dp) -- 102: critDim/Navrátil/GTCT axioms → removed, replaced with -- CollatzDescent.lean (real, partially open, self-correcting) -- 103: "Galilean Confluence" → removed (Week 7) -- "1080-Proofs Programme" → replaced with 9 Honest Sorrys (Wk15) -- G⁹/"Vol IX" → corrected to G⁵ (Week 13, per chV-g6.html) -- -- Series complete. Portfolio: full constants table + 1-page -- reflection on the largest self-correction and why it mattered. example : True := trivial