domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the RS J-cost of m/e. Gravity and structural-bridge arguments cite it whenever a dimensionless mismatch between mass and energy scales must be scored. The body is a one-line abbreviation of the unique T5 cost functional applied to that ratio.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=(x+x^{-1})/2-1$ is the Recognition Science cost of a positive ratio.
background
Recognition Science scores dimensionless mismatches with the unique cost $J(x)=(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge) all fix this same $J$; EnergyProcessingBridge notes it is forced by the Recognition Composition Law, matching forcing-chain step T5.
This module is Gravity RS Structural Module 9: the local setting is the structural forcing chain T5 (J-uniqueness) through T8 ($D=3$), with status structural theorem (zero sorry, zero axiom). Domain cost simply specializes $J$ to the mass-over-energy ratio that appears in gravitational and energy-processing comparisons.
Sibling facts in the same file (non-negativity, evaluation identities, a canonical threshold) treat this definition as the primitive cost of a domain mismatch.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally equal to Jcost (m / e). No tactics, no lemmas, no side conditions are discharged at this site; all analytic content lives in properties of $J$ proved elsewhere.
why it matters
Gives the gravity stack a named, reusable cost for mass-energy domain mismatch instead of inlining $J(m/e)$ at every call site. It sits on the T5 landmark (unique J forced by RCL) inside the module's stated chain T5→T6→T7→T8. Downstream siblings such as non-negativity and the structural certificate package (RSGRVStructural009Cert) are built on this abbreviation; the used-by list is currently empty at the graph edge level, so its role is local scaffolding for those certificate lemmas rather than a cross-module export yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.