canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of the Higgs-ratio physics module is strictly positive. Cite it whenever a later certificate or comparison needs a positive φ-derived scale in this module. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The module's canonical threshold (a real constant built from the golden ratio $\varphi$) is strictly positive: $0 < \tau$, where $\tau$ denotes that threshold.
background
Physics RS Module 6 packages the structural comparison of the Higgs vacuum expectation value ratio $v/M_Z = 246/91.2 \approx 2.70$ with $\varphi^2 \approx 2.618$ (about 3% off). The module is marked as a structural theorem block: zero sorry, zero axiom.
The golden ratio is $\varphi = (1+\sqrt{5})/2$. An upstream constants lemma records the tighter lower bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a real defined from $\varphi$ in this module (sibling of the domain-cost helpers); the present result only asserts its positivity.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then run linarith on the resulting arithmetic inequality, feeding the upstream lemma $\varphi > 1.5$. No case split and no further RS structure is used.
why it matters
Supplies the positivity side-condition on the module's φ-derived threshold scale. Sits beside domainCost_nonneg and the module certificate (RSPhysics006Cert / cert_inhabited) that package the Higgs-ratio observation as a structural theorem. No external used_by edges yet; the lemma is local scaffolding for any later comparison that needs $\tau > 0$.
In the broader RS stack this is routine hygiene on φ-ladder scales: once $\varphi > 1.5$ is known, elementary linear combinations stay positive. It does not touch the forcing chain (T5–T8), the Recognition Composition Law, or the mass-ladder formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.