domainCost
plain-language theorem explainer
Domain cost assigns to a mass-energy pair the recognition cost of their ratio. Module-6 Higgs-VEV work cites it as the local cost on m/e. The body is a one-line abbreviation of the standard J-cost at that ratio.
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 a positive scale ratio by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream definitions in Cost, Cosmology.RefineTrigger, and Gravity.CoherenceCollapse all fix this same functional; the Cosmology doc calls it "the RS recognition cost of a positive ratio," and CoherenceCollapse records that $J$ is nonnegative for positive $x$.
Physics RS Module 6 treats the Higgs VEV ratio $v/M_Z\approx 246/91.2\approx 2.70$ against $\phi^2\approx 2.618$ (about 3% off) as a structural comparison. Domain cost is the module-local name for $J$ evaluated on a mass-to-energy (or mass-to-mass) ratio in that setting.
The forcing chain identifies $J$ uniquely at T5 via the Recognition Composition Law, so every later cost comparison inherits that uniqueness.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally Jcost (m / e). No tactics, no lemmas, no proof obligations.
why it matters
Gives Module 6 a named cost on mass-energy ratios so the Higgs VEV comparison can be stated in RS-native language rather than raw $J$. Sibling facts (domainCost_at_eq, domainCost_nonneg) and the module certificate RSPhysics006Cert sit on top of this abbreviation. It inherits T5 J-uniqueness and the RCL shape of $J$, and it is the cost side of the structural claim that $v/M_Z$ sits near $\phi^2$. No downstream theorems are wired yet (used_by is empty); the immediate consumers are the nonnegativity and equality lemmas in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.