canonicalThreshold_pos
plain-language theorem explainer
The materials-module canonical threshold is a strictly positive real. Anyone citing the RS creep package (power-law exponent n = D = 3) needs this sign fact before comparing costs or rates. Proof is a one-line unfold of the threshold definition followed by linarith from the bound φ > 1.5.
Claim. The canonical threshold constant of the materials creep module is strictly positive: $0 < t_{\mathrm{can}}$.
background
Materials RS Module 7 records the structural claim that the power-law creep exponent equals the spatial dimension, $n = D = 3$, with no sorry and no extra axioms. The module imports the RS constants and the J-cost layer.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified chain. An upstream lemma tightens the elementary bound to $\varphi > 1.5$ (from $\sqrt{5} > 2$). The canonical threshold is a real constant defined in this module from $\varphi$; its positivity is the elementary sign fact needed before any comparison that treats the threshold as a positive scale.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting linear inequality by linarith using the upstream lemma $\varphi > 1.5$. No further case splits or cost identities are required.
why it matters
Positivity of the threshold is a supporting lemma inside the materials creep package whose headline claim is $n = D = 3$ (exact, structural). That identification sits on the forcing-chain landmark T8 ($D = 3$ spatial dimensions) and uses the $\varphi$-ladder fixed at T6. Sibling certificate constructors (RSMatl007Cert, cert_inhabited) package the module; this sign fact keeps threshold comparisons well-defined. No downstream dependents are recorded yet, so the lemma is presently a leaf inside the module certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.