Lean 4 Skeleton & AXLE Issue #12

What We Will Cover

1. 0 – 8 min — Why formalise? What Lean 4 / Mathlib 4 give us in this context.
2. 8 – 20 min — AXLE/Chain.lean walk-through: the operator chain $G = U\circ F\circ K\circ C$ as a Lean structure.
3. 20 – 35 min — SpiralReturn: the formal statement of Theorem 2.1 and what exists in Mathlib to close it.
4. 35 – 48 min — AXLE Issue #12: the open Lipschitz estimate. What it says, why it is the bottleneck.
5. 48 – 60 min — Q&A, contribution on-ramp, pointers to Mathlib's ODE and dynamics files.

Why Lean 4, Why Now

Theorem 2.1 in its symmetric form is an ODE result. Calculus says it is true. So why formalise it?

• Transparency. The Lyapunov chain in S2 had a half-dozen little assumptions ("assume $z(0) \geq \log 2$", "use the induction hypothesis", "absorb this constant"). In a paper this is normal. In Lean 4 each is a separate, type-checked obligation.
• Reuse. The operator chain $G = U\circ F\circ K\circ C$ is a structural claim about every chapter in GTCT. A Lean 4 formalisation of $G$ in one setting (here: the dm³ ODE) becomes a template for the other chapters.
• Discovery. Writing the proof down in Lean 4 is what exposed AXLE Issue #12: the Lipschitz estimate that our paper hand-waves. Lean would not accept the hand-wave. That is how the gap became a named issue.

AXLE/Chain.lean — The Operator Chain

The four-operator chain $G = U\circ F\circ K\circ C$ from GTCT (contraction, curvature, filter, unfolding) is represented as a dependent structure. Each operator is a map between state spaces with its own regularity hypothesis.

/- AXLE/Chain.lean — operator chain for GTCT -/
import Mathlib.Analysis.ODE.Gronwall
import Mathlib.Analysis.NormedSpace.Basic
import Mathlib.Topology.MetricSpace.Lipschitz

namespace AXLE

structure OperatorChain (α β γ δ ω : Type*)
    [MetricSpace α] [MetricSpace β] [MetricSpace γ]
    [MetricSpace δ] [MetricSpace ω] where
  C : α → β                 -- Contract
  K : β → γ                 -- Curvature
  F : γ → δ                 -- Filter
  U : δ → ω                 -- Unfold
  C_lip : LipschitzWith 1 C
  K_lip : ∃ L : ℝ≥0, LipschitzWith L K   -- ← Issue #12
  F_lip : LipschitzWith 1 F
  U_cont : Continuous U

def OperatorChain.compose
    (ch : OperatorChain α β γ δ ω) : α → ω :=
  ch.U ∘ ch.F ∘ ch.K ∘ ch.C

end AXLE

Reading the structure

Note the regularity hypotheses: $C$ and $F$ are non-expanding (LipschitzWith 1), $U$ only needs to be continuous (it fans information out, it need not preserve metric), and $K$ — the curvature operator, geometrically the dm³ radial flow — carries an existential Lipschitz constant. This is the crucial structural choice.

GCTC/Chain_updated.lean — Current Proof State

The canonical Lean file is now GCTC/Chain_updated.lean (updated 2026-04-18 in the GTCT repo). The symmetric $\varepsilon_0 = 1/3$ formulation has been replaced by an asymmetric-basin model. The snippet below shows the two key theorems: one proved, one still sorry.

/- GCTC/Chain_updated.lean — updated 2026-04-18 -/
-- ε₀ = 1/3 removed: false on the inner side (see FINDINGS.md).
-- Replaced with asymmetric basin: r_star ≈ 0.80 inner, unbounded outer.

/-- Inner-basin boundary (empirical; replaces ε₀ = 1/3). -/
noncomputable def r_star : ℝ := 0.8

/-- Outer-basin Lyapunov bound — PROVED. -/
theorem gronwall_outer
    (μ_max ε μ_bound : ℝ) (hμ_bound : 0 < μ_bound)
    (hμ : μ_max + 3 * ε ≤ -μ_bound) :
    ∃ C : ℝ, 0 < C ∧ ∀ t : ℝ, 0 ≤ t →
      Real.exp ((μ_max + 3 * ε) * t) ≤ C * Real.exp (-μ_bound * t) := by
  refine ⟨1, one_pos, ?_⟩
  intro t ht; rw [one_mul]
  apply Real.exp_le_exp.mpr
  exact mul_le_mul_of_nonneg_right hμ ht   -- ← proved

/-- Spiral Return (T1) — corrected hypothesis; still sorry. -/
theorem spiral_return_exists
    {X : Type*} [MetricSpace X] [SeminormedAddCommGroup X]
    (G : GChain X) (x₀ : X)
    (h_nontrivial : GChain.iter G 64 x₀ ≠ x₀) :
    ∃ sr : SpiralReturn X G, sr.x₀' ≠ sr.x₀ := by
  sorry   -- pending AXLE integration of dm³ flow dynamics

-- Two axioms mark the ODE dependency boundary:
--   axiom inner_basin_is_asymmetric  (inner side; TODO(AXLE) replace with ODE statement)
--   axiom outer_basin_unbounded      (outer side; TODO(AXLE) tie to dm³ flow)

end GCTC

What is proved, what is sorry, what is axiom

gronwall_outer is now proved — the corrected hypothesis ($\mu_{\max} + 3\varepsilon \leq -\mu_{\text{bound}}$, stronger than the old $< 0$) was what made the proof go through. Two theorems remain as sorry: spiral_return_exists and poincare_collatz. Two further claims are declared as axiom — a permanent dependency on the dm³ ODE once it is formalised in Mathlib: inner_basin_is_asymmetric and outer_basin_unbounded. An axiom is not a sorry: it extends the logical foundation, which means the "0 extra axioms" headline is only recoverable once those two are replaced with real ODE proofs.

AXLE Issue #12 — The Lipschitz Estimate

lemma kappa_lipschitz
    (ε₀ : ℝ) (hε₀ : 0 < ε₀) (hε₀' : ε₀ < 1/3)
    (z_lo : ℝ) :
    ∃ L : ℝ≥0, ∀ r₁ r₂ : ℝ, ∀ z : ℝ,
      |r₁ - 1| < ε₀ → |r₂ - 1| < ε₀ → z ≥ z_lo →
      |κ r₁ z - κ r₂ z| ≤ L * |r₁ - r₂| := sorry

Related: two already-closed issues

How to Contribute

The mini-curso has three kinds of take-home:

• Short-term (afternoon). Close Issue #12. Low difficulty, high clarity, named attribution in the AXLE commit log.
• Medium-term (week). Formalise Corollary 2.3 (the explicit basin) as a consumer of spiralReturn. Depends on #12 being closed.
• Long-term (research). Find the sign-aware Lyapunov function that yields $r_\star$. This is a paper, not an issue.

Relevant Mathlib files to read before starting

• Mathlib.Analysis.ODE.Gronwall — the comparison lemma.
• Mathlib.Analysis.ODE.PicardLindelof — local existence/uniqueness.
• Mathlib.Topology.MetricSpace.Lipschitz — LipschitzWith, LipschitzOnWith.
• Mathlib.Analysis.SpecialFunctions.Log.Basic — Real.log, Real.exp.

What the Course Did

In three hours we walked from contact 3-manifolds (S1) through Theorem 2.1 with its Lyapunov basin (S2) to a Lean 4 formalisation with one open obligation (S3). The formalisation is live, public, and welcomes contributions. The sharp basin $r_\star$ is open research. The dm³ simulator runs in any browser.