pith. machine review for the scientific record. sign in
def definition def or abbrev high

strainRate

show as:
view Lean formalization →

strainRate defines the characteristic strain rate for the k-th creep regime as phi to the power k. Materials scientists analyzing failure modes would cite this when scaling rates across the five regimes via the phi-ladder. The definition is a direct power assignment that supplies the base for ratio and positivity results.

claimFor each natural number $k$, the strain rate at rung $k$ is defined by $s(k) = phi^k$, where $phi$ is the self-similar fixed point satisfying the Recognition Composition Law.

background

The module models materials creep through five canonical regimes (primary, secondary, tertiary, ductile-brittle transition, fracture) that equal configDim D = 5. Each regime's strain rate occupies one rung on the phi-ladder, so adjacent-regime ratios equal phi. This rests on the Recognition Science constants imported from Constants, with phi arising as the fixed point in T6 of the unified forcing chain.

proof idea

The declaration is a one-line definition that directly assigns strainRate k to phi raised to the power k. No lemmas or tactics are applied; it functions as the base assignment for the downstream ratio and positivity theorems.

why it matters in Recognition Science

This definition feeds the CreepRegimeCert structure, which certifies five regimes, phi ratios between adjacent strain rates, and strict positivity. It realizes the B9 Materials Failure Depth by placing creep rates on the phi-ladder from the forcing chain (T5 J-uniqueness through T8 D = 3). The placement extends the Recognition Composition Law to materials scaling while leaving open the explicit mapping from spatial D = 3 to configDim = 5.

scope and limits

formal statement (Lean)

  30noncomputable def strainRate (k : ℕ) : ℝ := phi ^ k

proof body

Definition body.

  31

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.