Volume I §13 gives an explicit correspondence between the abstract operators of this paper and the concrete dm³ toy model used throughout the wider Principia Orthogona series — the bridge from “proved abstract structure” to “numbers you can check.”
| Volume I | dm³ Toy Model | Lean |
|---|---|---|
| Compression C | Basin contraction | CompressionOp.contractive ✓ |
| Curvature flow K | Lyapunov descent \(\dot V \le -cV\) | gronwall_contraction_below_stability_radius ✓ |
| Fold F | Whitney \(A_1\) at \(q^*=1\) | V_factored, V_critical_at_one ✓ |
| Unfolding U | Gradient flow to \(\Gamma\) | UnfoldOp.stable_branch ✓ |
| Entropy E | \(\dot z \ge 0\) | Theorem T1 — open (O3) |
The worked toy model carries concrete, calibrated constants worth memorizing before Week 5: Lyapunov exponent \(\mu_{{\max}} = -2\), Gronwall basin radius \(\varepsilon_0 = 1/3\), inner basin boundary \(r^* \approx 0.776\), and the canonical triple \((T^*, \mu_{{\max}}, \tau) = (2\pi, -2, 2)\) — note \(\tau = 2\) appears here as a defined embodiment-threshold constant, not as something derived through a multi-week argument.
PrincipiaVol1.lean in the AXLE repo and locate CompressionOp.contractive, UnfoldOp.stable_branch, and gronwall_contraction_below_stability_radius. Confirm for yourself which of the five rows in the table above are proved (0 sorry) versus open, using §17’s Formal Status table as the source of truth — don’t take this page’s word for it.PrincipiaVol1.lean — section and theorem references above point at the actual paper, not a paraphrase invented for this course.-- dm³ 101 · Week 04 · Milestone — §17 Formal Status, PrincipiaVol1.lean -- -- Machine-checked (0 sorry unless noted): -- Theorems A–D (operator structures: C, K, F, U) ✓ -- Gronwall contraction exponent sign ✓ -- P2: Contact non-degeneracy c(ρ) ✓ -- P5: Lyapunov exponents μ_max = -2 ✓ -- -- Open obligations (explicitly not proved): -- O1 AXLE #12 — eigenvalue API gap (separation_theorem) -- O3 AXLE #15 / Theorem T1 — full ODE Gronwall (entropy E) -- O6 Conjecture 16.1 — discrete N=3 / c=3 threshold -- -- Milestone: verify these claims against the real file before -- treating any of them as settled. example : True := trivial