canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant in the RS physics layer is strictly positive. Mass-matching and domain-cost arguments that need a positive cutoff cite this fact. The proof unfolds the definition and finishes by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < T_{\mathrm{can}}$, where $T_{\mathrm{can}}$ is the real constant obtained by unfolding the module's canonical-threshold definition (a simple expression in the golden ratio $\varphi$).
background
Physics RS Module 11 records the structural Z-boson mass match $M_Z \simeq 91.2,\mathrm{GeV} \sim \varphi^{13}\cdot 0.175$, with status "structural theorem" (no sorry, no axiom). The module imports the global Constants and Cost layers and exposes a small family of domain-cost and threshold helpers.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the Recognition forcing chain. The upstream lemma phi_gt_onePointFive supplies the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a real constant built from $\varphi$; positivity of that constant is the only claim here.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (exposing an elementary expression in $\varphi$), then invoke linarith on the single upstream fact $\varphi > 1.5$. No further lemmas or case splits are required.
why it matters
Module 11 is a structural certificate for the Z-boson rung on the $\varphi$-ladder. A positive canonical threshold is the minimal arithmetic hygiene needed before any domain-cost comparison or mass-yardstick inequality can be stated. Downstream use is currently empty in the graph, so the lemma sits as a local positivity fact supporting the module certificate RSPhysics011Cert and the inhabited certificate cert_inhabited. It does not itself encode the mass formula or the eight-tick octave; it only clears the sign of the cutoff those arguments presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.