gapAt_strictly_decreasing
plain-language theorem explainer
Consecutive gaps in the athletic record progression model decay strictly. Researchers fitting world records to the phi-ladder cite this to confirm monotonic improvement toward the asymptote. The proof rewrites the target via the successor ratio, invokes positivity of the current gap, and applies the bound phi greater than 1.5 to obtain the strict inequality by left multiplication.
Claim. For every natural number $N$, $g(N+1) < g(N)$, where the gap function is $g(N) = r_0 · ϕ^{-N}$ and $r_0$ is the reference gap to the asymptote.
background
The module supplies an explicit fit of athletic records to the Recognition Science phi-ladder. Successive record improvements are modeled by gaps that shrink geometrically by the factor $ϕ^{-1}$ at each step. The gapAt definition in this module is identical to the one imported from PolarCodeGapFromPhi: referenceGap times phi raised to minus the step index.
proof idea
Applies the successor-ratio lemma to replace the target inequality with a product involving phi inverse. Uses the positivity theorem gapAt_pos' to obtain a positive multiplier, invokes phi_gt_onePointFive to deduce that phi inverse is less than one, then applies the left-multiplication inequality for positive reals and simplifies.
why it matters
The result is bundled directly into the recordProgressionCert definition, which assembles the full certificate for the athletic-record fit. It supplies the strictly-decreasing clause required by the geometric-decay claim in the module documentation. The surrounding framework treats systematic deviation from the 1/phi ratio as a potential falsifier of the phi-ladder model for performance limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.