domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio: J(m/e). It is the local cost functional used in the gap-45 forcing module (g_D = 45 at D = 3). Anyone citing RS structural cost on mass/energy scales will use it. The body is a one-line abbreviation of the standard J-cost.
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 measures mismatch of positive ratios by the J-cost $J(x) = \frac{x + x^{-1}}{2} - 1$, equivalently $\cosh(\log x) - 1$. It vanishes only at $x = 1$ and is nonnegative for $x > 0$. Upstream modules (Cost, Cosmology.RefineTrigger, Gravity.CoherenceCollapse) all fix this same functional.
This module is Foundation RS Module 3: the structural gap $g_D = D^2(D+2) = 45$ at $D = 3$, the minimum depth for self-reference. Domain cost specializes $J$ to a mass–energy ratio $m/e$, the natural scale pair in that forcing setting. Status is structural (0 sorry, 0 axiom).
proof idea
Pure definition: domain cost is the abbreviation $J(m/e)$. No proof obligations; the body is the single application of the shared J-cost functional to the ratio of the two real arguments.
why it matters
Gives the module a named cost on mass/energy pairs so later lemmas (nonnegativity, evaluation identities, canonical threshold) can cite a single symbol rather than raw $J(m/e)$. It sits inside the T5–T8 forcing landscape: J-uniqueness, $\phi$ as self-similar fixed point, eight-tick octave, and $D = 3$. The module headline is gap-45 at three spatial dimensions; domain cost is the cost primitive that gap arguments act on. No downstream theorems are wired yet in the graph, so its immediate role is local scaffolding for the Module 3 certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.