gapAt_pos'
plain-language theorem explainer
gapAt_pos' establishes that the predicted gap to the athletic asymptote stays strictly positive at every natural-number improvement step N. Analysts fitting successive world records to the phi-ladder decay invoke the result to guarantee the geometric sequence never reaches zero in finite steps. The term-mode proof unfolds the gap definition, invokes positivity of phi to a negative integer power, and closes by linear arithmetic.
Claim. $0 < g(N)$ for every natural number $N$, where the gap function is defined by $g(N) := 1 · ϕ^{-N}$ with reference gap normalized to unity.
background
The module supplies an explicit fitting layer on top of the structural athletic-record theorem. gapAt is defined locally as referenceGap multiplied by phi raised to the negative integer N, with referenceGap fixed at 1; the same pattern appears in the upstream PolarCodeGapFromPhi module. Constants supplies the positivity and ordering facts for phi. The module doc states that any sequence of records whose consecutive gap ratios deviate systematically from 1/phi would falsify the RS-ladder model of athletic limits.
proof idea
One-line wrapper that unfolds gapAt and referenceGap, asserts 0 < phi^(-(N:ℤ)) via zpow_pos applied to Constants.phi_pos, and finishes with linarith.
why it matters
The result is the positivity premise required by consecutive_gap_ratio, gapAt_strictly_decreasing, and the recordProgressionCert bundle. It therefore closes the positivity slot in the athletic-progression certificate that the module doc presents as the empirical test of the phi-decay law. The certificate in turn supports the claim that observed record sequences must track the geometric decay generated by the T6 self-similar fixed point or falsify the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.