domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the Recognition J-cost of their ratio. Structural work on ratio-symmetric cost in RS Mathematics module 7 uses this as the local functional. The body is a one-line abbreviation: apply J 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 forces a unique nonnegative cost on positive ratios. The functional is $J(x)=\frac{1}{2}(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge) all expose this same $J$, and EnergyProcessingBridge records that it is the unique cost forced by the Recognition Composition Law.
This module is Mathematics RS Structural 7: it packages the elementary symmetry $J(x)=J(1/x)$ and treats recognition cost as ratio-symmetric. Status is structural theorem material (no sorry, no axioms).
Domain cost is the specialization of $J$ to a mass-over-energy ratio. The two arguments are plain reals; positivity and well-definedness of the inverse are left to downstream lemmas that invoke $J$ only on positive inputs.
proof idea
Pure definitional abbreviation. The body is the term $J(m/e)$ with no proof obligations. No lemmas are applied; the name simply packages the ratio specialization used by the rest of the module (nonnegativity, threshold comparisons, certificate assembly).
why it matters
Gives the module a named cost on mass–energy pairs so later statements can talk about domain cost rather than raw $J(m/e)$. Siblings build on it: equality at a point, nonnegativity, a canonical positive threshold, and the structural certificate RSMTHStructural007Cert.
In the forcing chain this sits under T5 (J-uniqueness): once $J$ is fixed by the composition law, every structural cost is an instance of that same functional. The module theme is the elementary symmetry $J(x)=J(1/x)$, which makes cost depend only on the unordered ratio class. No downstream external theorems are wired yet (used_by is empty); the definition is local scaffolding for the certificate in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.