canonicalThreshold_pos
plain-language theorem explainer
The canonical materials threshold is a strictly positive real. Anyone packaging Module-12 certificates or needing a positive φ-built cutoff cites this fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold (the Module-12 cutoff built from $\varphi$) is strictly positive: $0 < t_{\mathrm{can}}$.
background
Materials RS Module 12 records BCS coherence lengths as φ-ladder values: $\varphi^7,\mathrm{nm}\approx 29,\mathrm{nm}$ (cuprates) and $\varphi^{15},\mathrm{nm}\approx 1364,\mathrm{nm}$ (conventional), marked MATCH. The module is structural (zero sorry, zero axiom).
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. The upstream lemma supplies the tighter bound $\varphi>1.5$ (from $\sqrt{5}>2$). The canonical threshold is the module's named real cutoff expressed in terms of $\varphi$; its positivity is the elementary gate for any later comparison or certificate that treats the cutoff as a positive scale.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the upstream lemma $\varphi>1.5$. No case split and no materials-specific arithmetic beyond that lower bound.
why it matters
Positivity of the Module-12 cutoff is a structural lemma in the materials layer that matches BCS coherence lengths to φ-ladder rungs. It sits beside the sibling domain-cost nonnegativity facts and feeds the module certificate (RSMatl012Cert / cert_inhabited) even though the current use-graph lists no direct dependents yet.
Framework landmarks: T6 forces φ; the φ-ladder supplies the length yardsticks used in the module doc. The result closes a trivial but required positivity obligation so later materials claims can treat the threshold as a genuine positive scale without re-proving $\varphi>1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.