RotSpectraCert
plain-language theorem explainer
Certificate packing three structural hypotheses for φ-ladder rotational spectra: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical intensity threshold is strictly positive. Spectroscopists and RS auditors cite it when discharging the rotational-spectra interface. Pure structure definition; the concrete inhabitant is assembled from sibling lemmas elsewhere in the module.
Claim. A rotational-spectra certificate is a record of three facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats molecular rotational spectra in Recognition Science units. Classical levels are $E_J = J(J+1)\hbar^2/(2I)$; RS selects preferred transitions at quantum numbers $J=\varphi^n$ on the golden-ratio ladder, so the most intense lines cluster near $J_{\mathrm{peak}}\approx kT/(2hcB)\approx\varphi^n$.
Domain cost is the specialized cost functional used on this spectral domain (imported from the Cost layer and Constants). Its nonnegativity is the local avatar of the global fact that every recognition event has nonnegative cost, proved upstream via nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$. The canonical threshold is the positive cutoff that marks when a rotational line is intense enough to count as a preferred $\varphi$-ladder transition.
The certificate simply packages the three Prop-level obligations any such spectral construction must meet before downstream claims about line clustering are allowed.
proof idea
No proof body: this is a structure declaration whose three fields are propositions. Inhabitation is deferred. The sibling definition cert fills the fields by applying domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass/energy arguments), and canonicalThreshold_pos (strict positivity of the cutoff). The companion theorem then exhibits nonempty by packaging that record.
why it matters
Gives the typed interface that the module's structural theorem (status: 0 sorry, 0 axiom) must inhabit before any claim about rotational line clustering on the $\varphi$-ladder is admitted. Downstream, cert builds a concrete witness and cert_inhabited records that the type is nonempty, closing the local certificate obligation.
In the broader RS chain this sits under the $\varphi$-ladder mass/energy bookkeeping (T6 forces $\varphi$ as the self-similar fixed point) and the nonnegative J-cost calculus. It does not itself force $D=3$ or the eight-tick octave; it only certifies the cost and threshold hypotheses needed so that preferred $J=\varphi^n$ transitions can be discussed as recognition events rather than ad-hoc spectroscopic fits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.