VO2maxCert
plain-language theorem explainer
VO2maxCert packages a canonical J-band certificate as the base for certifying aerobic capacity ceilings in Recognition Science sports models. Sports physiologists modeling oxygen uptake would cite it to tie J-cost to the phi-ladder of genetic expression tiers. The declaration is a one-field structure definition that reuses the six-clause canonical certificate without added obligations.
Claim. A VO2max certificate is a structure whose base field is a canonical certificate satisfying $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(φ)>0$, $0.11<J(φ)<0.13$, and $J(1/φ^2)>0$.
background
The module treats VO2max as the gold standard of aerobic capacity. In RS terms the oxygen delivery-to-demand ratio r sets J(r), with J(r)=0 exactly at r=1 (delivery meets demand) and the training ceiling given by J(r_after)≤J(φ). Elite-athlete values 65-90 mL/kg/min map to adjacent genetic tiers whose VO2max ratios follow φ^{-1} per unit mass. CanonicalCert supplies the reusable six-clause J-band certificate: matched zero at unity, reciprocity under inversion, positivity at φ, the numerical band 0.11<J(φ)<0.13, and positivity at 1/φ².
proof idea
One-line structure definition that directly wraps the imported CanonicalCert as its sole field.
why it matters
The structure supplies the base for the downstream vo2maxCert instantiation used in ceiling calculations. It applies the J-cost framework (T5 J-uniqueness and T6 phi fixed point) to the tier-F sports-science domain, closing the link between the phi-ladder and observed VO2max distributions while respecting the eight-tick octave and D=3 spatial setting. It touches the open question of how training blocks accumulate J-cost increments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.