canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2, with φ the golden-ratio fixed point of the Recognition cost. Module-12 cosmology certificates compare domain costs against this scale when treating the Li-7 Spite plateau band. Anyone citing the structural RS_PASS claim for that plateau needs the constant as a named yardstick. The declaration is a bare definition with no proof body.
Claim. Define the canonical threshold by $T_{\mathrm{can}}:=\varphi-\frac{3}{2}$, where $\varphi>1$ is the unique positive self-similar fixed point forced by the Recognition cost (the golden ratio).
background
Recognition Science fixes a unique dimensionless cost $J$ on positive reals (T5: $J(x)=(x+x^{-1})/2-1$) and forces $\varphi$ as its self-similar fixed point (T6). Constants throughout the monolith are expressed in $\varphi$-native units; the present module imports those constants together with the cost layer.
This file is Cosmology RS Module 12. Its module brief states the Li-7 Spite plateau target: RS band $(4.69,4.86)\times 10^{-10}$ against observed $(4.0,5.2)\times 10^{-10}$, status STRUCTURAL THEOREM (0 sorry, 0 axiom). Sibling definitions introduce a nonnegative domain cost and a positivity lemma for the threshold itself; the threshold is the comparison scale those objects use.
proof idea
Bare definition: the name is bound to the closed-form real $\varphi-3/2$. No tactics, no lemmas, no proof obligations. Downstream positivity and certificate lemmas unfold this equality.
why it matters
Gives Module 12 a single named real against which domain costs are measured when certifying the Li-7 Spite plateau band. The module claims an RS_PASS structural match of the RS interval $(4.69,4.86)\times 10^{-10}$ to the observed window; the threshold is the local yardstick those comparisons cite. It sits downstream of the forcing-chain landmarks T5–T6 ($J$-uniqueness and $\varphi$) and upstream of the module certificate and its inhabited proof. No open scaffold: the status line reports zero sorry and zero axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.