cert
plain-language theorem explainer
Packages the three algebraic facts needed to certify φ-ladder rotational spectra: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical intensity threshold is positive. Spectroscopists or RS auditors cite it as the inhabited certificate object for the module. The definition is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate object asserting: (i) for every nonzero real $r$, the domain cost of matching $r$ to itself is zero; (ii) for all positive reals $m,e$, the domain cost of $m$ against $e$ is nonnegative; (iii) the canonical intensity 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 prefers transitions whose angular-momentum quantum numbers sit on the $\varphi$-ladder, so the strongest lines cluster near $J_{\mathrm{peak}}\approx kT/(2hcB)\approx\varphi^n$.
Domain cost is the local cost functional comparing a measured rung $m$ to an expected rung $e$. The certificate structure RotSpectraCert packages three elementary properties of that cost and of the canonical intensity threshold: diagonal vanishing, nonnegativity, and a positive cutoff. Upstream, nonnegativity of recognition cost is already forced by the J-cost minimum ($J(x)\ge 0$ with equality at $x=1$).
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work occurs.
why it matters
Gives the module a single named certificate that the φ-ladder rotational-spectra story is algebraically well-posed: cost is a genuine defect (zero only on match, nonnegative otherwise) and the intensity gate is nontrivial. That matches the module status line (structural theorem, zero sorry). No downstream consumers are recorded yet; the natural parent is any theorem that assumes an inhabited RotSpectraCert when deriving preferred $J=\varphi^n$ lines or the peak clustering $J_{\mathrm{peak}}\approx\varphi^n$. Ties to the broader RS ladder (T6 φ fixed point, mass/rung formulas) only as the spectral application layer, not as a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.