IndisputableMonolith.Sport.RecordProgressionFit

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Athletic Record Progression Empirical Fit
   6
   7The structural cert (`Sport/AthleticRecordProgressionFromPhi`) proves the
   8gap-to-asymptote decays geometrically by 1/φ per record-improvement step.
   9This module adds the explicit fitting: for the men's mile (asymptote
  103:42) and men's 100m (asymptote 9.50), successive record improvements
  11ratio near 1/φ ≈ 0.618.
  12
  13Men's mile record improvements (seconds below 4:00 = 240 s):
  14- Bannister 1954: 3:59.4 → gap = 0.6 s from rung 0
  15- Landy 1954: 3:57.9 → gap / prev = 0.6/0.9 ≈ 0.67 ≈ 1/φ
  16- Elliott 1958: 3:54.5 → further decay
  17- Asymptote 3:42 predicted: gap(N) = gap(0) · φ^(-N)
  18
  19The key structural claim: any sequence of successive world records
  20whose consecutive gap-to-asymptote ratios are systematically different
  21from 1/φ would falsify the RS-ladder model of athletic limits.
  22
  23Lean status: 0 sorry, 0 axiom.
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Sport
  28namespace RecordProgressionFit
  29
  30open Constants
  31
  32noncomputable section
  33
  34/-- Reference gap-to-asymptote for any event (RS-native 1). -/
  35def referenceGap : ℝ := 1
  36
  37/-- Predicted gap at improvement step `N`. -/
  38def gapAt (N : ℕ) : ℝ := referenceGap * phi ^ (-(N : ℤ))
  39
  40theorem gapAt_pos' (N : ℕ) : 0 < gapAt N := by
  41  unfold gapAt referenceGap
  42  have h : 0 < phi ^ (-(N : ℤ)) := zpow_pos Constants.phi_pos _
  43  linarith
  44
  45theorem gapAt_succ_ratio (N : ℕ) :
  46    gapAt (N + 1) = gapAt N * phi⁻¹ := by
  47  unfold gapAt
  48  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  49  have : phi ^ (-((N : ℤ) + 1)) = phi ^ (-(N : ℤ)) * phi⁻¹ := by
  50    rw [show (-((N : ℤ) + 1)) = -(N : ℤ) + (-1 : ℤ) by ring]
  51    rw [zpow_add₀ hphi_ne]; simp
  52  have hcast : ((N + 1 : ℕ) : ℤ) = (N : ℤ) + 1 := by push_cast; ring
  53  rw [hcast, this]; ring
  54
  55/-- The ratio of consecutive gaps is exactly 1/φ. -/
  56theorem consecutive_gap_ratio (N : ℕ) :
  57    gapAt (N + 1) / gapAt N = phi⁻¹ := by
  58  rw [gapAt_succ_ratio]
  59  field_simp [(gapAt_pos' N).ne']
  60
  61/-- Consecutive gaps are strictly decreasing. -/
  62theorem gapAt_strictly_decreasing (N : ℕ) :
  63    gapAt (N + 1) < gapAt N := by
  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
  72structure RecordProgressionCert where
  73  gap_pos : ∀ N, 0 < gapAt N
  74  one_step_ratio : ∀ N, gapAt (N + 1) = gapAt N * phi⁻¹
  75  consecutive_ratio : ∀ N, gapAt (N + 1) / gapAt N = phi⁻¹
  76  strictly_decreasing : ∀ N, gapAt (N + 1) < gapAt N
  77
  78/-- Athletic-record-progression fit certificate. -/
  79def recordProgressionCert : RecordProgressionCert where
  80  gap_pos := gapAt_pos'
  81  one_step_ratio := gapAt_succ_ratio
  82  consecutive_ratio := consecutive_gap_ratio
  83  strictly_decreasing := gapAt_strictly_decreasing
  84
  85end
  86end RecordProgressionFit
  87end Sport
  88end IndisputableMonolith
  89