AthleticRecordCert
plain-language theorem explainer
AthleticRecordCert packages positivity of the phi-ladder improvement sequence, a lower bound on scaled initial records, and the numerical interval 10 < phi^5 < 12. Researchers fitting sprint-record decay to Recognition Science scaling would cite the certificate when checking consistency with historical 100 m data. The structure is assembled by direct reference to the improvementAtRung positivity lemma together with the two sibling facts on boundedness and the phi^5 band.
Claim. A certificate consists of positivity $0 < I(k,n)$ for all natural numbers $k,n$ where $I(k,n) = phi^k / phi^n$, the implication that every positive initial record $r_0$ satisfies $r_0 / phi^5 > 0$, and the band condition $10 < phi^5 < 12$.
background
The module treats athletic-record asymptotes via the phi-ladder. Upstream, improvementAtRung is defined by improvementAtRung(k,n) := phi^k / phi^n and described as a phi-ladder improvement sequence at scale 1/n per rung. The sibling structure AthleticRecordCert from AthleticRecordProgressionFromPhi supplies the parallel certificate with gap positivity, one-step ratio equal to phi^{-1}, and strict decrease, carrying the doc-comment 'Athletic-record progression certificate.'
proof idea
The declaration is a structure definition that directly bundles the three fields. It obtains the positivity witness from the upstream lemma improvementAtRung_pos, the boundedness witness from record_bounded_below, and the band witness from phi5_in_band. No tactics or reductions are performed; the structure is instantiated by naming the component lemmas.
why it matters
The certificate supplies the interface instantiated by athleticRecordCert in both the local module and the Sport.AthleticRecordProgressionFromPhi sibling. It closes the F9 claim by verifying the phi^5 band and improvement positivity, connecting to the self-similar fixed point phi and the eight-tick periodicity in the T0-T8 forcing chain. The construction enables downstream checks that observed record ratios lie on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.