canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of the W-boson mass module is strictly positive. Anyone citing the Module-12 structural certificate (M_W ≈ φ^13 · 0.154) needs this gate before cost or mass comparisons. Proof is a one-line unfold of the threshold definition plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold $t_{\mathrm{can}}$ (the named real constant built from $\varphi$ in this module) satisfies $0 < t_{\mathrm{can}}$.
background
Physics RS Module 12 records the W-boson mass match $M_W \approx 80.4,\mathrm{GeV}$ against $\varphi^{13}\cdot 0.154 \approx 80.3,\mathrm{GeV}$ as a structural theorem (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 phi_gt_onePointFive supplies the tighter real bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. The canonical threshold is a sibling definition in the same module: an explicit real expression in $\varphi$ used as a positivity gate for domain-cost and mass comparisons. Sibling lemmas include nonnegativity of the domain cost and the inhabited certificate RSPhysics012Cert.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0<t_{\mathrm{can}}$ by linarith using the single fact $1.5<\varphi$ from Constants.phi_gt_onePointFive.
why it matters
Local positivity gate inside the W-boson structural certificate of Module 12. No recorded downstream edges yet; it supports sibling comparison and certificate lemmas (domainCost_nonneg, RSPhysics012Cert, cert_inhabited). Sits on the φ-ladder mass formula (yardstick · φ^(rung−8+gap(Z))) and on the T6 forcing of φ. Fully proved; closes no open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.