dm³ 101 · Week 12 · Lean Lab

AXLE: Mechanising φ

What’s formalized for the Tribonacci rung, and what’s still missing for Fibonacci
dm³ 101 · Week 12 · Lean Lab
AXLE: Mechanising φ
Course: dm³ 101  ·  Lean Lab  ·  Source: TribonacciMeasure.lean, TribonacciRatioConvergence.lean, AXLE repo

Search the AXLE repo for Fibonacci-specific Lean files and you will not find one. Search for Tribonacci and you will find three: TribonacciMeasure.lean, TribonacciRatioConvergence.lean, and TribonacciDNLS.lean — all reporting sorry_count: 0. This asymmetry is real and worth understanding rather than glossing over.

Why η (Tribonacci) got formalized first, not φ (Fibonacci)
\(\eta\) sits at the critical rung of the ladder (\(n=3\), tied to the Collatz map’s \(c=3\)) — it is the constant load-bearing the framework’s flagship application. \(\varphi\) is subcritical (Week 9) and, mathematically, is the special case that needed the least new machinery — its convergence properties are 19th-century number theory, not novel results requiring formal verification to be trusted. Formalization effort went where it was structurally necessary first.

What this means concretely for this course: the strict antitonicity of the Tribonacci-derived amplitude sequence is machine-verified (TribonacciMeasure.lean); the ratio convergence to \(\eta\) is machine-verified (TribonacciRatioConvergence.lean); a discrete nonlinear Schrödinger realization on a Tribonacci substitution chain is machine-verified for amplitude decay (TribonacciDNLS.lean) — and none of the analogous Fibonacci/\(\varphi\) statements from Weeks 9–11 currently have a Lean file. The convergence claims are numerically verified (Week 10’s table) and classically well-established in the mathematical literature, but not yet formalized inside this specific project’s Lean codebase.

This week’s exercise is diagnostic, not a coding task: open the AXLE repo, confirm the three Tribonacci files exist and report 0 sorry, confirm no equivalent Fibonacci file exists, and write one sentence on what a minimal FibonacciRatioConvergence.lean would need to state to close this specific gap (hint: it would mirror TribonacciRatioConvergence.lean’s structure with \(n=2\) in place of \(n=3\)).
This gap is open on purpose — it’s yours to take
AXLE is a living, actively maintained repo, not a closed textbook. The missing FibonacciRatioConvergence.lean is a real gap, not a rhetorical one, and it is genuinely tractable at the 101 level: the proof pattern already exists in TribonacciRatioConvergence.lean, the target statement is classical (F(n+1)/F(n) → φ), and Mathlib almost certainly already has the Fibonacci and limit lemmas you’d need. Formalizing it is a legitimate first open-source Lean contribution — write the file, confirm sorry_count: 0 locally, and open a pull request against github.com/TOTOGT/AXLE. This is not a hypothetical exercise for a grade; it is how this specific gap in the actual project gets closed, and your name goes on the commit.
This week’s content is grounded in Principia Orthogona, Book 3 (“The Recurrence Ladder”) and AXLE_v6.lean — theorem names and Lean identifiers above point at the actual source files.
-- dm³ 101 · Week 12 · Diagnostic — φ formalization gap
--
-- Confirmed present in AXLE (0 sorry each):
--   TribonacciMeasure.lean
--   TribonacciRatioConvergence.lean
--   TribonacciDNLS.lean
--
-- Confirmed absent from AXLE:
--   (no FibonacciMeasure.lean / FibonacciRatioConvergence.lean)
--
-- Exercise: sketch the statement (not proof) of what
-- FibonacciRatioConvergence.lean would need to assert to mirror
-- TribonacciRatioConvergence.lean at n=2.
example : True := trivial
← Week 11 ↑ dm³ 101 Course Week 13 →