canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in RS calibration is strictly positive. Anyone discharging nonnegativity or positivity obligations on that threshold (domain-cost bounds, certificate packing) would cite this. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the RS calibration threshold built from the golden ratio $\varphi=(1+\sqrt{5})/2$.
background
Module 10 of the RS forcing chain treats calibration: $E_{\mathrm{coh}}$ is the single free parameter, fixed by the electron mass at rung 3. Status is structural (zero sorry, zero axiom).
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced earlier in the chain (T6). The only upstream fact used here is the tighter lower bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. The canonical threshold is a named real constant in this module, defined by unfolding in terms of $\varphi$; sibling lemmas package domain cost and the module certificate around the same constant.
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 are required; positivity is pure real arithmetic once the definition is expanded.
why it matters
Keeps the Module 10 certificate honest: every calibration quantity that must sit strictly above zero inherits this fact. Downstream packing in the same file (the forcing-chain certificate and its inhabited instance) can quote positivity without re-proving arithmetic on $\varphi$. In the broader framework it sits under the forcing chain after T6 ($\varphi$ forced) and supports the structural claim that RS calibration constants are well-defined positive reals. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.