domainCost
plain-language theorem explainer
Domain cost maps a mass-energy pair to the recognition cost of their ratio. RS QCD and ladder calculations cite it as the local cost on (m,e). It is a one-line specialization of the unique J-cost to the dimensionless argument 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 scores mismatch of positive ratios by the J-cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). Upstream modules define this same functional as the RS recognition cost of a positive ratio; it is the unique cost forced by the Recognition Composition Law (forcing-chain T5).
Physics RS Module 5 packages structural results for the one-loop QCD coefficient $b_0=7=2^D-1$, identified with the Count Law once spatial dimension is fixed at $D=3$. Domain cost is the specialization of $J$ to a mass-over-energy ratio, the natural dimensionless input when a mass scale is compared to an energy scale on the RS ladder.
proof idea
Definitional abbreviation only: the value on $(m,e)$ is exactly $J(m/e)$. No lemmas, tactics, or proof obligations.
why it matters
Infrastructure inside Physics RS Module 5, whose structural claim is that the QCD one-loop coefficient equals 7 by the Count Law in $D=3$. Sibling facts (evaluation at equality, nonnegativity, canonical threshold, and the module certificate) build on this cost. The dependency graph shows no external used-by edges, so the declaration is local scaffolding for the module cert rather than a leaf of the global forcing chain. It inherits uniqueness of $J$ from T5 and sits next to the $D=3$ Count-Law step (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.