domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the RS recognition cost J(m/e). Information theorists working the mutual-information-from-J-cost bridge cite it as the coupling weight between a domain scale and an energy scale. The body is a one-line abbreviation of Jcost on the quotient.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ is the Recognition Science cost of a positive ratio.
background
The module develops mutual information from the RS J-cost: at recognition coupling one has $I(X;Y) = J(\varphi),H(X)$, so mutual information is a fixed fraction of marginal entropy. The cost functional itself is the unique solution forced by the Recognition Composition Law, $J(x) = \frac12(x + x^{-1}) - 1$ (also written $\cosh(\log x) - 1$), non-negative for $x > 0$ and zero only at $x = 1$.
Upstream, every copy of Jcost in Cost, Cosmology, Gravity, and Spiral is the same formula: the RS recognition cost of a positive ratio. Domain cost simply specializes that functional to a mass-over-energy argument, treating $m/e$ as the scale ratio whose mismatch is charged.
proof idea
Pure definitional abbreviation: apply the upstream J-cost functional to the quotient $m/e$. No lemmas, no tactics.
why it matters
Gives the module a named coupling weight for how far a domain scale sits from an energy scale under J. Sibling lemmas (domainCost_at_eq, domainCost_nonneg) and the mutual-info certificate (MutualInfo2Cert, cert) sit on top of this abbreviation. In the forcing chain it inherits T5 J-uniqueness and the RCL identity; the module status line frames the whole development as a structural theorem with zero sorry and zero axiom, tying mutual information at recognition to the $J(\varphi)$ fraction of entropy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.