canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of the lead (Pb) materials module is strictly positive. Anyone citing the Module 9 Cooper-pair certificate or needing a positive cutoff built from φ can invoke it. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $T$ (the explicit real constant defined from the golden ratio $\varphi$ in this materials module) satisfies $0 < T$.
background
Materials RS Module 9 is a structural (zero-sorry) certificate for Cooper-pair binding in lead: it records the match $\varphi^3 \cdot 0.642,\mathrm{meV} = 2.72,\mathrm{meV}$. The module introduces a domain cost (from the RS cost layer) and a canonical threshold built from the golden ratio $\varphi = (1+\sqrt{5})/2$.
The only upstream fact used here is the elementary lower bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$ so that $(1+\sqrt{5})/2 > 3/2$. That bound is enough to force positivity once the threshold definition is unfolded. Sibling facts in the same file establish nonnegativity of the domain cost and package the module certificate RSMatl009Cert.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi > 1.5$. No further lemmas or case splits are required; positivity is pure linear arithmetic in $\varphi$.
why it matters
Supplies the positivity half of the canonical cutoff used by the Pb Cooper-pair materials certificate (RSMatl009Cert / cert_inhabited in the same module). The module is marked STRUCTURAL THEOREM with a numerical MATCH for lead binding, so a proved positive threshold is part of keeping that certificate axiom-free.
In the broader RS chain this sits downstream of T6 (φ forced as the self-similar fixed point) and the Constants layer; it does not itself touch T5 J-uniqueness, the eight-tick octave, or the α band. No external used_by edges are recorded yet, so its present role is local scaffolding closure inside Module 9 rather than a cross-module lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.