canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold in the RS cosmology module is strictly positive. Cosmology certificates and domain-cost arguments cite this to keep the threshold above zero. The proof is a one-line unfold of the definition followed by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold of the RS cosmology module is strictly positive: $0 < T_{\mathrm{can}}$.
background
Module RS_Cosmo_Module_002 is a structural cosmology certificate: it records that the dimensionless combination $\Lambda \ell_P^2$ equals $8\varphi^5/45$, which lands in $(1.88,2.03)\times 10^{-122}$ and matches the Planck value $1.99\times 10^{-122}$ (RS_PASS, zero sorry, zero axioms).
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. The upstream lemma phi_gt_onePointFive supplies the tight lower bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. The canonical threshold is a $\varphi$-expression used as a positivity gate for domain-cost comparisons in this module.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting real inequality by linarith using the single fact $\varphi>1.5$. No further case splits or algebraic identities are required.
why it matters
Keeps the positivity gate of the RS cosmology certificate honest: without $T_{\mathrm{can}}>0$, domain-cost non-negativity and the inhabited certificate RSCosmo002Cert would be vacuous. The module sits in the cosmology lane that checks $\Lambda\ell_P^2=8\varphi^5/45$ against Planck. No downstream consumers are wired yet; the lemma is local scaffolding for the module's own cert bundle. It does not touch the forcing chain T0–T8 directly, but inherits $\varphi$ from Constants, which is forced at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.