InjuryRiskCert
plain-language theorem explainer
InjuryRiskCert bundles five properties: the J-cost on the acute-to-chronic workload ratio vanishes at balance, remains nonnegative for positive loads, and the injury tip point satisfies 1 < phi < 1.9 inside the band (1.4, 1.9). Sports scientists applying Recognition Science to training-load data would cite it to link the Gabbett-Hulin ACWR threshold to the phi-ladder. The declaration is a direct structure definition that packages lemmas already proved in sibling declarations.
Claim. Let $acwrCost(a,c) := Jcost(a/c)$ and let $phi$ be the golden ratio. InjuryRiskCert is the structure asserting $acwrCost(w,w)=0$ for all nonzero $w$, $acwrCost(a,c)geq 0$ whenever $a>0$ and $c>0$, together with $0<phi$, $1<phi$, and $1.4<phi<1.9$.
background
In the Recognition Science treatment of athletic injury the acute:chronic workload ratio is mapped to J-cost by the definition acwrCost(acute,chronic) := Jcost(acute/chronic). The injury tip point is defined as phi, the self-similar fixed point forced by the unified forcing chain. Upstream cost_nonneg from ObserverForcing supplies the general nonnegativity of recognition cost, which is instantiated here for the ACWR function.
proof idea
This is a structure definition whose five fields are filled by direct references to sibling lemmas: acwrCost_at_balance supplies the zero-cost balance condition, acwrCost_nonneg supplies nonnegativity, and the three injuryTipPoint_* lemmas supply positivity, the strict inequality above 1, and membership in the open interval (1.4,1.9).
why it matters
The structure is instantiated by the downstream cert definition and shown inhabited by cert_inhabited. It supplies the structural theorem slot in the Sport.InjuryRiskFromJCost module, connecting the J-cost formalism to the phi-ladder (T6) and the eight-tick octave. The module doc states the falsifier explicitly: any large-N prospective cohort study placing the ACWR injury-risk inflection outside (1.4,1.9).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.