canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold (a real calibration constant built from the golden ratio) is strictly positive. Structural and cost-layer arguments that need a positive cutoff cite 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 $T$ (the real calibration constant defined from the golden ratio $\varphi$ in this module) satisfies $0 < T$.
background
This module is RS Structural Mathematics 10. Its local setting is RS calibration with the coherence energy $E_{\mathrm{coh}}$ fixed once by the electron mass, after which predictions are parameter-free. The status line marks the file as a structural theorem block (no sorry, no extra axioms).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced in the RS chain (T6). The only upstream fact used here is the tighter numerical bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a real constant defined from $\varphi$ in this file (sibling of the domain-cost definitions); positivity is the minimal arithmetic fact needed before any cost or cutoff comparison can fire.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi > 1.5$ from phi_gt_onePointFive. No case split and no further RS lemmas: after unfolding, the goal is a linear inequality in $\varphi$ discharged by that bound.
why it matters
Positivity of the canonical threshold is a structural hygiene lemma in the mathematics layer: any later comparison that treats the threshold as a strict cutoff needs $T > 0$ on the nose. The module packages this with domain-cost non-negativity and a certificate (RSMTHStructural010Cert) so the structural block can be inhabited as a unit.
In the broader RS forcing picture this sits downstream of T6 ($\varphi$ forced) and the Constants development that supplies $\varphi > 1.5$. It does not itself touch T5 J-uniqueness, the eight-tick octave, or the mass ladder, but it keeps the calibration side free of ad-hoc sign assumptions. No downstream theorems are wired yet (used_by is empty); the immediate consumer is the module certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.