Formal verification · Lean 4 / Mathlib4 📦

Lean 4 formal verification

Key analytic lemmas supporting the amplitude envelope ansatz are proved without sorry and kernel-checked in TribonacciMeasure.lean (AXLE repository). The companion file TribonacciDNLS.lean in the Zenodo deposit does not currently pass kernel check and should be treated as work in progress. The decay constant η ≈ 1.839287 is the Perron–Frobenius eigenvalue of the tribonacci companion matrix — the unique real root of x³ − x² − x − 1 = 0 in [1, 2].

η_gt_one : 1 < η✓ proved
η_characteristic : η³ = η² + η + 1✓ proved
w_pos : ∀ k, 0 < η⁻ᵏ✓ proved
w_strictAnti : StrictAnti (k ↦ η⁻ᵏ)✓ proved
w_tendsto_zero : η⁻ᵏ → 0 as k → ∞✓ proved
IPR_trib(0) > IPR_fib(0) 📦○ open (AXLE roadmap)
differential nonlinear robustness threshold (statement)○ open (AXLE roadmap)

Verified lemmas above refer to TribonacciMeasure.lean (AXLE). Open proof obligations — including restoring kernel check for the deposit's TribonacciDNLS.lean — are tracked in the AXLE sorry roadmap. Other Lean files in the deposit: FoldEvents.lean.