Encyclopedia Materials Materials Creep Regimes From Config Dim Creep Regime Count
ARTICLE 3 claims 3 theorems
Materials Creep Regimes From Config Dim Creep Regime Count
In materials science, creep is slow deformation under stress; a machine-checked library proves five canonical stages and ties their rates to a single ratio.
Creep regimes
Creep is the slow, time-dependent deformation of a material under a sustained load. When a turbine blade runs hot or a bridge carries its weight for decades, creep is what slowly changes shape. Engineers classify the process into stages. The Recognition Science framework's machine-checked library of formal theorems contains a declaration, creepRegime_count, that pins down the number of these stages: there are exactly five. They are primary (transient), secondary (steady-state), tertiary (accelerating), the ductile-brittle transition, and final fracture. This is a proved theorem, not a definitional choice; the proof is a direct computation in the library.
The classical picture of creep has a long history. In 1910, Andrade described transient creep, where the strain rate decreases with time. By the 1920s, the steady-state or secondary stage, where the rate is roughly constant, was recognized as the design-relevant regime for long service life. The tertiary stage, with accelerating strain leading to rupture, completes the standard three-stage model. The framework's five-regime count extends this by separating the ductile-brittle transition and final fracture as distinct regimes, matching the way engineers treat them as separate failure modes.
In Recognition Science, the number five is not arbitrary. The framework derives it from a deeper structure: the configDim, a count of configuration dimensions, which for materials failure is 5. Each regime's characteristic strain rate sits one rung up the φ-ladder, meaning the ratio of strain rates between adjacent regimes is the golden ratio φ. The library proves this ratio theorem: for any step k, the strain rate at step k+1 divided by the strain rate at step k equals φ. It also proves that all these strain rates are positive. Together, these three results form a certificate, a bundled proof that the five-regime structure and the φ-ratio are consistent.
The practical consequence is a quantitative rule of thumb: when a material moves from one creep regime to the next, its characteristic strain rate multiplies by about 1.618. This is a strong, testable prediction. The framework does not claim that real materials always obey this ratio exactly; real creep depends on temperature, stress, and microstructure. What the library establishes is a clean structural result, a precise statement about a model. The empirical check, comparing the φ-ratio to measured creep rates, is a separate question that the library does not address.
THEOREM creepRegime_count · IndisputableMonolith/Materials/CreepRegimesFromConfigDim.lean
theorem creepRegime_count : Fintype.card CreepRegime = 5 := by decide
THEOREM strainRate_ratio · IndisputableMonolith/Materials/CreepRegimesFromConfigDim.lean
theorem strainRate_ratio (k : ℕ) : strainRate (k + 1) / strainRate k = phi := by
unfold strainRate
have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
rw [div_eq_iff hpos.ne', pow_succ]
ring
THEOREM strainRate_pos · IndisputableMonolith/Materials/CreepRegimesFromConfigDim.lean
theorem strainRate_pos (k : ℕ) : 0 < strainRate k := pow_pos phi_pos k
What this page does not claim
The library does not claim that measured creep rates in real materials follow the φ-ratio exactly. The theorem does not define what creep is; it only counts the regimes in the framework's model. The framework does not claim that the ductile-brittle transition is universally a separate creep stage in all materials.
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/CreepRegimesFromConfigDim.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:
- How does the framework derive configDim = 5 for materials failure from the underlying forcing chain?
- What experimental evidence, if any, supports the φ-ratio between creep regime strain rates?
- Does the five-regime classification match the standard three-stage creep model in all engineering contexts?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM creepRegime_count · IndisputableMonolith/Materials/CreepRegimesFromConfigDim.lean
theorem creepRegime_count : Fintype.card CreepRegime = 5 := by decideThere are exactly five creep regimes: primary, secondary, tertiary, ductile-brittle transition, and final fracture. creepRegime_count · IndisputableMonolith/Materials/CreepRegimesFromConfigDim.leanTHEOREM strainRate_ratio · IndisputableMonolith/Materials/CreepRegimesFromConfigDim.lean
theorem strainRate_ratio (k : ℕ) : strainRate (k + 1) / strainRate k = phi := by unfold strainRate have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k rw [div_eq_iff hpos.ne', pow_succ] ringThe ratio of strain rates between adjacent regimes is the golden ratio φ. strainRate_ratio · IndisputableMonolith/Materials/CreepRegimesFromConfigDim.leanTHEOREM strainRate_pos · IndisputableMonolith/Materials/CreepRegimesFromConfigDim.lean
theorem strainRate_pos (k : ℕ) : 0 < strainRate k := pow_pos phi_pos kAll strain rates are positive. strainRate_pos · IndisputableMonolith/Materials/CreepRegimesFromConfigDim.lean