IsFatigueFailing
plain-language theorem explainer
Materials engineers analyzing cyclic stress in alloys cite the predicate to mark the regime where per-cycle J-cost on the stress ratio meets or exceeds the golden-section endurance threshold. The definition directly compares the pre-set EnduranceThreshold to fatigueCost r. It is introduced without additional lemmas as the boundary condition for finite-life behavior in the Recognition Science model of fatigue.
Claim. A stress ratio $r$ satisfies the fatigue failure condition when $J(φ) ≤ J(r)$, where $J$ is the recognition cost function and $φ$ is the golden ratio.
background
The module treats fatigue as accumulation of recognition cost under cyclic loading, with $r$ defined as observed stress over yield stress. The J-cost function from the Cost module is applied directly to $r$ for the per-cycle cost, and to $φ$ for the endurance threshold. This places the fatigue limit at the same $J(φ)$ quantum used for other RS thresholds such as plaque vulnerability and magnetic reconnection.
proof idea
The declaration is a one-line definition that sets the predicate to the proposition EnduranceThreshold ≤ fatigueCost r. It relies on the definitions of EnduranceThreshold as Cost.Jcost phi and fatigueCost as Cost.Jcost r, with no further reduction or lemmas required.
why it matters
This predicate feeds the mutual-exclusivity theorem regimes_exclusive and the certification structure FatigueThresholdCert, which records the threshold band 0.11 < EnduranceThreshold < 0.13. It implements the fatigue indicator in the universal RS quantum that spans structural engineering, combustion, and plasma physics, consistent with the J-uniqueness and phi fixed-point steps in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.