consecutive_gap_ratio
Successive gaps to the asymptotic limit in the athletic record model satisfy a fixed ratio of the inverse golden ratio. Analysts fitting track records to the phi-ladder would cite this to confirm the predicted geometric decay. The term proof rewrites the ratio via the successor lemma then simplifies the field expression after confirming positivity of the gap.
claimLet $g(N)$ denote the gap to the asymptotic record limit at improvement step $N$. Then $g(N+1)/g(N) = phi^{-1}$ for every natural number $N$.
background
The gap function is defined by $g(N) = referenceGap * phi^{-N}$. This module supplies the explicit fitting layer for athletic records, showing that successive improvements decay geometrically by $phi^{-1}$ per step, as already proved structurally for the men's mile and 100 m. The upstream gapAt_succ_ratio in PolarCodeGapFromPhi establishes the identical relation for polar-code gaps, which is mirrored verbatim here.
proof idea
The proof applies the successor ratio theorem to replace the left-hand side, then invokes field_simp using the positivity fact gapAt_pos' N.
why it matters in Recognition Science
This supplies the consecutive_ratio field inside recordProgressionCert, the top-level certificate for athletic-record fits. It implements the geometric decay required by the Recognition Science phi-ladder, consistent with the self-similar fixed point and T5 J-uniqueness. No open scaffolding remains.
scope and limits
- Does not fix the numerical value of the reference gap.
- Does not test the model on sports outside track and field.
- Does not prove that phi is the only possible decay base.
formal statement (Lean)
56theorem consecutive_gap_ratio (N : ℕ) :
57 gapAt (N + 1) / gapAt N = phi⁻¹ := by
proof body
Term-mode proof.
58 rw [gapAt_succ_ratio]
59 field_simp [(gapAt_pos' N).ne']
60
61/-- Consecutive gaps are strictly decreasing. -/