canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as φ − 3/2 in RS-native units. Cosmology and cost-layer arguments cite it as the fixed numerical cut used beside domain cost. The body is a one-line definitional abbreviation of that combination of the golden ratio and the rational 3/2.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio fixed by the RS self-similarity equation.
background
RS Cosmology Module 7 treats matter–radiation equality as a structural match: $\varphi^{17}\cdot 0.95$ is identified with $z_{\mathrm{eq}}\sim 3400$, in line with the empirical value, under a zero-sorry, zero-axiom certificate.
The module imports the global RS constants (including $\varphi$) and the cost layer. In the forcing chain, $\varphi$ is the unique self-similar fixed point (T6) tied to the J-cost $J(x)=(x+x^{-1})/2-1$. Sibling definitions package a domain cost and its nonnegativity; this constant supplies a single named real cut built from $\varphi$ and the rational offset $3/2$.
proof idea
No proof obligations. The declaration is a definitional abbreviation: the identifier is bound to the real expression $\varphi - 3/2$ with no tactics, lemmas, or rewriting.
why it matters
Gives Module 7 a stable named threshold so cost and certificate siblings can refer to one RS-native cut rather than an inline combination of $\varphi$ and $3/2$. It sits in the cosmology domain next to the matter–radiation equality match ($\varphi^{17}\cdot 0.95\approx z_{\mathrm{eq}}$) and the structural certificate for the module. It does not itself close a forcing-chain step (T0–T8); it is infrastructure for threshold comparisons in the cost layer of this cosmology package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.