canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold is strictly positive. Physicists citing domain-cost cutoffs or φ-ladder comparisons in the proton-electron module use this fact. The proof is a one-line wrapper: unfold the threshold definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the RS-native threshold constructed from the golden ratio $\varphi=(1+\sqrt{5})/2$.
background
Physics Module 9 is a structural (zero-sorry) treatment of the proton-electron mass ratio on the φ-ladder: $\varphi^{12}\approx 321.9$, leaving a known factor-$\sim 5.7$ gap relative to the experimental ratio $\sim 1836$. The module introduces a domain cost and a canonical threshold against which that cost is compared.
The golden ratio $\varphi$ is the self-similar fixed point forced at T6 of the unified forcing chain. The only upstream lemma used here is the elementary bound $\varphi>1.5$, obtained from $\sqrt{5}>2$ so that $(1+\sqrt{5})/2>1.5$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith with the lemma $\varphi>1.5$. No further case splits or rewriting are required; positivity is immediate from the linear inequality once the definition is expanded.
why it matters
Supplies the positivity obligation for the canonical threshold used by domain-cost comparisons in the proton-electron structural module. Sits beside domainCost_nonneg and feeds the module certificate RSPhysics009Cert. In the broader framework it aligns with the φ-ladder mass formula and the Berry creation scale $\varphi^{-1}$. The graph currently lists no downstream dependents; the result closes a local arithmetic gap inside a zero-sorry structural theorem rather than a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.