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 Gronwall 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.

SpiralReturn — Formalising Theorem 2.1

The ODE itself is a Picard–Lindelöf application. Mathlib's ODE.Gronwall and ODE.PicardLindelof give us existence, uniqueness, and the Gronwall lemma. The skeleton below shows the statement in its current form.

/- AXLE/SpiralReturn.lean — Theorem 2.1 (symmetric) -/
import AXLE.Chain
import Mathlib.Analysis.ODE.PicardLindelof
import Mathlib.Analysis.SpecialFunctions.Log.Basic

namespace AXLE

/-- The dm³ radial equation at ε = 2. -/
noncomputable def dm3Radial (z : ℝ) (r : ℝ) : ℝ :=
  r * (1 - r^2) + 2 * (r - 1) * Real.exp (-z)

/-- Theorem 2.1 (symmetric): if |r₀ - 1| < 1/3 and z₀ ≥ log 2,
    the solution converges exponentially to r = 1 at rate -2. -/
theorem spiralReturn
    {r₀ z₀ : ℝ}
    (hr : |r₀ - 1| < 1/3)
    (hz : z₀ ≥ Real.log 2) :
    ∃ (r : ℝ → ℝ), ∃ (μ : ℝ), μ < 0 ∧
      r 0 = r₀ ∧
      (∀ t ≥ 0, |r t - 1| ≤ |r₀ - 1| * Real.exp (μ * t)) := by
  -- Step 1: apply Picard–Lindelöf for local existence
  -- Step 2: derive the scalar inequality ½ d/dt u² ≤ (-2 + 3ε₀ + εe^{-z₀}) u²
  -- Step 3: apply Mathlib.Analysis.ODE.Gronwall
  -- Step 4: the Lipschitz bound needed at Step 2 — see Issue #12
  sorry

end AXLE

What is proved, what is sorry

Steps 1 and 3 of the proof sketch are library calls. Mathlib's ODE.PicardLindelof and ODE.Gronwall are complete, maintained, and well-documented. Step 2 — producing the scalar inequality from the radial equation — needs a bound on the coupling term. That bound is the content of Issue #12.

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 Gronwall 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.