creepRegimeCert
plain-language theorem explainer
This definition supplies a concrete certificate asserting exactly five creep regimes whose strain rates form a geometric sequence with common ratio phi and all rates strictly positive. Materials physicists analyzing failure mechanisms under configDim = 5 would cite it to anchor the phi-ladder description of creep. The construction is a direct record instantiation that substitutes three prior theorems for the structure fields.
Claim. Let CreepRegimeCert be the structure with fields asserting that the cardinality of the set of creep regimes equals 5, that the strain rate function satisfies strainRate(k+1)/strainRate(k) = phi for every natural number k, and that strainRate(k) > 0 for every k. The definition creepRegimeCert is the instance of this structure obtained by substituting the decidable enumeration theorem for the cardinality field, the algebraic ratio theorem for the phi-ratio field, and the power-positivity theorem for the positivity field.
background
In the Creep Regimes from configDim module, materials failure depth is modeled by five canonical regimes (primary transient, secondary steady-state, tertiary accelerating, ductile-brittle transition, final fracture) that correspond to configDim equal to 5. Each regime's characteristic strain rate occupies one rung on the phi-ladder, so adjacent-regime ratios equal phi exactly. The structure CreepRegimeCert packages the three required assertions: exact count of five regimes, constant ratio phi between successive strain rates, and strict positivity of every strain rate value.
proof idea
The definition is a direct structure constructor that populates the three fields of CreepRegimeCert. It assigns the cardinality field from the theorem creepRegime_count, the phi-ratio field from the theorem strainRate_ratio, and the positivity field from the theorem strainRate_pos. No further tactics or reductions are applied.
why it matters
This definition supplies the certified instance realizing the five-regime creep model for materials failure in the Recognition Science framework. It implements the module claim that creep proceeds through five regimes with phi-scaled strain rates, directly linking to the phi-ladder and configDim = 5. Although no downstream theorems depend on it yet, it closes the materials section by providing the concrete certificate needed for further creep analysis. It touches the open question of deriving the specific count 5 from deeper forcing-chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.