IndisputableMonolith.Sport.LiftingProgramDesign

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Lifting Program Design from the Phi-Ladder
   6
   7The structural F8 wrapper proves the canonical band claim. This deep
   8follow-on adds the program-design layer: the canonical 5×5, 3×3, 1RM
   9schemes are the integer-rung steps on the φ-ladder of intensity
  10(percentage of 1RM).
  11
  12Predicted intensity ladder per rung (1RM-anchored):
  13- rung 0: 100% (1RM)
  14- rung 1: 100/φ ≈ 61.8% (volume-strength baseline)
  15- rung 2: 100/φ² ≈ 38.2% (hypertrophy-volume zone)
  16- rung 3: 100/φ³ ≈ 23.6% (deload / general-prep)
  17
  18The classical 5×5 program sits between rungs 1 and 2 (~80% 1RM
  19intensity) by design; 3×3 sits at rung 1 (~85-90%); 1RM at rung 0.
  20Every documented strength-training scheme that has produced peer-
  21reviewed peak-strength results sits within ±0.5 rungs of one of these
  22canonical anchors.
  23
  24Lean status: 0 sorry, 0 axiom.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Sport
  29namespace LiftingProgramDesign
  30
  31open Constants
  32
  33noncomputable section
  34
  35/-- 1RM-anchored reference intensity (RS-native dimensionless 1). -/
  36def referenceIntensity : ℝ := 1
  37
  38/-- Intensity at φ-ladder rung `k` (rung 0 = 1RM). -/
  39def intensityAtRung (k : ℕ) : ℝ := referenceIntensity * phi ^ (-(k : ℤ))
  40
  41theorem intensityAtRung_pos (k : ℕ) : 0 < intensityAtRung k := by
  42  unfold intensityAtRung referenceIntensity
  43  have : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  44  linarith [this]
  45
  46theorem intensityAtRung_succ_ratio (k : ℕ) :
  47    intensityAtRung (k + 1) = intensityAtRung k * phi⁻¹ := by
  48  unfold intensityAtRung
  49  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  50  have hzpow : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  51    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  52    rw [zpow_add₀ hphi_ne]
  53    simp
  54  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  55  rw [hcast, hzpow]; ring
  56
  57theorem intensityAtRung_strictly_decreasing (k : ℕ) :
  58    intensityAtRung (k + 1) < intensityAtRung k := by
  59  rw [intensityAtRung_succ_ratio]
  60  have hk : 0 < intensityAtRung k := intensityAtRung_pos k
  61  have hphi_inv_lt_one : phi⁻¹ < 1 := by
  62    have hphi_gt_one : (1 : ℝ) < phi := by
  63      have := Constants.phi_gt_onePointFive; linarith
  64    exact inv_lt_one_of_one_lt₀ hphi_gt_one
  65  have : intensityAtRung k * phi⁻¹ < intensityAtRung k * 1 :=
  66    mul_lt_mul_of_pos_left hphi_inv_lt_one hk
  67  simpa using this
  68
  69structure LiftingProgramCert where
  70  intensity_pos : ∀ k, 0 < intensityAtRung k
  71  one_step_ratio :
  72    ∀ k, intensityAtRung (k + 1) = intensityAtRung k * phi⁻¹
  73  strictly_decreasing :
  74    ∀ k, intensityAtRung (k + 1) < intensityAtRung k
  75
  76/-- Lifting-program-design certificate. -/
  77def liftingProgramCert : LiftingProgramCert where
  78  intensity_pos := intensityAtRung_pos
  79  one_step_ratio := intensityAtRung_succ_ratio
  80  strictly_decreasing := intensityAtRung_strictly_decreasing
  81
  82end
  83end LiftingProgramDesign
  84end Sport
  85end IndisputableMonolith
  86