canonicalThreshold_pos
plain-language theorem explainer
The canonical materials threshold is strictly positive. Anyone citing the RS copper Debye-temperature ladder (φ^12 structural match) needs this positivity fact as a basic well-definedness check. Proof is a one-line wrapper: unfold the threshold and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold built from the golden ratio $\varphi$ is strictly positive: $0 < T_{\mathrm{can}}(\varphi)$.
background
This module is Materials RS Module 2, a structural (zero-sorry) package whose headline comparison is the copper Debye temperature on the $\varphi$-ladder: $\varphi^{12},\mathrm{K} \approx 321.9,\mathrm{K}$ versus the experimental $\sim 343,\mathrm{K}$ (about 6% off).
The golden ratio is $\varphi = (1+\sqrt{5})/2$. The upstream lemma phi_gt_onePointFive records the tight elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a module-local constant expressed in terms of $\varphi$ (sibling of the domain-cost definitions imported from Constants and Cost); positivity of that constant is the claim here.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting strict inequality by linarith using the single upstream fact $\varphi > 1.5$. No further case splits or cost-functional identities are required.
why it matters
Positivity is the minimal well-definedness gate for any threshold used later in the materials stack (domain cost, certification bundle RSMatl002Cert). The module itself is marked STRUCTURAL and targets the copper Debye match on the $\varphi$-ladder, consistent with the broader RS forcing picture in which $\varphi$ is the self-similar fixed point (T6) and dimensionful scales sit on integer rungs. No downstream theorems currently cite this lemma (used_by is empty), so it functions as local infrastructure inside the materials certificate rather than a cross-module bridge. It does not itself close the 6% Debye residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.