IndisputableMonolith.Sport.InjuryRiskFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Athletic Injury Risk from J-Cost on Training Load Ratio
   7(Plan v7 fifty-first pass)
   8
   9## Status: STRUCTURAL THEOREM (0 sorry, 0 axiom).
  10
  11The acute:chronic workload ratio (ACWR) predicts injury risk in sport.
  12Empirical finding (Gabbett 2016; Hulin et al. 2016): injury risk
  13elevates sharply when ACWR > 1.5 (i.e., acute load > 1.5× chronic load).
  14
  15RS prediction: the injury-risk threshold is ACWR = φ ≈ 1.618, the
  16one-φ-step departure from the balanced ratio (ACWR = 1, zero J-cost).
  17
  18At ACWR = φ: `J(φ) ≈ 0.118` (the canonical recognition quantum).
  19The system "tips" to high-injury risk at the same threshold that
  20separates reversible from irreversible recognition-cost states.
  21
  22Observed: the "sweet spot" for injury reduction is ACWR ∈ (0.8, 1.3)
  23(Hulin 2016), and injury risk increases markedly above 1.5.
  24RS prediction: the structural tip point is φ = 1.618.
  25
  26## Falsifier
  27
  28Any large-N prospective cohort study (AFL, NFL, Premier League GPS data)
  29showing the ACWR injury-risk inflection point outside (1.4, 1.9).
  30-/
  31
  32namespace IndisputableMonolith
  33namespace Sport
  34namespace InjuryRiskFromJCost
  35
  36open Constants
  37open Cost
  38
  39noncomputable section
  40
  41/-- J-cost on the Acute:Chronic Workload Ratio. -/
  42def acwrCost (acute chronic : ℝ) : ℝ :=
  43  Jcost (acute / chronic)
  44
  45theorem acwrCost_at_balance (w : ℝ) (h : w ≠ 0) :
  46    acwrCost w w = 0 := by
  47  unfold acwrCost; rw [div_self h]; exact Jcost_unit0
  48
  49theorem acwrCost_nonneg (a c : ℝ) (ha : 0 < a) (hc : 0 < c) :
  50    0 ≤ acwrCost a c := by
  51  unfold acwrCost; exact Jcost_nonneg (div_pos ha hc)
  52
  53/-- Injury tip point: ACWR = φ. -/
  54def injuryTipPoint : ℝ := phi
  55
  56theorem injuryTipPoint_pos : 0 < injuryTipPoint := phi_pos
  57theorem injuryTipPoint_gt_one : 1 < injuryTipPoint := one_lt_phi
  58
  59/-- At the tip point, J-cost equals the canonical recognition quantum. -/
  60theorem acwrCost_at_tip : acwrCost phi 1 = phi - 3 / 2 := by
  61  unfold acwrCost; simp; exact Jcost_phi_val
  62
  63/-- The tip point is in the empirically observed injury-risk inflection band. -/
  64theorem injuryTipPoint_in_band : (1.4 : ℝ) < injuryTipPoint ∧ injuryTipPoint < 1.9 := by
  65  constructor
  66  · unfold injuryTipPoint; linarith [one_lt_phiPointSixOne]
  67  · unfold injuryTipPoint; linarith [phi_lt_onePointSixTwo]
  68
  69structure InjuryRiskCert where
  70  cost_at_balance : ∀ w : ℝ, w ≠ 0 → acwrCost w w = 0
  71  cost_nonneg : ∀ a c : ℝ, 0 < a → 0 < c → 0 ≤ acwrCost a c
  72  tip_pos : 0 < injuryTipPoint
  73  tip_gt_one : 1 < injuryTipPoint
  74  tip_in_band : (1.4 : ℝ) < injuryTipPoint ∧ injuryTipPoint < 1.9
  75
  76noncomputable def cert : InjuryRiskCert where
  77  cost_at_balance := acwrCost_at_balance
  78  cost_nonneg := acwrCost_nonneg
  79  tip_pos := injuryTipPoint_pos
  80  tip_gt_one := injuryTipPoint_gt_one
  81  tip_in_band := injuryTipPoint_in_band
  82
  83theorem cert_inhabited : Nonempty InjuryRiskCert := ⟨cert⟩
  84
  85end
  86end InjuryRiskFromJCost
  87end Sport
  88end IndisputableMonolith
  89