canonicalThreshold_pos
plain-language theorem explainer
The canonical materials threshold is strictly positive. Lattice and domain-cost arguments in the Cu FCC module cite this to keep the threshold on the positive side of the cost scale. The proof is a one-line unfold of the threshold definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold constant of the materials module is strictly positive: $0 < \tau_{\mathrm{can}}$.
background
Materials RS Module 3 records a structural match for the copper FCC lattice: $\varphi^4 a_0 \approx 3.626,\mathrm{\AA}$ against the experimental $3.615,\mathrm{\AA}$ (about $0.3%$). The module is marked as a structural theorem block with no sorry and no extra axioms.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced in the Recognition chain (T6). The upstream lemma phi_gt_onePointFive supplies the tighter real bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a $\varphi$-native constant used alongside the domain cost $J$ in this materials layer; positivity is the elementary gate before any comparison to lattice scales.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \tau_{\mathrm{can}}$ by linarith using the single upstream fact $\varphi > 1.5$. No further case splits or Recognition identities are required.
why it matters
Keeps the materials threshold on the positive side of the cost scale so later Cu FCC comparisons and the module certificate (RSMatl003Cert / cert_inhabited) can treat it as a genuine positive yardstick. It sits in the materials domain rather than the T0–T8 forcing chain, but it inherits $\varphi$ from Constants and therefore from T6. No downstream theorems are wired yet (used_by is empty); the immediate consumers are the sibling certificate constructions in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.