domainCost
plain-language theorem explainer
The domain cost of a mass m at energy scale e is the recognition cost J of the ratio m/e. Anyone matching particle masses on the phi-ladder in RS Physics Module 12 (W boson) uses this as the local cost functional. It is a one-line abbreviation of the standard J-cost, not a derived identity.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
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 (Cost, Cosmology.RefineTrigger, Gravity.CoherenceCollapse) all fix this same functional: it vanishes only at $x=1$ and is nonnegative for $x>0$.
This module (Physics RS Module 12) targets the W-boson mass match $M_W\approx 80.4,\mathrm{GeV}\sim\phi^{13}\cdot 0.154$. Domain cost specializes J to a mass-over-energy ratio, the natural dimensionless input when a mass sits against a reference energy scale on the phi-ladder.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally Jcost (m / e). No lemmas, tactics, or proof obligations.
why it matters
Gives Module 12 a named cost on mass-energy ratios so later facts (nonnegativity, evaluation at equality, canonical thresholds, and the RSPhysics012Cert bundle among the siblings) can speak about W-boson matching without reopening the J formula. Ties directly to the T5 J-uniqueness landmark: the same forced cost that appears in the forcing chain is the one used for the structural W-mass claim. No downstream theorems yet list this def as a dependency; it is infrastructure for the module certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.