domainCost
plain-language theorem explainer
Domain cost assigns to a mass m and energy scale e the recognition cost of their ratio. Anyone working the RS structural calibration (electron mass fixing E_coh once) cites it as the local cost functional on mass–energy pairs. 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$.
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 define the same functional: any genuine distinction (ratio not one) has strictly positive cost, and $J$ is nonnegative on positive reals.
This module is Mathematics RS Structural 10. Its setting is RS calibration: the coherence energy $E_{\mathrm{coh}}$ is fixed once by the electron mass, after which predictions are parameter-free. Domain cost is the local specialization of $J$ to a mass–energy pair $(m,e)$, i.e. the cost of the dimensionless ratio $m/e$.
proof idea
Pure definitional abbreviation. The body is the term $J(m/e)$ with no proof obligations; it inherits nonnegativity and uniqueness properties from the ambient $J$-cost once positivity of the ratio is assumed downstream.
why it matters
Places the T5 J-uniqueness cost on the mass–energy ratios that structural calibration uses when $E_{\mathrm{coh}}$ is set by the electron mass. Sibling facts in the same module (evaluation at equality, nonnegativity, canonical threshold positivity, and the structural certificate) build on this abbreviation. No downstream edges are recorded yet; the declaration is infrastructure for the parameter-free structural theorem package rather than a leaf claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.