domainCost
plain-language theorem explainer
Domain cost of a mass m against an energy scale e is the recognition cost of the positive ratio m/e. Standard Model structural calibrations cite it when masses are measured against the electron-fixed coherence energy. The body is a one-line abbreviation of the unique J-cost on that ratio.
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 scales by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$. Upstream modules record that this is the unique cost forced by the Recognition Composition Law (forcing chain T5): any genuine distinction (ratio not one) has strictly positive cost, and $J$ is nonnegative on positives.
This module is Standard Model structural block 10. Its standing convention is that the coherence energy $E_{\mathrm{coh}}$ is fixed once by the electron mass, after which mass and threshold predictions are parameter-free. Domain cost is the local name for applying $J$ to a mass-over-energy ratio in that calibrated setting.
proof idea
Definitional abbreviation only: evaluate the shared J-cost functional on the ratio $m/e$. No lemmas, tactics, or side conditions appear in the body.
why it matters
Gives the Standard Model layer a named handle on mass-versus-scale mismatch under electron calibration of $E_{\mathrm{coh}}$. Sibling facts in the same module (equality at equal arguments, nonnegativity, canonical threshold positivity, and the structural certificate) build directly on this abbreviation. Framework-wise it is the T5 J-cost specialized to SM mass ratios; it does not itself force $\varphi$, the eight-tick period, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.