gapAt_succ_ratio
plain-language theorem explainer
The gap function obeys the recurrence gapAt(N+1) = gapAt(N) * phi^{-1} for every natural number N. Athletic record modelers and polar-code analysts cite this to establish exact geometric decay of residuals to the asymptote. The proof unfolds the definition, invokes phi non-zero, shifts the integer exponent by ring arithmetic, and closes with a cast and ring tactic.
Claim. For every natural number $n$, the gap function satisfies $g(n+1) = g(n) · ϕ^{-1}$, where $g$ denotes gapAt and $ϕ$ is the golden ratio.
background
Within the Sport module the function gapAt(N) measures the residual distance from the current athletic record to its predicted asymptotic limit, with the structural claim that these residuals form a geometric sequence on the phi-ladder. The module imports Constants for the value of phi and draws on PhiForcingDerived for the underlying J-cost and self-similar scaling. Upstream, phi_ne_zero supplies the non-vanishing fact required for exponent arithmetic, while LedgerFactorization and SpectralEmergence furnish the discrete-tier background that forces the 1/phi ratio.
proof idea
The tactic proof begins by unfolding gapAt to expose the explicit power phi^(-(N+1)). It obtains phi ≠ 0 from Constants.phi_ne_zero, rewrites the exponent as -(N) + (-1) and applies zpow_add₀, then uses a push_cast ring lemma to equate the natural-number increment with the integer one. The final ring tactic closes the equality.
why it matters
This one-step recurrence supplies the ratio axiom for RecordProgressionCert in the same module and for polarCodeCert in Information.PolarCodeGapFromPhi; both certificates are then used to certify geometric decay in athletic and coding contexts. It directly instantiates the self-similar fixed-point property of phi (T6) inside the empirical record model, confirming that systematic departure from the 1/phi ratio would falsify the RS-ladder prediction for performance limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.