The object to be proved

Let ρ = r − 1 denote the radial displacement from the dm³ limit cycle Γ = {r = 1}. In the limit z → ∞ (the asymptotic phase), the transverse dynamics of the dm³ contact ODE reduce to a single scalar equation:

This is an exact, separable ODE with an asymptotically stable fixed point at ρ = 0 (r = 1). Three numerical quantities are extracted from it:

Theorem (P3 — Gronwall Stability Radius). The Gronwall stability radius^{[Ch 10]} of the dm³ limit cycle is

Below we give seven independent proofs of this value, following the seven-proof template established in the Contact-Geometric Theory of Generative Transitions (TOGT, doi:10.5281/zenodo.20682934) for the Tribonacci constant η.

Proof I — Lyapunov energy function

IW = ½ρ² with Ẇ ≤ μ_max·W

Define the Lyapunov energy W(ρ) = ½ρ². Differentiate along (★):

The Gronwall stability radius is the largest ε such that Ẇ ≤ μ_max·W for all |ρ| ≤ ε. With μ_max = −2 and W = ½ρ²:

This is ≤ 0 (i.e., Ẇ ≤ μ_max·W) if and only if 1 + 3ρ + ρ² ≥ 0. Evaluate at the boundary ρ = −1/3:

The quadratic q(ρ) = 1 + 3ρ + ρ² has roots at ρ = (−3 ± √5)/2 ≈ {−2.618, −0.382}. On the symmetric ball B(0, 1/3) ⊂ B(0, 0.382), q(ρ) achieves its minimum of 1/9 at ρ = −1/3, so q(ρ) ≥ 1/9 > 0 throughout. Therefore Ẇ ≤ μ_max·W on B(0, 1/3), giving exponential decay W(t) ≤ W(0)·e^μ_maxt = W(0)·e^−2t.

□

Proof II — Whitney A₁ curvature

IIFrom V(q) = q³ − 3q and the fold curvature

The fold at r = 1 is classified by the Whitney potential V(q) = q³ − 3q (Lean: P1a–P1d). Setting q = 1 + ρ, the gradient expands as:

Two coefficients are visible: the linear coefficient 6 (= V''(1), the Whitney A₁ curvature at the fold) and the quadratic coefficient A₁ = 3. The Gronwall radius of the associated gradient system ρ̇ = −V'(1+ρ) is:

The Gronwall radius equals the ratio of the transverse Lyapunov exponent to the Whitney curvature V''(1):

Geometrically: the basin radius is the ratio of how fast the linearised flow contracts (= |μ_max| = 2) to how quickly the Whitney fold curves away from the tangent plane (= V''(1) = 6). A sharper fold ⟹ smaller basin.

□

Proof III — Explicit ODE quadrature

IIIPartial fractions on ρ̇ = −ρ(1+ρ)(2+ρ)

Equation (★) is separable. Write:

Partial-fraction decomposition:

Integrating from 0 to t:

For small ρ₀, expand K at t = 0: K = √(ρ₀(2+ρ₀))/(1+ρ₀) ≈ √(2ρ₀) for ρ₀ → 0⁺. The decay time-scale is exactly 1 (rate = 1 = |μ_max|/2).

The threshold at which the quadratic correction to the exponential decay equals the leading-order contribution:

□

Proof IV — Contraction mapping (Picard–Banach)

IVThe period-T* Poincaré map is a contraction on B(0, 1/3)

Write the flow of (★) as Φ^t and define the Poincaré map P = Φ^T* where T* = 2π is the period of Γ. The mean-value theorem gives, for ρ₁, ρ₂ ∈ B(0, ε):

The variation equation along Φ^t(ρ₀) gives:

Integrating with Gronwall:

