canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in the RS CMB damping-scale certificate is strictly positive. Cosmology certificates that normalize or cut on that threshold cite this non-degeneracy. Proof is a one-line unfold of the threshold definition followed by linear arithmetic from φ > 1.5.
Claim. The canonical threshold (the explicit real built from $\varphi$ in this module) is strictly positive: $0 < t_{\mathrm{can}}$.
background
This module treats the CMB damping multipole as an RS structural claim: observationally $\ell_D \sim 1500$–$2000$, while the $\varphi$-ladder gives $\varphi^{15} \approx 1364$ and $\varphi^{16} \approx 2207$, so $\ell_D$ sits between those two rungs. The file is marked structural (zero sorry, zero axiom).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced in the Recognition chain (T6). The only upstream fact used here is the tighter numerical bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is an explicit real expression in $\varphi$ (unfolded in the proof); siblings also record a domain cost and its nonnegativity for the same certificate.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting strict inequality by linarith using phi_gt_onePointFive ($1.5 < \varphi$). No further lemmas or case splits.
why it matters
Keeps the CMB damping-scale certificate non-vacuous: a non-positive threshold would collapse the cut or normalization used when matching $\ell_D$ to the $\varphi^{15}$–$\varphi^{16}$ window. The module status line frames this as part of a structural theorem with no sorry and no axioms. No downstream consumers are wired yet in the graph; the natural parent is the CMB damping-scale certificate inhabitation in this same file. Landmark link is T6 ($\varphi$ forced) and the $\varphi$-ladder mass/scale bookkeeping used throughout RS cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.