gapAt
plain-language theorem explainer
GapAt(N) assigns the value phi to the power of minus N, with reference gap normalized to 1. Researchers fitting athletic record sequences to the RS phi-ladder cite this to express the predicted distance to the asymptotic limit after N improvements. The definition is a direct unfolding of the geometric decay law already fixed in the upstream referenceGap constants.
Claim. The predicted gap after $N$ record-improvement steps is $1 · ϕ^{-N}$, where $ϕ$ is the golden ratio and the reference gap-to-asymptote is normalized to the dimensionless unit 1.
background
The module supplies an explicit fitting function for athletic record progressions under the Recognition Science model. The structural certificate in AthleticRecordProgressionFromPhi establishes that the gap-to-asymptote decays geometrically by the factor 1/ϕ per successive record improvement. This definition simply applies that decay to an arbitrary step count N, using the same referenceGap = 1 that appears in the polar-code and sport sibling modules.
proof idea
One-line definition that directly multiplies the upstream referenceGap constant by phi raised to the negative integer N.
why it matters
The definition supplies the concrete gap function required by consecutive_gap_ratio, gapAt_pos', and gapAt_strictly_decreasing inside the same module, and by the PolarCodeCert structure in the information layer. It completes the explicit fitting step for the athletic-record model whose key claim is that any systematic deviation of consecutive ratios from 1/ϕ would falsify the RS-ladder description of performance limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.