canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2 used as a cutoff in the J-cost treatment of matter perturbations. Cosmology proofs that bound domain cost against CMB-scale anisotropy cite it as the reference level. It is a bare definition in terms of the golden ratio from Constants; no derivation is packed into the declaration itself.
Claim. Define the canonical threshold as the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition ladder).
background
Module MatterPert4 develops a structural account of CMB temperature anisotropy from the Recognition J-cost. The module status line records a zero-sorry theorem stack and the order-of-magnitude match $\Delta T/T \sim 10^{-5}$ against $J(\varphi)^{D+1} = J(\varphi)^4 \approx 1.94\times 10^{-4}$.
Here $J$ is the unique cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law, and $\varphi$ is the golden ratio fixed by T6 of the forcing chain. Spatial dimension $D=3$ (T8) supplies the exponent four on $J(\varphi)$. The threshold $\varphi-3/2$ sits beside sibling domain-cost definitions that measure how far a perturbation sits above this cutoff.
proof idea
No proof: the declaration is a one-line real constant, $\varphi - 3/2$, read from Constants. Positivity and any comparison lemmas live in sibling declarations (e.g. canonicalThreshold_pos), not here.
why it matters
Gives the numerical hinge for the MatterPert4 domain-cost story: fluctuations are scored relative to $\varphi-3/2$ before being compared with the $J(\varphi)^4$ anisotropy scale. That scale is the module's bridge from the forcing chain (T5 J-uniqueness, T6 $\varphi$, T8 $D=3$) to the observed $\Delta T/T\sim 10^{-5}$ band. Downstream certificate objects in the same file (MatterPert4Cert and friends) package the structural claim; this constant is the named cutoff those certificates and domainCost lemmas refer to. It does not itself close an open physics derivation; it freezes the RS-native threshold so the rest of the stack can stay sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.