domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost J to a mass-to-energy ratio m/e. Cosmology and ISM-dust calculations cite it as the local cost of a mass scale against a reference energy. The body is a one-line abbreviation of the standard 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 J-cost $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. Upstream modules (Cost, RefineTrigger, CoherenceCollapse) all fix this same functional: it vanishes only at ratio one and is nonnegative for $x>0$.
This file is Cosmology RS Module 11, whose structural claim is that the ISM dust fraction equals $J(\phi)^2\approx 1.39%$, matching the empirical $\sim 1%$ band. Domain cost is the local wrapper that feeds mass and energy scales into that J-cost before thresholds and certificates are applied.
proof idea
Pure definition: one-line abbreviation that evaluates the imported J-cost at the ratio $m/e$. No tactics, no lemmas, no hypotheses.
why it matters
Gives the module a named cost of a mass scale against a reference energy, so later siblings (equality at a point, nonnegativity, canonical threshold, and the RSCosmo011 certificate) can talk about domain cost without reopening the J formula. It sits under the Module 11 structural theorem that $J(\phi)^2$ reproduces the ISM dust fraction, tying the T5 J-uniqueness landmark into cosmology bookkeeping. No downstream users are wired yet; the immediate consumers are the in-module lemmas and the inhabited certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.