domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the recognition cost J(m/e). Gravity and structural RS modules use it as the scalar cost of a mass scale relative to an energy scale. The body is a one-line abbreviation of the unique J-cost on the positive ratio m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x) = \frac{1}{2}(x + x^{-1}) - 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 (Cost, CoherenceCollapse, EnergyProcessingBridge) all pin this same functional; EnergyProcessingBridge notes it is the unique cost forced by the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
This module is Gravity RS Structural Module 6, whose stated theme is RS phi uniqueness (the self-similar fixed point $\varphi = 1 + 1/(1+1/(1+\cdots))$). Domain cost packages $J$ on a mass-over-energy ratio so later structural lemmas can talk about nonnegativity and thresholds without repeating the ratio argument.
proof idea
Pure definitional abbreviation: apply the shared $J$-cost to the ratio $m/e$. No tactics, no lemmas, no proof obligations.
why it matters
Gives the gravity stack a named scalar for how costly a mass scale is relative to an energy scale under the forced $J$. Siblings in the same file (domainCost_nonneg, domainCost_at_eq, canonicalThreshold) build nonnegativity and threshold facts on top of it; the module certificate RSGRVStructural006Cert sits in that structural layer.
Framework landmark: $J$ is the T5 uniqueness result in the forcing chain, and the unique solution of the Recognition Composition Law. Packaging $J(m/e)$ keeps mass/energy comparisons inside that forced cost rather than an ad hoc metric. No downstream edges are recorded yet; the def is local scaffolding for the module's structural theorems on phi uniqueness and gravity thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.