domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio. Structural gravity arguments in the gap-45 module use it as the local cost of placing mass m against energy scale e. The body is a one-line abbreviation of 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 forces a unique cost on positive ratios: $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. Upstream modules record that $J$ is the unique functional satisfying the Recognition Composition Law, and that $J(x)\ge 0$ for $x>0$ with equality only at $x=1$.
This module is Gravity RS Structural Module 4. Its theme is the RS gap-45 identity $D^2(D+2)=9\cdot 5=45$, the minimum rung for stable self-reference at spatial dimension $D=3$ (forcing chain T8). Domain cost is the local scalar that measures how far a mass–energy ratio sits from the unit-cost fixed point of $J$.
Notation: $m$ is a mass-like scale and $e$ an energy-like scale in RS-native units; their ratio is fed to $J$ without further normalization at this definition site.
proof idea
Pure definition: one-line abbreviation that applies the upstream $J$-cost functional to the ratio $m/e$. No tactics, no lemmas, no proof obligations.
why it matters
Gives the gravity stack a named scalar for the recognition cost of a mass–energy mismatch, aligned with T5 J-uniqueness and the RCL. Sibling results in the same module (nonnegativity of domain cost, equality at unit ratio, the canonical threshold, and the RSGRVStructural004 certificate) build on this abbreviation. The module status is structural theorem with zero sorry and zero axiom; gap-45 and the $D=3$ self-reference rung are the parent structural claims this cost is meant to support. No downstream uses are recorded yet outside the module siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.