domainCost
plain-language theorem explainer
Domain cost is the recognition cost of a mass-to-energy ratio: J(m/e) with the unique RS cost J. Gravity structural proofs cite it as the local imbalance cost on a domain. The body is a one-line specialization of Jcost to the ratio m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac12(x+x^{-1})-1$ is the recognition cost of a positive ratio.
background
The module is Gravity RS Structural Module 1: structural predictions with J forced as $\frac12(x+1/x)-1$, $\phi$ the golden ratio, and $D=3$, status zero sorry and zero axiom.
The recognition cost $J$ is the unique functional forced by the Recognition Composition Law (T5 in the forcing chain). Upstream definitions write $J(x)=\frac12(x+x^{-1})-1$ and record that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive $x$.
Here the cost is applied to a mass-energy ratio $m/e$, the natural dimensionless argument when comparing a domain mass scale to an energy scale in the RS gravity layer.
proof idea
Pure definition: one-line wrapper that feeds the ratio $m/e$ into the standard $J$-cost. No tactics, no lemmas, no side conditions in the body.
why it matters
Gives the gravity module a named cost of domain imbalance so later structural facts (nonnegativity, equality cases, canonical thresholds) can quote a single symbol rather than raw $J(m/e)$. That sits under T5 $J$-uniqueness and the RCL, the same cost that appears across cosmology, coherence collapse, and energy-processing bridges.
Siblings in this file build on it: equality at matched scales, nonnegativity, and the canonical threshold certificate for RS-GRV structural claim 001. No external used-by edges are recorded yet; the immediate consumers are those in-module lemmas and the structural certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.