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. It is the local cost functional used in the gap-45 structural module (minimum rung for stable self-reference at D=3). The definition is a one-line application of the unique J-cost forced by the Recognition Composition Law.
Claim. For real mass $m$ and energy scale $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 of positive ratios by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. Upstream modules record that this is the unique cost forced by the Recognition Composition Law (RCL), and that $J(x)\ge 0$ for $x>0$ with equality only at $x=1$.
This module is Foundation structural item 4 (RS gap-45). The module header states the arithmetic identity $D^2(D+2)=9\cdot 5=45$ and identifies 45 as the minimum rung for stable self-reference when spatial dimension is forced to $D=3$ (T8). Domain cost packages the J-cost of a mass-to-energy ratio so later lemmas can talk about thresholds and nonnegativity without repeating the ratio argument.
proof idea
Pure definition: one-line abbreviation that feeds the ratio $m/e$ into the already-defined J-cost functional. No tactics, no lemmas, no proof obligations.
why it matters
Gives the structural module a named cost on mass/energy pairs so sibling facts (evaluation at equality, nonnegativity, the canonical threshold, and the RS-FDN-Structural-004 certificate) can cite a single symbol. It sits under the forcing chain landmarks T5 (J-uniqueness) and T8 ($D=3$), and under the gap-45 claim that 45 is the lowest rung supporting stable self-reference in three dimensions. No downstream users are wired yet; the immediate consumers are the in-module lemmas that discharge nonnegativity and the certificate inhabitation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.