canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold φ − 3/2 used in the CMB-from-J-cost module. Cosmologists and RS auditors cite it when comparing domain cost against a fixed cutoff tied to the golden ratio. The body is a one-line real abbreviation; no proof obligations.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio fixed by the Recognition self-similarity equation.
background
The module derives the CMB temperature structurally from the phi-ladder: $T_{\mathrm{CMB}}/T_{\mathrm{vac}}=\varphi^{-k}$ with $T_{\mathrm{vac}}$ at the Planck scale and rung $k=196$, recovering $T_{\mathrm{CMB}}\approx 2.73,\mathrm{K}$ against the observed $2.725,\mathrm{K}$. Status is structural (zero sorry, zero axiom).
Recognition Science forces $\varphi$ as the unique self-similar fixed point (forcing chain T6) and the cost functional $J(x)=(x+x^{-1})/2-1$. Sibling definitions in this file introduce a domain cost built from $J$ and prove it nonnegative. The threshold $\varphi-3/2$ sits slightly above zero ($\varphi\approx 1.618$) and supplies a fixed positive cutoff against which that cost is compared when certifying the temperature match.
proof idea
Pure definition: the real constant is introduced by the abbreviation $\varphi - 3/2$. No tactics, no lemmas, no reduction. Downstream positivity is handled by the sibling canonicalThreshold_pos.
why it matters
Gives a named, reusable cutoff inside the CMB temperature certificate path (siblings CMBTemp3v2Cert, cert, cert_inhabited). The module claims a structural derivation of $T_{\mathrm{CMB}}$ from the phi-ladder rather than a fitted parameter. The threshold links the J-cost comparison to the same $\varphi$ forced by T5–T6 and used in the mass ladder and eight-tick octave. It does not itself prove the temperature identity; it only anchors the numerical gate used by the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.