RecordProgressionCert
plain-language theorem explainer
RecordProgressionCert bundles positivity, geometric decay by phi inverse, explicit ratio equality, and strict decrease for the gapAt sequence. A sports data analyst or RS modeler would cite it when certifying that successive athletic record gaps follow the phi-ladder prediction toward an asymptote. The structure is a definition whose fields are populated downstream by direct application of four module lemmas.
Claim. A certificate asserting that the gap-to-asymptote function obeys $0 < gapAt(N)$ for all natural numbers $N$, the recurrence $gapAt(N+1) = gapAt(N) · ϕ^{-1}$, the ratio $gapAt(N+1)/gapAt(N) = ϕ^{-1}$, and the inequality $gapAt(N+1) < gapAt(N)$.
background
The module models athletic record progression by gaps to an empirical asymptote that shrink geometrically with each improvement. gapAt N is defined as referenceGap multiplied by phi raised to minus N, adopting the same phi-ladder construction used for gap-to-capacity in the LDPC and Polar code modules. The module documentation states that any sequence of world records whose consecutive gap ratios differ systematically from 1/phi would falsify the RS-ladder model of athletic limits.
proof idea
RecordProgressionCert is a structure definition whose four fields state the required properties of gapAt. No internal tactics or reductions occur; verification is supplied downstream when recordProgressionCert is constructed by applying the lemmas gapAt_pos', gapAt_succ_ratio, consecutive_gap_ratio, and gapAt_strictly_decreasing.
why it matters
RecordProgressionCert supplies the certified properties that recordProgressionCert instantiates to confirm geometric decay in athletic records. It operationalizes the module claim that record gaps follow the phi inverse ratio, aligning with the self-similar fixed point phi in the forcing chain. The construction closes the empirical fit section by providing a Lean object usable for consistency checks against observed data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.