domainCost
plain-language theorem explainer
The domain cost of a mass–energy pair is the recognition cost of their ratio m/e. Rotational-spectra arguments on the φ-ladder cite it as the local cost on (m,e). It is a one-line abbreviation of the unique J-cost applied to that ratio.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
The module treats molecular rotational spectra from the φ-ladder. Classically $E_J=J(J+1)\hbar^2/(2I)$; in RS the preferred transitions sit at quantum numbers $J=\phi^n$, so intense lines cluster near $J_{\mathrm{peak}}\approx kT/(2hcB)\approx\phi^n$.
The recognition cost $J(x)=\frac{x+x^{-1}}{2}-1$ is the unique functional forced by the Recognition Composition Law (forcing chain T5). It vanishes only at ratio one and is nonnegative for positive arguments. Upstream modules define the same $J$ under the name Jcost.
Domain cost specializes $J$ to a mass-to-energy ratio, the natural dimensionless input for the spectra setting.
proof idea
Definitional abbreviation only: domain cost of $(m,e)$ is exactly $J(m/e)$. No lemmas, no tactics, no proof obligations.
why it matters
Gives the module a named cost on the $(m,e)$ domain used by the rotational-spectra certification path (siblings: nonnegativity of domain cost, the canonical threshold, and the RotSpectraCert bundle). Anchors the spectra story to T5 J-uniqueness and the RCL-forced cost, so later claims about preferred $\phi^n$ transitions measure mismatch in the same units as the rest of the monolith. No external used-by edges yet; the immediate consumers are in-module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.