canonicalThreshold
plain-language theorem explainer
Defines the real constant $\varphi-3/2$ used as the reference cost threshold in the RS matter-radiation equality module. Cosmologists matching $z_{\mathrm{eq}}\sim 3400$ to a $\varphi$-ladder power cite it when normalizing domain cost. The body is a one-line definitional assignment from the forced golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the unique self-similar fixed point of the Recognition cost (the golden ratio).
background
The module treats matter-radiation equality redshift $z_{\mathrm{eq}}\approx 3400$ in Recognition Science units. The working match is structural: $\varphi^{17}\approx 3571$, and $\varphi^{17}\cdot 0.95\approx 3392\approx z_{\mathrm{eq}}$. Status is a structural theorem block with no sorry and no axioms.
$\varphi$ is imported from Constants: it is the T6 fixed point forced by J-uniqueness (T5), with $J(x)=(x+x^{-1})/2-1$. Domain cost (sibling domainCost) is the non-negative cost functional on the equality locus; the threshold below is the scalar against which that cost is compared when building the certificate MatterRadEqCert.
proof idea
Definitional. The value is the closed-form real $\varphi-3/2$; no tactic proof, no lemmas. Downstream positivity is handled by the sibling canonicalThreshold_pos.
why it matters
Gives the single scalar that anchors the RS matter-radiation equality certificate in this module. The parent narrative is the structural match $z_{\mathrm{eq}}\sim\varphi^{17}$ (module doc), not a full Friedmann derivation. It sits downstream of the forcing chain only through $\varphi$ itself (T6) and the J-cost import; it does not invoke T7 eight-tick or T8 $D=3$ directly. Siblings cert and cert_inhabited package the threshold into an inhabited certificate that the equality redshift lies on the $\varphi$-ladder after a fixed $0.95$ prefactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.