canonicalThreshold_pos
plain-language theorem explainer
The RS canonical cosmological threshold is strictly positive. Cosmology certificates and domain-cost arguments that need a positive cutoff cite this fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical cosmological threshold built from the golden ratio is strictly positive: $0 < T_{\mathrm{can}}$, where $T_{\mathrm{can}}$ is defined from $\varphi = (1+\sqrt{5})/2$.
background
This module is Cosmology RS Module 1. Its structural claim is that the RS dark-energy density $\Omega_\Lambda = 11/16 - \alpha/\pi$ equals $0.685$, matching the Planck value to $0.665\sigma$, with status STRUCTURAL THEOREM (zero sorry, zero axiom).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the Recognition forcing chain. The upstream lemma phi_gt_onePointFive records the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$.
Sibling definitions in the module introduce a domain cost and a canonical threshold built from $\varphi$. Positivity of that threshold is the elementary arithmetic fact needed before nonnegativity or certificate packing can proceed.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the single upstream fact $\varphi > 1.5$. No case split and no further Recognition identities are required.
why it matters
Keeps the Module-1 cosmology certificate on a fully proved footing: every quantity that feeds the $\Omega_\Lambda$ match must be known positive before the structural certificate (RSCosmo001Cert / cert_inhabited) can be inhabited. The result is pure arithmetic on $\varphi$, so it sits under T6 (phi forced) rather than under the later mass or coupling ladders. Downstream graph edges are empty here, but the sibling cluster (domainCost_nonneg, cert) is the natural consumer. No open scaffold remains: the claim is closed with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.