Final assessment: a 2-page written proof summary covering (a) Theorem C.1’s \(c^*=3\) derivation (Weeks 7–8) and (b) the orbit_halving attempt and the Terras/Everett strategy for the harder gap (Weeks 10–12), submitted alongside your Lean portfolio (Week 4’s abstract-vs-concrete \(r^*\) distinction, Week 8’s Cardano derivation for \(\eta\), your Week 12 Lean attempt). Grading rewards precision about the proved/open boundary over enthusiasm about any external framing — the same standard this course has held since Week 1.
| Constant | Value | Status |
|---|---|---|
| \(\mu_{{\max}}\) | −2 | Proved (two independent derivations agree) |
| \(\varepsilon_0\) | 1/3 | Proved (gronwall_outer, symmetric bound) |
| \(r^*\) | 0.77594059 | Value certified (8dp); general asymmetry still an axiom |
| \(\eta\) (n=3) | 1.839… | Proved (Cardano, closed form); 3 Lean files, 0 sorry |
| \(\Delta\) (n=4) | 1.928… | Proved (root); rank-supercritical, potential-subcritical |
| Theorem C.1 (\(c^*=3\)) | — | Proved (Weeks 7–8, worked in full) |
Collatz descent | — | Even case + n∈{{3,5,7}} proved; general odd case: 2 open sorries (Weeks 10–12) |
Portfolio submission: proof summary + this table, annotated with your own check marks. dm³ 103 opens with \(\Sigma\), \(\Omega\), and \(\rho\) (spectral radius, developed properly) — built entirely on material this course has verified directly, with no dependency on the external source removed earlier in this course.
CollatzDescent.lean, the criticality bridge (Weeks 7–8), and this course’s own constants — no material in this page depends on the external, unverified source removed from earlier drafts of this course.-- dm³ 102 · Week 16 · Milestone IV — full constants + axiom audit
--
-- Proved outright:
-- μ_max = -2 (two independent derivations agree)
-- ε₀ = 1/3 (gronwall_outer)
-- η ≈ 1.839 (Cardano closed form; 3 Lean files, 0 sorry)
-- Δ ≈ 1.928 (quartic root)
-- Theorem C.1 (c*=3 fold, Weeks 7-8) — worked in full by hand
--
-- Certified numerically, not formally proved as general theorem:
-- r* = 0.77594059 (asymmetry itself still an axiom)
--
-- Genuine open problem, honestly scoped (CollatzDescent.lean):
-- descent: even case + n∈{3,5,7} proved; general odd case has
-- 2 sorries — orbit_halving (tractable, attempted Week 12) and
-- the Nat.log 2-induction case (harder, Terras/Everett strategy)
--
-- Course complete. dm³ 103 begins with Σ, Ω, ρ — built entirely on
-- material this course verified directly.
example : True := trivial