canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant in the RS cosmology module on matter-radiation equality is strictly positive. Anyone building domain-cost comparisons or the Module-7 structural certificate cites this positivity fact. The proof is a one-line wrapper: unfold the definition, then linear arithmetic from φ > 1.5.
Claim. The canonical threshold $T$ of this cosmology module (a real constant built from the golden ratio $\varphi$) satisfies $0 < T$.
background
Module 7 of the RS cosmology stack treats matter-radiation equality as a structural match: $\varphi^{17}\cdot 0.95$ recovers $z_{\mathrm{eq}}\sim 3400$, in line with the empirical value. The module status is a structural theorem (no sorry, no axiom).
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced earlier in the RS chain. A sibling definition introduces the canonical threshold as a real constant built from $\varphi$; nearby siblings also define a domain cost and prove it nonnegative. The only upstream lemma used here is the tighter bound $\varphi>1.5$, obtained from $\sqrt{5}>2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then close by linarith using the lemma $\varphi>1.5$. No case split and no further RS lemmas are required; positivity is pure real arithmetic once the definition is expanded.
why it matters
Positivity of the canonical threshold is a local hygiene fact for the Module-7 cosmology certificate (matter-radiation equality at $z_{\mathrm{eq}}\sim\varphi^{17}\cdot 0.95\approx 3400$). It sits beside the domain-cost nonnegativity sibling and feeds the inhabited certificate bundle for this module. In the broader framework it rests on T6 ($\varphi$ forced as the self-similar fixed point) and on the $\varphi$-ladder scaling that sets cosmological redshifts. No downstream consumers are wired yet; the lemma is infrastructure for cost cutoffs rather than a headline equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.