fatigueThresholdCert
plain-language theorem explainer
fatigueThresholdCert packages the J-cost properties of the dimensionless stress ratio into a single certificate structure. Materials modelers working on cyclic loading would cite it to anchor the endurance limit inside the golden-section band. The definition is a direct structure constructor that supplies the five required fields from already-proved sibling lemmas.
Claim. Let $c(r)$ be the J-cost on the stress ratio $r$. The fatigue threshold certificate asserts $c(1)=0$, $c(r)=c(r^{-1})$ for all $r>0$, $c(r)≥0$ for all $r>0$, the endurance threshold lies in $(0.11,0.13)$, and the infinite-life and fatigue-failing regimes are disjoint.
background
The module treats fatigue as recognition cost accumulated on the dimensionless ratio $r$ = observed stress over yield stress. The J-cost function reaches its minimum at $r=1$ and is strictly positive for $r<1$, matching the physical observation that sub-yield cyclic loading still produces damage. FatigueThresholdCert is the structure whose fields are yield_zero, reciprocal_symm, cost_nonneg, threshold_band, and regimes_exclusive. Upstream, cost_nonneg states that the cost of any recognition event is non-negative, while endurance_threshold_band proves the threshold lies inside the canonical interval by direct substitution of the golden-ratio expression for J-cost.
proof idea
The definition constructs the FatigueThresholdCert structure by direct field assignment. yield_zero receives fatigueCost_zero_at_yield, reciprocal_symm receives fatigueCost_reciprocal_symm, cost_nonneg receives fatigueCost_nonneg, threshold_band receives endurance_threshold_band, and regimes_exclusive receives regimes_exclusive. Each assignment is a one-line wrapper that invokes the corresponding pre-proved lemma.
why it matters
The certificate certifies that the J-cost model on stress ratio reproduces the observed endurance band and the mutual exclusion of infinite-life and failing regimes, placing fatigue on the same footing as plaque vulnerability and magnetic reconnection inside the Recognition Science framework. It draws on the universal RS quantum described in the module documentation and on the non-negativity property of recognition cost. No downstream theorems yet consume the certificate, leaving open its use in quantitative life-prediction lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.