domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair $(m,e)$ the recognition cost of their ratio $m/e$. Cosmology proofs that need a nonnegative scalar measuring how far a mass sits from an energy scale cite this abbreviation. It is a one-line wrapper around the forced J-cost functional.
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
Recognition Science measures mismatch of positive ratios by the unique cost $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. Upstream modules (Cost, RefineTrigger, CoherenceCollapse, EnergyProcessingBridge) all fix this same functional; it is forced by the Recognition Composition Law and appears as T5 in the forcing chain.
This module is Cosmology Structural 4. Its header states the RS gap-45 identity $D^2(D+2)=9\cdot 5=45$ and identifies 45 as the minimum rung for stable self-reference when spatial dimension is $D=3$ (T8). Domain cost supplies the scalar that later certificates compare against a canonical threshold on that rung ladder.
proof idea
Pure definitional abbreviation: apply the imported J-cost to the quotient $m/e$. No tactics, no lemmas, no side conditions at the definition site. Nonnegativity and evaluation identities live in sibling lemmas.
why it matters
Gives the cosmology layer a uniform name for "how expensive is this mass relative to this energy scale" without reopening the J-uniqueness argument. The module status is structural theorem (zero sorry, zero axiom) and sits on the gap-45 / $D=3$ self-reference story. Downstream certificates in the same file (canonical threshold positivity, the RS-COS-Structural-004 cert) are the natural consumers; the used-by graph is currently empty at export time, so the def is infrastructure for those siblings rather than a finished bridge theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.