canonicalThreshold
plain-language theorem explainer
Defines the canonical energy threshold as φ − 3/2, which is exactly the J-cost of the golden ratio, J(φ). Anyone working the RS recognition spectrum or the first excited rung cites this constant. It is a bare real abbreviation, not a proved identity.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio fixed by self-similarity. Equivalently it equals the J-cost $J(\varphi) = (\varphi + \varphi^{-1})/2 - 1$.
background
The module builds the recognition spectrum of $H_{RS}$ on the $\varphi$-ladder: levels $E_n = J(\varphi^n),\hbar_R,\omega_0$ for $n = 0,1,2,\ldots$, with ground state $E_0 = 0$ and first excited state the recognition quantum $E_1 = J(\varphi),\hbar_R,\omega_0$.
The cost $J$ is the unique symmetric generator forced by the Recognition Composition Law (T5): $J(x) = (x + x^{-1})/2 - 1$. Because $\varphi$ satisfies $\varphi^{-1} = \varphi - 1$, one has $J(\varphi) = \varphi - 3/2$ by direct algebra. The constant $\varphi$ itself is the self-similar fixed point forced at T6.
Sibling definitions package the domain cost on the ladder and a certificate that the spectrum is well-formed; positivity of this threshold is recorded separately.
proof idea
Pure definitional abbreviation: the real is set equal to $\varphi - 3/2$. No tactics, no lemmas. The equality with $J(\varphi)$ is the elementary expansion of the closed form of $J$ at the golden ratio and is left implicit for downstream lemmas.
why it matters
Pins the numerical value of the recognition quantum that opens the RS spectrum. Module status is structural (0 sorry, 0 axiom): the first excited rung is exactly this threshold times $\hbar_R\omega_0$. Downstream certificates (RecogSpectrum3Cert and inhabitants) and positivity lemmas sit on top of the constant. In the forcing chain it sits at the junction of T5 (J-uniqueness) and T6 ($\varphi$ fixed point), and it is the concrete energy scale against which Berry-threshold and higher-rung mass formulae are compared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.