dm³ 101 · Week 07 · Lean Lab

AXLE: Mechanising π

What is actually proved about T* = 2π in Lean 4, and what is still pending
dm³ 101 · Week 07 · Lean Lab
AXLE: Mechanising π
Course: dm³ 101  ·  Lean Lab  ·  Source: AXLE_v6.lean, GitHub TOTOGT/AXLE

This week is a Lean-reading exercise, not a Lean-writing one — the honest kind. Open AXLE_v6.lean in the AXLE repo and locate the Dm3Canonical structure (around the constants section). You will find:

What is actually in the file
structure Dm3Canonical where T_star : ℝ; mu_max : ℝ; tau : ℝ, followed by an instance assigning T_star := 2 * Real.pi. This is a definitional assignment: Lean accepts \(T^*=2\pi\) as given data of the structure, and separately proves derived facts such as tau_embodiment : tau^6 = 2^6 and spectral-closure facts noted near “dominant eigenvalue has period \(2\pi\) (\(\lambda_{{\text{{dom}}}}^6=1\))” in the file’s comments.

What is not in the file, and this matters for how you read this course: a full formal derivation, inside Lean, of the Reeb-flow compactification argument for Theorem π.1 (why \(z \in S^1=\mathbb{{R}}/2\pi\mathbb{{Z}}\) forces period exactly \(2\pi\)). The file itself flags this: a comment near the eigenvalue-period section reads “Pending: Mathlib Floquet theory / periodic orbit API.” That is an accurate, self-reported gap — the geometric argument is given in prose in Book 3, and the numerical/algebraic consequences (\(\tau^6=2^6\), spectral period \(2\pi\)) are proved, but the underlying periodic-orbit theorem is not yet machine-checked because Mathlib does not yet have the relevant Floquet-theory API built out.

This week’s actual exercise
Write down, in your own words, the difference between “\(T^*=2\pi\) is asserted as structure data and used correctly downstream” and “\(T^*=2\pi\) is derived from first principles inside Lean.” Both are legitimate states for a formal project to be in — but they are not the same claim, and conflating them is exactly the kind of overclaiming this course tries to avoid.
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 07 · Reading exercise on AXLE_v6.lean

-- 1. Locate the structure:
structure Dm3Canonical where
  T_star : ℝ; mu_max : ℝ; tau : ℝ

-- 2. Locate the instance (line ~253 in AXLE_v6.lean):
--    T_star := 2 * Real.pi; mu_max := -2; tau := 2

-- 3. Locate the downstream proved fact (~line 479):
--    "dominant eigenvalue has period 2π (λ_dom^6 = 1)"

-- 4. Locate the self-reported gap (~line 725):
--    "Pending: Mathlib Floquet theory / periodic orbit API."

-- Exercise: is the period-2π claim (a) asserted, (b) derived
-- from other proved Lean facts, or (c) proved from a Mathlib
-- API that doesn't exist yet? Answer for T_star specifically —
-- not for tau_embodiment, which IS fully proved.
example : True := trivial
← Week 6 ↑ dm³ 101 Course Week 8 →