domainCost
plain-language theorem explainer
The domain cost of a mass m against an energy scale e is the recognition cost of their ratio. Calibration and forcing-chain work cite it as the local mismatch cost between a mass and the coherence energy. The definition is a one-line abbreviation: apply the standard J-cost to m/e.
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 measures mismatch by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream modules record that $J$ is the unique cost forced by the Recognition Composition Law, and that a genuine distinction (ratio not one) has strictly positive cost.
This module is Foundation RS Module 10: structural calibration in which the coherence energy $E_{\mathrm{coh}}$ is the single free parameter, fixed by the electron mass at rung 3 on the $\varphi$-ladder. Domain cost specializes $J$ to the ratio of a mass to an energy scale, the natural local cost in that calibration setting.
proof idea
Pure definitional abbreviation. The body is the single application of the upstream $J$-cost functional to the ratio $m/e$; no lemmas or tactics are involved.
why it matters
Gives the local cost functional used throughout Module 10's calibration story: how far a mass sits from the coherence energy scale. Sibling facts (non-negativity of domain cost, equality at matched scales, the canonical threshold and its positivity) build directly on this abbreviation. In the broader forcing chain it sits under T5 J-uniqueness: once $J$ is forced, every domain mismatch is measured by the same functional. The module status is structural (zero sorry, zero axiom), so this def is part of the closed calibration layer rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.