recordProgressionCert
plain-language theorem explainer
The recordProgressionCert definition assembles a certificate verifying that athletic record gaps decay geometrically with ratio 1/φ per successive improvement. Sports analysts testing the Recognition Science phi-ladder against data for the mile or 100m would cite it to confirm the predicted decay. It is a direct structure constructor that populates RecordProgressionCert from four sibling lemmas on positivity, exact ratio, and monotonicity.
Claim. Let $gapAt(N)$ denote the gap to the performance asymptote after $N$ record improvements and let $phi$ be the golden ratio. The definition recordProgressionCert is the structure asserting $forall N, 0 < gapAt(N)$, $forall N, gapAt(N+1) = gapAt(N) cdot phi^{-1}$, $forall N, gapAt(N+1)/gapAt(N) = phi^{-1}$, and $forall N, gapAt(N+1) < gapAt(N)$.
background
In the Sport.RecordProgressionFit module the gapAt function measures the remaining distance to the predicted asymptotic limit for an athletic event, expressed as a geometric sequence in powers of phi. The RecordProgressionCert structure packages four properties: positivity of all gaps, the one-step multiplicative decay by phi inverse, the explicit ratio equality, and strict monotonic decrease. The module documentation states that any sequence of successive world records whose consecutive gap-to-asymptote ratios differ systematically from 1/φ would falsify the RS-ladder model of athletic limits.
proof idea
The definition recordProgressionCert is a direct structure constructor that assigns the four fields of RecordProgressionCert to the corresponding sibling theorems: gap_pos to gapAt_pos', one_step_ratio to gapAt_succ_ratio, consecutive_ratio to consecutive_gap_ratio, and strictly_decreasing to gapAt_strictly_decreasing. The upstream gapAt_succ_ratio lemma supplies the multiplicative step by unfolding gapAt and applying the ring identity for the exponent shift.
why it matters
This definition supplies the concrete certificate for the empirical fit of athletic record progressions to the phi-ladder predicted by Recognition Science. It directly implements the structural claim that gap-to-asymptote decays geometrically by 1/φ per record-improvement step, with explicit examples for the men's mile (asymptote 3:42) and 100m (9.50). Although currently unused downstream, it closes the fitting interface for testing the T6 phi fixed point against sports data. An open question is whether the same ladder applies uniformly across all track and field events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.