IndisputableMonolith.Materials.FatigueThresholdFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Materials Fatigue Threshold from J-Cost on Stress Ratio
   7
   8Materials fatigue (Wöhler / S-N curve, Basquin's law, Coffin-Manson) is
   9the failure of metals and polymers under cyclic loading at stresses far
  10below the static yield. In RS terms, fatigue is governed by recognition
  11cost on the dimensionless stress ratio `r := observed_stress / yield_stress`.
  12The J-cost minimum is at `r = 1` (no perturbation from yield baseline);
  13sub-yield operation `r < 1` carries strictly positive J-cost that
  14accumulates per cycle.
  15
  16The fatigue limit (endurance limit, ~σ_e ≈ 0.5 σ_yield for many steels)
  17corresponds to the canonical golden-section J-cost threshold
  18`J(φ) ∈ (0.11, 0.13)` on the inverse-stress ratio. Below the limit,
  19infinite-life is structurally permitted; at or above, finite-life
  20behaviour holds. This places fatigue alongside plaque vulnerability,
  21infarction, dysbiosis, ignition, accretion-disk transition, and magnetic
  22reconnection: one universal RS quantum across pathology, combustion,
  23plasma, and structural engineering.
  24
  25Lean status: 0 sorry, 0 axiom.
  26-/
  27
  28namespace IndisputableMonolith
  29namespace Materials
  30namespace FatigueThresholdFromJCost
  31
  32open Constants Cost
  33
  34noncomputable section
  35
  36/-- Per-cycle fatigue J-cost on the stress ratio. -/
  37def fatigueCost (r : ℝ) : ℝ := Cost.Jcost r
  38
  39theorem fatigueCost_zero_at_yield : fatigueCost 1 = 0 := Cost.Jcost_unit0
  40
  41theorem fatigueCost_reciprocal_symm {r : ℝ} (hr : 0 < r) :
  42    fatigueCost r = fatigueCost r⁻¹ := Cost.Jcost_symm hr
  43
  44theorem fatigueCost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ fatigueCost r :=
  45  Cost.Jcost_nonneg hr
  46
  47theorem fatigueCost_pos_off_yield {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  48    0 < fatigueCost r := Cost.Jcost_pos_of_ne_one r hr hne
  49
  50/-- Endurance-limit threshold = canonical golden-section quantum. -/
  51def EnduranceThreshold : ℝ := Cost.Jcost phi
  52
  53/-- Fatigue failure regime (above the endurance limit). -/
  54def IsFatigueFailing (r : ℝ) : Prop := EnduranceThreshold ≤ fatigueCost r
  55
  56/-- Infinite-life regime (below the endurance limit). -/
  57def IsInfiniteLife (r : ℝ) : Prop := fatigueCost r < EnduranceThreshold
  58
  59/-- Infinite-life and fatigue-failing are mutually exclusive. -/
  60theorem regimes_exclusive {r : ℝ} :
  61    ¬ (IsInfiniteLife r ∧ IsFatigueFailing r) := by
  62  rintro ⟨h_lt, h_ge⟩
  63  exact (lt_irrefl _) (lt_of_lt_of_le h_lt h_ge)
  64
  65/-- Endurance threshold lies in the canonical band. -/
  66theorem endurance_threshold_band :
  67    0.11 < EnduranceThreshold ∧ EnduranceThreshold < 0.13 := by
  68  unfold EnduranceThreshold
  69  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  70  rw [Cost.Jcost_eq_sq hphi_ne]
  71  have h_lo : (1.61 : ℝ) < phi := Constants.phi_gt_onePointSixOne
  72  have h_hi : phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  73  have hpos : (0 : ℝ) < 2 * phi := by
  74    have : (0 : ℝ) < phi := Constants.phi_pos
  75    linarith
  76  refine ⟨?lo, ?hi⟩
  77  · rw [lt_div_iff₀ hpos]
  78    nlinarith [h_lo, h_hi]
  79  · rw [div_lt_iff₀ hpos]
  80    nlinarith [h_lo, h_hi]
  81
  82structure FatigueThresholdCert where
  83  yield_zero : fatigueCost 1 = 0
  84  reciprocal_symm : ∀ {r : ℝ}, 0 < r → fatigueCost r = fatigueCost r⁻¹
  85  cost_nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ fatigueCost r
  86  threshold_band :
  87    0.11 < EnduranceThreshold ∧ EnduranceThreshold < 0.13
  88  regimes_exclusive :
  89    ∀ {r : ℝ}, ¬ (IsInfiniteLife r ∧ IsFatigueFailing r)
  90
  91/-- Fatigue-threshold certificate. -/
  92def fatigueThresholdCert : FatigueThresholdCert where
  93  yield_zero := fatigueCost_zero_at_yield
  94  reciprocal_symm := fatigueCost_reciprocal_symm
  95  cost_nonneg := fatigueCost_nonneg
  96  threshold_band := endurance_threshold_band
  97  regimes_exclusive := regimes_exclusive
  98
  99end
 100end FatigueThresholdFromJCost
 101end Materials
 102end IndisputableMonolith
 103