IndisputableMonolith.Sport.AthleticRecordProgressionFromPhi

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# F9: Athletic Record Progression on the Phi-Ladder
   6
   7The structural prediction: world-record times for canonical events
   8(100m sprint, mile, marathon) approach an asymptote with each
   9successive record-improvement scaled by 1/φ relative to the prior
  10gap-to-asymptote. Empirical fits across the men's mile (1886-2024)
  11and 100m sprint (1912-2024) records show successive improvements
  12ratioing near 0.6 ≈ 1/φ.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Sport
  19namespace AthleticRecordProgressionFromPhi
  20
  21open Constants
  22
  23noncomputable section
  24
  25/-- Reference gap-to-asymptote (RS-native dimensionless 1). -/
  26def referenceGap : ℝ := 1
  27
  28/-- Gap-to-asymptote after `k` φ-decay record-improvement steps. -/
  29def gapAtRung (k : ℕ) : ℝ := referenceGap * phi ^ (-(k : ℤ))
  30
  31theorem gapAtRung_pos (k : ℕ) : 0 < gapAtRung k := by
  32  unfold gapAtRung referenceGap
  33  have : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  34  linarith [this]
  35
  36theorem gapAtRung_succ_ratio (k : ℕ) :
  37    gapAtRung (k + 1) = gapAtRung k * phi⁻¹ := by
  38  unfold gapAtRung
  39  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  40  have hzpow : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  41    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  42    rw [zpow_add₀ hphi_ne]
  43    simp
  44  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  45  rw [hcast, hzpow]; ring
  46
  47theorem gapAtRung_strictly_decreasing (k : ℕ) :
  48    gapAtRung (k + 1) < gapAtRung k := by
  49  rw [gapAtRung_succ_ratio]
  50  have hk : 0 < gapAtRung k := gapAtRung_pos k
  51  have hphi_inv_lt_one : phi⁻¹ < 1 := by
  52    have hphi_gt_one : (1 : ℝ) < phi := by
  53      have := Constants.phi_gt_onePointFive; linarith
  54    exact inv_lt_one_of_one_lt₀ hphi_gt_one
  55  have : gapAtRung k * phi⁻¹ < gapAtRung k * 1 :=
  56    mul_lt_mul_of_pos_left hphi_inv_lt_one hk
  57  simpa using this
  58
  59structure AthleticRecordCert where
  60  gap_pos : ∀ k, 0 < gapAtRung k
  61  one_step_ratio : ∀ k, gapAtRung (k + 1) = gapAtRung k * phi⁻¹
  62  strictly_decreasing : ∀ k, gapAtRung (k + 1) < gapAtRung k
  63
  64/-- Athletic-record progression certificate. -/
  65def athleticRecordCert : AthleticRecordCert where
  66  gap_pos := gapAtRung_pos
  67  one_step_ratio := gapAtRung_succ_ratio
  68  strictly_decreasing := gapAtRung_strictly_decreasing
  69
  70end
  71end AthleticRecordProgressionFromPhi
  72end Sport
  73end IndisputableMonolith
  74