For P to be a contraction (|P'| < 1), need the exponent negative:

Within B(0, 1/3), the Poincaré map is a contraction with ratio at most e^{(−2 + 6·(1/3))·T*} = e⁰ = 1 (boundary), and strictly less for ε < 1/3. The fixed point ρ = 0 is therefore the unique attracting point of P in B(0, 1/3).

□

Proof V — Hamiltonian normal form at the fold

VNormal-form momentum jump Δp = μ_max·n constrains ε₀

Near the fold point q* = 1 (r = 1), the dm³ Hamiltonian (restricted to the transverse direction) takes the distributional form:

The fold singularity F introduces a momentum jump at ρ = ρ* via the distributional generator: p⁺ − p⁻ = μ_max·n where n = sign(ρ*). Symplectic preservation (Theorem S of Vol I) requires the area enclosed by the pre- and post-fold trajectories to be invariant under 2-form ω = dρ ∧ dp.

The largest ball around ρ = 0 within which the jump condition is compatible with ω-preservation is bounded by the condition that the jump size |Δp| = |μ_max| · |ρ*| does not exceed the local symplectic area divided by the period T*:

The upper bound on ε₀ comes from requiring the nonlinear correction to Δp to be small relative to the linear term: the quadratic term in the momentum satisfies |L₂|·ε₀² ≤ |μ_max|·ε₀/2, giving:

The Gronwall radius ε₀ = 1/3 is the largest perturbation for which the Hamiltonian normal form remains a valid description of the dynamics at the fold (nonlinear corrections small relative to linear term).

□

Proof VI — Contact-geometric Reeb flow

VIConformal dissipation factor of the Reeb field R_α

On the dm³ contact manifold (M, α) with contact form α = dz − r dθ, the limit cycle Γ is the Reeb orbit of R_α at r = 1. The transverse dynamics is governed by the contact Hamiltonian:

The contact Hamiltonian vector field X_H satisfies ι(X_H)dα = dH − (R_αH)α, giving the flow:

The conformal factor of the Reeb flow in the transverse direction is the function σ(ρ) = |ρ̇/ρ| = (1+ρ)(2+ρ). The Gronwall basin is where σ(ρ) exceeds its linearised value σ(0) = 2 by at most a factor of (1 + δ):

Geometrically: within B(0, 1/3), the Reeb flow contracts the transverse direction at a rate no more than 50% faster than the linearized rate. This is the contact-geometric meaning of the Gronwall stability radius.

□

Proof VII — Lean 4 formal verification

VIIMachine-checked via norm_num in Mathlib4

The following theorem appears in PrincipiaVol1.lean (AXLE repository, github.com/TOTOGT/AXLE), verified in Lean 4 / Mathlib4 with zero axioms beyond the Mathlib4 kernel:

The formula instantiated is ε₀ = |μ_max| / [2·(1 + sup‖Hess V‖)] with |μ_max| = 2 and sup‖Hess V‖ = 2, giving:

Additionally, the companion theorem noiseTolerance derives that the noise budget is τ·ε₀ = 2·(1/3) = 2/3, where τ = 2 is the embodiment threshold. The canonical triple (T*, μ_max, τ) = (2π, −2, 2) is machine-checked in the same file.

□

The seven proofs compared

Proofs I, II, VII give ε₀ = 1/3 exactly. Proofs III–VI give 1/3 at leading order; the exact Lyapunov basin extends to ε = (3−√5)/2 ≈ 0.382 (a 15% margin of safety above the Gronwall radius). This gap between the Gronwall radius and the true basin boundary is structurally identical to the analogous gap in the Tribonacci constant proofs (TOGT §3): the machine-checked value is the conservative lower bound, not the supremum of the actual basin.

Corollaries

Noise tolerance

With τ = 2 (embodiment threshold, Lean: canonicalTriple.tau) and ε₀ = 1/3:

Factor-of-3 prediction

The basin asymmetry theorem (Lean: basin_asymmetry) states 1/3 < 4/5. In the quantum-gravity application (chPsi), this reads: the gravitational decoherence time satisfies τ_grav < τ_dec/3, giving a factor-of-3 prediction distinguishable from the Penrose τ_grav < τ_dec bound by an order of magnitude.

Lean status summary (P3 family)