canonicalThreshold_pos
plain-language theorem explainer
The RS canonical threshold (a φ-derived positive scale used in the AllPhysics5 package) is strictly greater than zero. Cite it wherever a positivity side-condition on that threshold is needed. Proof is a one-line unfold of the definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the Recognition-Science threshold constant defined from the golden ratio $\varphi = (1+\sqrt{5})/2$.
background
Module AllPhysics5 is the structural end-package of Recognition Science: gravity, EM, weak, strong, Higgs, matter masses, and cosmology are all to be read off the single cost $J$, with zero free parameters and no sorry.
The golden ratio $\varphi$ is the self-similar fixed point forced at T6 of the unified forcing chain. The Constants library supplies a tight elementary lower bound $\varphi > 1.5$ (from $\sqrt{5} > 2$). The canonical threshold is the local φ-scale used by the domain-cost apparatus in this file; its positivity is the elementary side-condition recorded here.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \tau_{\mathrm{can}}$ by linarith against the imported lemma $\varphi > 1.5$. No further algebraic identity is required.
why it matters
Keeps the AllPhysics5 certificate free of hidden positivity gaps: every later appeal to a positive threshold scale (domain-cost nonnegativity, mass-ladder cutoffs, or the structural AllPhysics5Cert) can quote a proved fact rather than an inline arithmetic side-condition. Sits next to domainCost_nonneg and the inhabited certificate in the same module. Landmark link is T6 (φ forced); the numerical bound used is the elementary Constants lemma $\varphi > 1.5$. No downstream edges are recorded yet; the lemma is infrastructure for the zero-sorry structural claim of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.