domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost of a mass-to-energy ratio m/e by evaluating the unique J-cost on that ratio. Cosmology and dark-matter mass ladder work cite it as the local cost of a domain scale relative to an energy reference. The body is a one-line definitional wrapper around J.
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 record that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative on positive arguments. That functional is forced uniquely by the Recognition Composition Law in the T5 step of the forcing chain.
This module is Cosmology RS Module 6: a structural, zero-sorry package aimed at a dark-matter mass scale $M_W/45\approx 1.787,\mathrm{GeV}$ and a XENONnT-facing falsifier. Domain cost is the local cost of a mass scale $m$ measured against an energy reference $e$, written as $J$ of their ratio.
proof idea
Definitional one-liner: apply the shared J-cost functional to the ratio $m/e$. No tactics, lemmas, or side conditions appear in the body; nonnegativity and evaluation identities are left to sibling lemmas.
why it matters
Gives the cosmology module a named cost for mass-versus-energy domain ratios, so later certificates can talk about thresholds without reopening the definition of $J$. Siblings such as nonnegativity of domain cost and the canonical threshold sit on top of this abbreviation. In the broader RS picture it is the same T5 J used for ladder masses and coherence collapse, specialized here to the Module-6 DM-mass and XENONnT test narrative. No downstream theorems are wired yet in the graph; the definition is infrastructure for those certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.