canonicalThreshold
plain-language theorem explainer
Defines the canonical reionization threshold as $\varphi - 3/2$ in RS-native units. Cosmology modules cite it as the structural cutoff against which domain cost is compared for the $\varphi^4$–$\varphi^5$ reionization window. The body is a one-line arithmetic definition from the golden ratio constant.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of the Recognition self-similarity relation.
background
RS Cosmology Module 8 treats reionization as a structural match: the interval $\varphi^4$ to $\varphi^5$ (numerically about $6.85$–$11.09$) is identified with the observed reionization redshift window $z_{\mathrm{reion}}\sim 7$–$10$. The module is marked as a structural theorem with no sorry and no extra axioms.
The golden ratio $\varphi$ enters from the forcing chain (T6): it is the unique self-similar fixed point forced by the J-cost calculus. Constants live in the shared Constants import; cost primitives come from Cost. Sibling definitions introduce a domain cost functional and prove it is nonnegative, so a positive numerical threshold is the natural comparison scale.
proof idea
Pure definition: the real constant is introduced by the arithmetic expression $\varphi - 3/2$. No lemmas are applied and no tactics run. Downstream positivity (canonicalThreshold_pos) is a separate one-line inequality on this value.
why it matters
Gives the module a single named cutoff for the reionization structural claim. In the broader RS framework it sits next to other $\varphi$-ladder thresholds (Berry creation at $\varphi^{-1}$, $Z_{\mathrm{cf}}=\varphi^5\in(11,12)$). The parent certificate objects in this file (RSCosmo008Cert, cert, cert_inhabited) package the match $\varphi^4$–$\varphi^5\leftrightarrow z_{\mathrm{reion}},7$–$10$; this constant is the comparison scale those certificates rely on when domain cost is evaluated. It does not itself force dimension or the eight-tick octave; those are upstream (T7, T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.