canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in the SGWB-from-phi-ladder construction is strictly positive. Cosmology proofs that normalize or cut on that threshold cite this fact. The argument is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold appearing in the stochastic gravitational-wave background construction is strictly positive: $0 < \tau_{\mathrm{can}}$.
background
The module builds a structural account of the stochastic gravitational wave background (SGWB) on the Recognition Science phi-ladder. Status is a zero-sorry structural theorem: the RS estimate $\Omega_{\mathrm{GW}} = J(\varphi)^2 \Omega_{\mathrm{matter}}$ is contrasted with the much smaller nHz band seen by PPTA/NANOGrav.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6. The only upstream fact used here is the tighter real bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a real constant defined from $\varphi$ in this module; positivity is the elementary sanity check before it enters cost or certificate statements (siblings such as domainCost and the SGWB3 certificate).
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \tau_{\mathrm{can}}$ by linarith using the lemma $\varphi > 1.5$. No further Recognition identities are required.
why it matters
Keeps the SGWB structural package free of hidden sign assumptions on its threshold constant. The parent module frames a structural (not phenomenological) theorem for $\Omega_{\mathrm{GW}}$ on the phi-ladder, with the RS-native scale set by $J(\varphi)$ and matter density. Positivity is the minimal arithmetic gate before certificate inhabitants (SGWB3Cert / cert) can treat the threshold as a genuine cut. Lands in the cosmology layer that sits on T6 ($\varphi$ forced) and the J-cost calculus; it does not itself touch T7/T8 or the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.