canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2, with φ the RS golden ratio. It is the cutoff used when comparing domain cost to the CMB damping-scale window (φ^15 to φ^16). Cosmologists citing the v3 damping certificate use it as the fixed comparison level. The declaration is a bare definitional constant, not a derived equality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio (the unique positive self-similar fixed point of the Recognition cost).
background
Recognition Science forces a unique dimensionless cost $J$ and a unique self-similar scale $\varphi$ (forcing chain T5–T6). In RS-native units the CMB damping multipole is read off the $\varphi$-ladder: $\varphi^{15}\approx 1364$ and $\varphi^{16}\approx 2207$, bracketing the observed $l_D\sim 1500$–$2000$ window.
This module packages that ladder reading as a structural certificate (zero sorry, zero axiom). Sibling definitions introduce a nonnegative domain cost on the same scale; the present constant supplies the fixed real level against which that cost is compared.
Imports are only Mathlib, Constants (for $\varphi$), and Cost (for $J$). No upstream lemma is required: the value is written directly as $\varphi-3/2$.
proof idea
Definitional abbreviation. The body is the single real expression phi - 3/2; there is no tactic proof, no lemma application, and no hypothesis. Downstream positivity or comparison lemmas simply unfold this constant.
why it matters
Gives the numerical hinge of the v3 CMB damping-scale certificate. The module status line records a structural theorem with $l_D$ identified with the $\varphi^{15}$–$\varphi^{16}$ band; the threshold $\varphi-3/2$ is the comparison level used by the sibling domain-cost predicates and by CMBDampingScale_v3Cert.
In the broader framework it sits downstream of T6 ($\varphi$ forced) and of the eight-tick / ladder bookkeeping that places cosmological scales on integer rungs. It does not itself re-derive $\varphi$ or the rung indices; it freezes the cutoff so the certificate can stay sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.