FatigueThresholdCert
plain-language theorem explainer
The FatigueThresholdCert structure bundles five properties of the J-cost on stress ratio that certify the endurance limit separating infinite-life and finite-life regimes. Materials modelers working on cyclic loading would cite it to locate the golden-section threshold in the interval (0.11, 0.13). The definition is a direct record that assembles vanishing at yield, reciprocal symmetry, non-negativity, the numerical band, and regime exclusivity from sibling lemmas.
Claim. A fatigue threshold certificate is a record asserting that the per-cycle recognition cost on the dimensionless stress ratio $r$ vanishes at the yield point, satisfies $C(r)=C(r^{-1})$ for $r>0$, is non-negative for $r>0$, that the golden-section endurance threshold lies in $(0.11,0.13)$, and that the infinite-life regime (cost below threshold) and fatigue-failure regime (cost at or above threshold) are disjoint.
background
In the Recognition Science treatment of materials fatigue the dimensionless stress ratio $r$ is observed stress divided by yield stress. The per-cycle cost is the J-cost function applied to $r$, which reaches its global minimum of zero at $r=1$. The endurance threshold is defined as the J-cost evaluated at the golden ratio, and the infinite-life regime holds when this cost lies strictly below the threshold while fatigue failure holds when it meets or exceeds the threshold.
proof idea
The structure is defined by direct record construction. Its five fields are populated by prior lemmas already proved in the same module: yield zero from fatigueCost_zero_at_yield, reciprocal symmetry from fatigueCost_reciprocal_symm, non-negativity from fatigueCost_nonneg, the numerical band from endurance_threshold_band, and regime exclusivity from regimes_exclusive. No further tactics are applied.
why it matters
This certificate supplies the bundled properties required by the downstream fatigueThresholdCert definition. It realizes the J-uniqueness and phi fixed-point steps of the forcing chain in the concrete setting of cyclic stress, extending the universal RS quantum (already applied to plaque vulnerability, ignition, and magnetic reconnection) to structural engineering. The construction closes the scaffolding for the endurance limit across the eight-tick octave framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.