Materials Fatigue Threshold From Jcost Fatigue Cost Pos Off Yield

The fatigue cost theorem

Materials fatigue is the failure of metals and polymers under repeated loading at stresses far below the static yield point. The classical picture is the Wöhler curve, also called the S-N curve: a plot of stress amplitude against the number of cycles to failure. For many steels the curve levels off at an endurance limit, roughly half the yield stress, below which the material can in principle survive an infinite number of cycles. The empirical laws of Basquin and Coffin-Manson describe the finite-life portion of that curve.

In the Recognition Science framework, fatigue is modeled by a recognition cost, a discrete record of the energy price the material pays for each deviation from its baseline state. The baseline is the yield stress, where the cost is zero. The framework defines a dimensionless stress ratio r, the observed stress divided by the yield stress. At r = 1 the material sits exactly at yield and pays nothing. The theorem fatigueCost_pos_off_yield proves that for any positive ratio other than 1, the per-cycle fatigue cost is strictly positive. In plain language: any departure from the yield baseline, whether above or below, forces the material to pay a positive price each cycle. The cost is symmetric in the ratio and its reciprocal, so operating at half the yield stress costs the same as operating at twice it.

The framework then identifies the endurance limit with a specific value of this cost function. The golden-section threshold J(φ) lies in the band between 0.11 and 0.13. Below that threshold the framework defines the infinite-life regime; at or above it, the fatigue-failing regime. A second theorem proves these two regimes are mutually exclusive: a material cannot be both in infinite life and failing at the same stress ratio. The framework's library also assembles these results into a single certificate, a packaged proof object that records all five properties at once.

What the theorem does not claim is just as important. It does not prove that any real material actually has an endurance limit at exactly this threshold. The framework models the cost, and the theorem proves properties of that model. Whether the model matches measured fatigue data for a specific steel or polymer is an empirical question, not a proved result. The theorem also does not say that sub-yield operation is always safe; it says only that the modeled cost is positive. Real fatigue depends on many factors the model does not include, such as mean stress, surface finish, and environment. The framework places this threshold alongside similar cost thresholds in plaque vulnerability, ignition, and magnetic reconnection, but that unification is a structural claim within the framework, not a demonstrated physical law.

theorem fatigueCost_pos_off_yield {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
    0 < fatigueCost r := Cost.Jcost_pos_of_ne_one r hr hne

/-- Endurance threshold lies in the canonical band. -/
theorem endurance_threshold_band :
    0.11 < EnduranceThreshold ∧ EnduranceThreshold < 0.13 := by
  unfold EnduranceThreshold
  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  rw [Cost.Jcost_eq_sq hphi_ne]
  have h_lo : (1.61 : ℝ) < phi := Constants.phi_gt_onePointSixOne
  have h_hi : phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  have hpos : (0 : ℝ) < 2 * phi := by
    have : (0 : ℝ) < phi := Constants.phi_pos
    linarith
  refine ⟨?lo, ?hi⟩
  · rw [lt_div_iff₀ hpos]
    nlinarith [h_lo, h_hi]
  · rw [div_lt_iff₀ hpos]
    nlinarith [h_lo, h_hi]

/-- Infinite-life and fatigue-failing are mutually exclusive. -/
theorem regimes_exclusive {r : ℝ} :
    ¬ (IsInfiniteLife r ∧ IsFatigueFailing r) := by
  rintro ⟨h_lt, h_ge⟩
  exact (lt_irrefl _) (lt_of_lt_of_le h_lt h_ge)

What this page does not claim

The theorem does not prove that any physical material has an endurance limit at the modeled threshold. The theorem does not establish that sub-yield operation is always safe in real components. The framework's placement of fatigue alongside plaque vulnerability and ignition is a structural claim, not a demonstrated physical law.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Materials/FatigueThresholdFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: