canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant used in the RS CMB acoustic-peak module is strictly positive. Cosmology certificates that compare domain costs against this cutoff cite it. The proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold constant of the RS CMB peak analysis is strictly positive: $0 < T_{\mathrm{can}}$.
background
The ambient module develops a structural account of CMB acoustic peaks under Recognition Science: observed multipoles $\ell_1\sim 220$, $\ell_2\sim 540$, $\ell_3\sim 800$ are read as $\varphi$-power spacings ($\ell_2/\ell_1\approx\varphi^2$, $\ell_3/\ell_1\approx\varphi^{2.8}$). The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain.
Sibling definitions introduce a domain cost (built from the RS cost functional $J$) and a canonical threshold against which that cost is compared when locating peak positions. The only upstream fact needed here is the elementary bound $\varphi>1.5$, recorded as phi_gt_onePointFive (from $\sqrt{5}>2$).
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0<T_{\mathrm{can}}$ by linarith using the lemma $\varphi>1.5$. No case splits or further RS identities are required.
why it matters
Keeps the CMB peak certificate free of hidden sign assumptions: any comparison of domain cost to the canonical threshold needs $T_{\mathrm{can}}>0$ as a precondition. The module is marked structural (zero sorry, zero axiom) and sits in the cosmology layer of the RS mirror. It does not yet appear in a recorded used_by edge, but it is a sibling of CMBPeakPos_v3Cert and the inhabited certificate constructors, so it is the positivity lemma those certificates rely on locally. Landmark contact is T6 ($\varphi$ forced) and the $\varphi$-ladder reading of multipole ratios; it does not touch T7/T8 or the RCL identity directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.