domainCost
plain-language theorem explainer
Domain cost assigns to a mass scale m and energy scale e the recognition cost of their ratio m/e. Gravity structural arguments use it as the local mismatch cost once E_coh is fixed by the electron mass. The definition is the direct specialization of the unique J-cost functional to that ratio.
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 the same functional (T5 J-uniqueness) and note that any genuine distinction ($x\neq 1$) has strictly positive cost, with $J\ge 0$ on positives.
This module is Gravity RS Structural 10: $E_{\mathrm{coh}}$ is calibrated once from the electron mass, after which predictions are parameter-free. Domain cost is the local specialization of $J$ to a mass-over-energy ratio, the natural mismatch measure between a mass scale $m$ and an energy scale $e$ in that calibrated setting.
proof idea
One-line definition: apply the shared $J$-cost functional to the ratio $m/e$. No lemmas or tactics; the body is exactly $J(m/e)$.
why it matters
Gives the gravity stack a named cost on mass-energy ratios once coherence energy is fixed by the electron. Sibling facts (nonnegativity, evaluation identities, the canonical threshold and the structural certificate) sit on this definition. It is the local instance of the T5-forced $J$ inside the RS gravity calibration story, not a new functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.