domainCost
plain-language theorem explainer
Domain cost of a mass m against an energy scale e is the recognition cost of their ratio. Module 11 (Z-boson mass match) uses it as the local cost functional on mass-to-scale ratios. The body is a one-line abbreviation of the standard J-cost applied 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 of positive ratios by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream definitions state that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive arguments. The same functional appears in the forcing chain as the unique cost satisfying the Recognition Composition Law.
This module is Physics RS Module 11: the structural claim that the Z boson mass matches $M_Z\approx 91.2,\mathrm{GeV}\sim\phi^{13}\cdot 0.175$. Domain cost supplies the local cost of a mass relative to a chosen energy scale inside that match.
proof idea
Pure definition: apply the imported J-cost to the ratio $m/e$. No proof obligations; the body is the abbreviation $J(m/e)$.
why it matters
Gives Module 11 a named cost on mass-to-scale ratios so later lemmas (nonnegativity, evaluation at equality, canonical threshold) can speak about domain cost rather than raw $J$. That supports the structural Z-mass match $M_Z\sim\phi^{13}\cdot 0.175$ without axioms or sorries. In the broader framework it is the same T5 J-cost used on the phi-ladder mass formula, specialized to a two-argument domain form. No external parents yet; it is infrastructure for the module certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.