creepRegime_count
plain-language theorem explainer
The theorem establishes that the type enumerating creep regimes has cardinality five. Materials researchers modeling failure under Recognition Science would cite this when confirming the five-stage structure tied to configDim. The proof is a one-line decision procedure that computes the cardinality directly from the inductive enumeration.
Claim. The number of creep regimes is five: $|S| = 5$, where $S$ consists of the stages primary, secondary, tertiary, ductile-brittle transition, and fracture.
background
The module models materials creep as advancing through five canonical regimes equated to configDim D = 5. These comprise primary (transient), secondary (steady-state), tertiary (accelerating), ductile-brittle transition, and final fracture. Each regime's characteristic strain rate occupies one rung on the phi-ladder, so adjacent-regime ratios equal phi.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This evaluates the Fintype cardinality of the inductive type with five constructors and confirms the result equals 5 by direct computation.
why it matters
The result supplies the five_regimes field for the downstream CreepRegimeCert definition. It realizes the module claim that creep proceeds through five regimes (= configDim D = 5) with phi-ladder spacing. This supports self-similar scaling from the forcing chain (T5-T6) and eight-tick octave (T7), applied here to materials configDim rather than spatial D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.