referenceGap
plain-language theorem explainer
The reference gap-to-asymptote is fixed at the dimensionless value 1 in RS-native units to initialize geometric decay sequences for athletic records. Researchers fitting successive world records to the phi-ladder, such as mile or 100 m progressions, would cite it as the rung-0 starting point before each improvement multiplies the gap by 1/φ. The definition is a direct constant assignment with no computation or hypotheses.
Claim. The reference gap-to-asymptote is defined as $1$.
background
In the Sport.RecordProgressionFit module the gap-to-asymptote is the remaining distance from a current record to the predicted asymptotic limit of an event. The module states that this quantity decays geometrically by the factor 1/φ at each record-improvement step, with explicit examples for the men's mile (asymptote 3:42) and men's 100 m (asymptote 9.50). Upstream results supply the same reference value in PolarCodeGapFromPhi.referenceGap and the logarithmic gap expression in RSBridge.Anchor.gap, which is F(Z) = ln(1 + Z/φ) / ln(φ).
proof idea
The definition is a direct assignment of the real number 1.
why it matters
This supplies the initial rung for gapAtRung and gapAt in AthleticRecordProgressionFromPhi and PolarCodeGapFromPhi, which implement the geometric decay gapAt(k) = referenceGap · φ^(-k). It anchors the structural claim that consecutive gap ratios near 1/φ support the RS-ladder model of athletic limits and connects to the self-similar fixed point phi (T6) in the forcing chain. The module notes that systematic deviation from this ratio would falsify the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.