strainRate_pos
plain-language theorem explainer
The theorem shows that strain rate at rung k on the phi-ladder is strictly positive for every natural number k. Materials modelers working on creep failure would cite it to guarantee well-defined positive rates in all five regimes. The proof is a one-line wrapper that applies the standard positivity lemma for powers of a positive base.
Claim. For every natural number $k$, the strain rate defined by $r(k) = phi^k$ satisfies $r(k) > 0$.
background
The module treats materials creep as five canonical regimes fixed by configDim equal to 5: primary, secondary, tertiary, ductile-brittle transition, and fracture. Each regime occupies one rung on the phi-ladder, so adjacent strain-rate ratios equal phi. The upstream definition sets the strain rate at rung k to phi raised to k.
proof idea
The proof is a one-line wrapper that applies the lemma pow_pos to the positivity of phi and the exponent k.
why it matters
The result is invoked inside creepRegimeCert to certify that all five regimes have positive strain rates together with the phi ratio. It closes the positivity requirement for the B9 materials failure model and aligns with the phi-ladder scaling used throughout the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.