domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio. Cosmologists in the RS vacuum program use it when comparing domain scales to the equation-of-state bound w = −1. It is a one-line specialization of the unique J-cost functional J(x) = (x + x⁻¹)/2 − 1 to the ratio m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The Recognition Science cost functional is $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). It is the unique continuous cost forced by the Recognition Composition Law (T5 in the forcing chain). For any positive ratio not equal to one, $J$ is strictly positive; at unity it vanishes.
This module develops RS cosmology as a structural theorem package (zero sorry, zero axiom). The headline claim is that the vacuum forces $w=-1$ exactly; any DESI Y3 deviation from $w=-1$ at $2\sigma$ would falsify the framework. Current DESI reports mild tension ($w_0\approx -0.95$, $w_a\approx -0.27$) but not yet at that threshold.
Domain cost simply evaluates $J$ on a mass-to-energy ratio, giving a nonnegative scalar that measures how far a cosmological domain sits from pure vacuum balance.
proof idea
Pure definitional abbreviation: apply the already-defined recognition cost $J$ to the single ratio $m/e$. No lemmas, no tactics, no side conditions are discharged at this site. Nonnegativity and equality-at-unity are proved in sibling lemmas that unfold this definition.
why it matters
In the RS cosmology stack this is the primitive scalar against which domain thresholds and equation-of-state certificates are measured. Sibling results (domainCost_nonneg, domainCost_at_eq, canonicalThreshold, EOSDeep4Cert) build directly on it. The parent scientific claim is the vacuum forcing $w=-1$ exactly (module status: structural theorem). That claim sits downstream of T5 J-uniqueness and the Recognition Composition Law; domain cost is the local bookkeeping device that turns those abstract uniqueness facts into a concrete mass–energy comparison. No downstream theorem yet cites it outside this file, so it is presently a local primitive rather than a cross-module export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.