IndisputableMonolith.Materials.CreepRegimesFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Creep Regimes from configDim — B9 Materials Failure Depth
   6
   7Materials creep proceeds through five canonical regimes (= configDim D = 5):
   8  primary (transient), secondary (steady-state), tertiary (accelerating),
   9  ductile-brittle transition, and final fracture.
  10
  11Each regime's characteristic strain rate sits one rung up the φ-ladder:
  12adjacent-regime rate ratio = φ.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith.Materials.CreepRegimesFromConfigDim
  18open Constants
  19
  20inductive CreepRegime where
  21  | primary
  22  | secondary
  23  | tertiary
  24  | ductileBrittle
  25  | fracture
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem creepRegime_count : Fintype.card CreepRegime = 5 := by decide
  29
  30noncomputable def strainRate (k : ℕ) : ℝ := phi ^ k
  31
  32theorem strainRate_ratio (k : ℕ) : strainRate (k + 1) / strainRate k = phi := by
  33  unfold strainRate
  34  have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  35  rw [div_eq_iff hpos.ne', pow_succ]
  36  ring
  37
  38theorem strainRate_pos (k : ℕ) : 0 < strainRate k := pow_pos phi_pos k
  39
  40structure CreepRegimeCert where
  41  five_regimes : Fintype.card CreepRegime = 5
  42  phi_ratio : ∀ k, strainRate (k + 1) / strainRate k = phi
  43  strainRate_always_pos : ∀ k, 0 < strainRate k
  44
  45noncomputable def creepRegimeCert : CreepRegimeCert where
  46  five_regimes := creepRegime_count
  47  phi_ratio := strainRate_ratio
  48  strainRate_always_pos := strainRate_pos
  49
  50end IndisputableMonolith.Materials.CreepRegimesFromConfigDim
  51