canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold appearing in the RS5 neutron–proton mass-difference setup is strictly positive. Anyone building or citing the structural certificate for m_n − m_p needs this sign fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold built from the golden ratio is strictly positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the module's canonical threshold (a real expression in $\varphi$).
background
This module records the Recognition Science account of the neutron–proton mass split as a structural theorem (zero sorry, zero axiom). The target identity is $m_n - m_p = 1.293,\mathrm{MeV}$, recovered in RS units as $J(\varphi)$ times a fixed MeV scale (equivalently $J(\varphi)\cdot(m_W/45)$ with a stated correction).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced earlier in the chain. An upstream lemma supplies the tight numerical bound $\varphi > 1.5$ (from $\sqrt{5} > 2$). The canonical threshold is a real quantity defined from $\varphi$ in this file; its positivity is the elementary sign fact needed before domain-cost and certificate constructions can proceed.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the upstream lemma $\varphi > 1.5$. No further case splits or Recognition-cost identities are required; positivity is pure real arithmetic once the definition is expanded.
why it matters
Sits in the Foundation layer that closes the RS5 neutron–proton difference as a structural theorem. The module status line states the exact match $J(\varphi)\cdot 10.96,\mathrm{MeV} = 1.293,\mathrm{MeV}$. Positivity of the canonical threshold is the first arithmetic hygiene step before nonnegativity of domain cost and inhabitation of the NeutProtonDiff5 certificate. It does not itself invoke the Recognition Composition Law or the T5–T8 forcing steps, but it inherits $\varphi$ from that chain and keeps the mass-gap certificate free of sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.