canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of the Higgs-mass physics module is strictly positive. Anyone comparing domain costs or rung placements against that cutoff cites this fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold of this module is a strictly positive real: $0 < \tau$, where $\tau$ is the module's canonical threshold constant (an explicit expression in the golden ratio $\varphi$).
background
Physics RS Module 10 records the Higgs-mass match $m_H \approx 125.25,\mathrm{GeV}$ against a $\varphi$-ladder placement ($\varphi^{13}$ scaled into GeV). Status 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 only upstream input is the elementary bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. Sibling declarations define a domain cost, its nonnegativity, and the canonical threshold itself; this theorem is the positivity half of that local cutoff package.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then close with linarith using the upstream lemma $\varphi > 1.5$. No case split and no further RS structure is required once the definition is expanded.
why it matters
Module 10's structural certificate needs the canonical threshold to be a strict positive barrier before domain-cost comparisons are meaningful. This lemma discharges that positivity obligation next to the siblings on domain cost and the module certificate inhabitation.
It sits inside the Higgs-mass match narrative ($m_H \sim \varphi^k,\mathrm{GeV}$) but does not itself compute the mass. Framework landmark in play is only T6 ($\varphi$ as fixed point) via the bound $\varphi > 1.5$. No downstream dependents are recorded yet; the result is local scaffolding closure for the module cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.