cert
plain-language theorem explainer
The declaration assembles a certificate that the ACWR cost function vanishes at equal acute and chronic loads, stays non-negative, and places the injury tip point inside the empirical risk band. Sports scientists applying recognition-cost models to training load data would cite it to embed the golden-ratio threshold inside the J-cost formalism. The construction is a direct structure instance that pulls five sibling results into the InjuryRiskCert record.
Claim. The injury-risk certificate asserts that the ACWR cost function satisfies $acwrCost(w,w)=0$ for all $w≠0$, $acwrCost(a,c)≥0$ whenever $a>0$ and $c>0$, and that the tip point obeys $0<tip<∞$, $1<tip$, and $1.4<tip<1.9$, where the tip equals the golden ratio.
background
The module models athletic injury risk via the acute-to-chronic workload ratio (ACWR) expressed as a J-cost. The structure InjuryRiskCert packages five properties: zero cost at load balance, non-negativity of cost for positive loads, and three statements locating the tip point. Upstream, cost_nonneg states that the cost of any recognition event is non-negative, while acwrCost_at_balance shows the cost vanishes when the ratio equals one by reduction to Jcost_unit0. The tip point is identified with φ by injuryTipPoint_gt_one and injuryTipPoint_in_band, the latter confirming the interval (1.4,1.9) matches observed inflection data.
proof idea
The definition is a one-line structure constructor that supplies the five fields of InjuryRiskCert directly from sibling declarations: cost_at_balance from acwrCost_at_balance, cost_nonneg from acwrCost_nonneg, tip_pos from injuryTipPoint_pos, tip_gt_one from injuryTipPoint_gt_one, and tip_in_band from injuryTipPoint_in_band.
why it matters
This definition completes the structural theorem for the Sport module, supplying the concrete certificate whose existence is asserted in the module documentation. It links the J-cost non-negativity result from ObserverForcing to the empirical ACWR threshold, fixing the tip at φ from the forcing chain (T5–T6). The construction touches the open falsifier stated in the module: any large-N cohort study placing the ACWR inflection outside (1.4,1.9) would refute the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.