canonicalThreshold
plain-language theorem explainer
Defines the real number φ − 3/2 as the canonical threshold used in this cosmology module. Anyone citing RS spectral-index or domain-cost comparisons against a fixed cutoff would reference it. The body is a one-line constant definition in terms of the golden ratio.
Claim. The canonical threshold is the real constant $\varphi - 3/2$, where $\varphi$ is the golden ratio fixed by the Recognition self-similarity equation.
background
Module RS_Cosmo_Module_004 sits in the Recognition Science cosmology layer. Its headline target is the scalar spectral index $n_s = 1 - 2/45 \approx 0.9556$, compared with the Planck value $0.9649$ (about $2.2\sigma$ tension); the module is marked OPEN on that empirical match but STRUCTURAL on the Lean side (zero sorry, zero axiom).
The only external constants needed here come from Constants and Cost: $\varphi$ is the unique positive fixed point of the self-similarity relation forced at T6 of the unified forcing chain, and the J-cost $J(x) = (x+x^{-1})/2 - 1$ supplies the non-negative domain cost used by sibling lemmas. The threshold itself is a pure real combination of $\varphi$ and the rational $3/2$.
proof idea
Pure definition: the right-hand side is the arithmetic expression $\varphi - 3/2$ at type $\mathbb{R}$. No lemmas, tactics, or proof terms are involved.
why it matters
Gives a named, reusable cutoff built from the same $\varphi$ that appears throughout RS (T6 fixed point, mass ladder, Berry threshold $\varphi^{-1}$, etc.). Sibling facts in the module establish positivity of this threshold and non-negativity of the domain cost, so later certificates (e.g. RSCosmo004Cert) can compare costs against a fixed positive scale without re-deriving $\varphi - 3/2$. It does not itself close the $n_s$ tension with Planck; that remains the OPEN empirical question flagged in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.