O3: Theorem T1 — full ODE Gronwall integration (z(t) monotonicity)

[TOTOGT]

Partial closure (V3)

gronwall_contraction_below_stability_radius in PrincipiaVol1.lean §8
proves the decay exponent sign: (μmax + 3ε)·T* < 0 for all ε < 1/3.
This is 0 sorry. This is the necessary condition for contraction.

What remains open

The full bound: ‖δxₜ‖ ≤ ‖δx₀‖·exp((μmax + 3ε)·t)
Requires defining the dm³ vector field as a C¹ map and invoking
Mathlib.Analysis.ODE.Gronwall on the explicit ODE.

Closure path

1. Define dm³ semiflow formally in Lean
2. Prove vector field is C¹ on the Gronwall basin
3. Apply ODE.Gronwall to get the exponential bound
4. Conclude z(t) monotonicity from ż = r² − 2(r−1)²e^{−z} ≥ 0

Files

PrincipiaVol1.lean §8, gronwall_proof.lean

Label

lean-sorry, mathlib-gap, theorem-T1