athleticRecordCert
plain-language theorem explainer
The athleticRecordCert definition assembles a certificate asserting that gaps to the athletic record asymptote remain positive, contract by the factor phi inverse at each rung, and decrease strictly. Modelers of sports performance records would reference it when embedding phi-ladder scaling into empirical progression data. Construction proceeds by direct field assignment to three supporting theorems on the gap function.
Claim. Let $g : ℕ → ℝ$ denote the gap to the record asymptote at rung $k$. The certificate asserts $g(k) > 0$, $g(k+1) = g(k) ⋅ φ^{-1}$, and $g(k+1) < g(k)$ for every natural number $k$.
background
In the Recognition Science treatment of athletic records, the phi-ladder models successive improvements as geometric contractions toward an asymptote. The gapAtRung function measures the remaining distance to this limit at rung k, defined via referenceGap scaled by negative powers of phi. The module F9 predicts that record times for events such as the mile and 100 m sprint improve with ratios near 1/φ ≈ 0.618.
proof idea
The definition constructs an AthleticRecordCert instance by assigning each required field to the corresponding theorem: gap_pos receives gapAtRung_pos, one_step_ratio receives gapAtRung_succ_ratio, and strictly_decreasing receives gapAtRung_strictly_decreasing. No additional reasoning is needed beyond these prior results.
why it matters
This certificate supplies the structural properties required by the athleticRecordCert definition in the Sports.AthleticRecordAsymptote module, which further incorporates improvement positivity and phi5-band constraints. It realizes the F9 prediction that record progressions follow the phi-scaling derived from the self-similar fixed point in the forcing chain. The construction closes the local scaffolding for the sport domain within the broader Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.