domainCost
plain-language theorem explainer
Domain cost of a mass–energy pair is the recognition cost of their ratio m/e. Structural and threshold arguments in the RS mathematics modules cite it whenever a mass-to-energy ratio must be scored by the unique J-functional. The declaration is a one-line abbreviation: apply Jcost 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 forces a unique cost on positive ratios. The functional $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$) is the unique solution of the Recognition Composition Law; that uniqueness is T5 in the forcing chain. Upstream modules package the same formula as Jcost, with the standing convention that a genuine distinction (ratio not one) has strictly positive cost and that $J$ is nonnegative on $(0,\infty)$.
This module is Mathematics RS Structural Module 9. Its local setting is the structural segment of the forcing chain T5 (J-uniqueness) through T8 ($D=3$), with status STRUCTURAL THEOREM (0 sorry, 0 axiom). Domain cost simply specializes $J$ to the mass-to-energy ratio that later siblings bound and threshold.
proof idea
No proof body: the declaration is a pure definition. It unfolds as the composition of the already-defined recognition cost $J$ with the ratio map $(m,e)\mapsto m/e$. Downstream lemmas (nonnegativity, evaluation identities) reason by unfolding this abbreviation and invoking the corresponding properties of $J$.
why it matters
The definition is the local scoring primitive for Structural Module 9. Sibling results such as nonnegativity of domain cost and the canonical threshold are stated directly in terms of it; the certificate objects in the same file package those facts. In the broader framework it ties mass–energy comparisons to the T5 J-uniqueness landmark and the Recognition Composition Law, so any later structural bound on how far $m/e$ may sit from 1 is automatically a bound in the unique RS cost. No external used-by edges are recorded yet; the immediate consumers are the in-module threshold and certificate declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.