gapAt_strictly_decreasing
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of the reference gap from first principles.
- Does not incorporate measurement uncertainty from actual athletic timing data.
- Does not extend the decay law to non-individual or team-based events.
- Does not prove that the sequence converges to the stated asymptote.
formal statement (Lean)
62theorem gapAt_strictly_decreasing (N : ℕ) :
63 gapAt (N + 1) < gapAt N := by
proof body
Term-mode proof.
64 rw [gapAt_succ_ratio]
65 have hk : 0 < gapAt N := gapAt_pos' N
66 have hphi_inv_lt_one : phi⁻¹ < 1 :=
67 inv_lt_one_of_one_lt₀ (by have := Constants.phi_gt_onePointFive; linarith)
68 have : gapAt N * phi⁻¹ < gapAt N * 1 :=
69 mul_lt_mul_of_pos_left hphi_inv_lt_one hk
70 simpa using this
71