canonicalThreshold
plain-language theorem explainer
Defines the canonical intensity threshold as φ − 3/2 for rotational line selection on the φ-ladder. Spectroscopists and RS auditors cite it when marking which J-levels count as preferred transitions. It is a bare real constant, not a proved inequality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition cost).
background
The module treats molecular rotational spectra in Recognition Science units. Classical rigid-rotor levels are $E_J = J(J+1)\hbar^2/(2I)$. RS selects preferred transitions at quantum numbers $J = \varphi^n$ on the φ-ladder, so the strongest lines cluster near $J_{\mathrm{peak}} \approx kT/(2hcB) \approx \varphi^n$.
Here $\varphi$ is the unique positive fixed point forced by the J-cost self-similarity (T6 in the forcing chain). The sibling domainCost packages a non-negative cost on the rotational domain; this threshold is the numerical cut used with that cost to decide which lines are canonical.
proof idea
Pure definitional abbreviation: the real constant $\varphi - 3/2$ is named and exposed. No tactics, no lemmas, no proof obligations.
why it matters
Gives a single named cut for the structural rotational-spectra certificate in this module (siblings RotSpectraCert, cert, canonicalThreshold_pos). In the RS picture, preferred $J=\varphi^n$ lines sit above a cost floor tied to the golden ratio; $\varphi-3/2$ is that floor in native units. It sits downstream of T6 (φ forced) and the eight-tick / ladder infrastructure, and upstream of any claim that the most intense rotational multiplet is the one nearest a φ-power. Status is structural (0 sorry): the number is fixed; positivity and certificate packing live in the sibling lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.