domainCost
plain-language theorem explainer
Domain cost assigns the RS recognition cost J to the dimensionless ratio of a mass parameter m to an energy scale e. Anyone working the strong-CP or theta-sector arguments in Module 8 cites it as the local cost of a mass/energy mismatch. The body 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 the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$ for $x>0$).
background
Recognition Science measures mismatch by the unique cost functional forced at T5: $J(x)=\frac{x+x^{-1}}{2}-1$. Upstream definitions state this as "the RS recognition cost of a positive ratio" and note that a genuine distinction (ratio not one) has strictly positive cost; $J$ is nonnegative on positives.
Module 8 is the structural treatment of QCD $\theta=0$ from eight-tick uniqueness (the strong-CP problem solved without a dynamical axion). In that setting one repeatedly needs the cost of a mass relative to a reference energy; domainCost packages exactly that ratio cost.
Notation is RS-native: $c=1$, costs live on positive reals, and the same $J$ appears in the Recognition Composition Law and the forcing chain.
proof idea
Pure definitional abbreviation. The right-hand side is the shared Jcost from Cost (and the identical Cosmology/Gravity copies): evaluate $J$ at the single argument $m/e$. No lemmas, no tactics, no hypotheses.
why it matters
Gives Module 8 a named hook for "how expensive is this mass relative to this energy scale" before nonnegativity and threshold lemmas (domainCost_nonneg, canonicalThreshold, the RSPhysics008Cert certificate). That cost language sits inside the structural $\theta=0$ argument driven by eight-tick uniqueness (T7) and the unique $J$ (T5). Even with no recorded downstream edges yet, the sibling certificate cluster shows the intended landing: certify that domain costs sit above a positive canonical threshold so unwanted CP-odd sectors are recognition-forbidden.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.