CreepRegimeCert
plain-language theorem explainer
CreepRegimeCert packages the assertion that exactly five creep regimes exist with strain rates forming a geometric sequence of common ratio phi. Materials modelers cite it when verifying that the configDim=5 ladder matches the Recognition Science phi-ladder. The declaration is a structure definition whose three fields are instantiated directly by the sibling constructor creepRegimeCert.
Claim. A structure certifying that the five creep regimes satisfy $|CreepRegime|=5$, that the strain rate obeys $r(k+1)/r(k)=phi$ for all $k$, and that $r(k)>0$ for all $k$, where $r$ denotes the strain-rate function on the phi-ladder.
background
CreepRegime is the inductive type with five constructors: primary, secondary, tertiary, ductileBrittle, and fracture. The strainRate function is defined noncomputably as phi^k, placing each regime one rung higher on the phi-ladder so that adjacent rates differ by the factor phi. The module states that materials creep proceeds through these five regimes when configDim equals 5, with the phi-ratio supplied by the upstream Quasicrystal.phi_ratio definition.
proof idea
CreepRegimeCert is a structure definition containing no proof body. Its fields are populated by the downstream constructor creepRegimeCert, which applies the sibling lemmas creepRegime_count for the cardinality, strainRate_ratio for the geometric progression, and strainRate_pos for positivity.
why it matters
The structure anchors the B9 materials failure model by certifying the five-regime phi-ladder required for creep analysis. It is instantiated by creepRegimeCert and thereby supplies the rate-scaling hypothesis used in downstream materials theorems. Within the Recognition Science framework it realizes the phi-ladder forced at T6 and the self-similar fixed point, linking configDim=5 to the eight-tick octave while leaving the spatial dimension D=3 to the upstream forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.