domainCost
plain-language theorem explainer
Domain cost assigns to a pair of real quantities the recognition cost of their ratio. Anyone working the RS forcing-chain cost calculus or ratio-symmetric J identities cites this wrapper. It is a one-line definition that feeds the ratio into the standard J-cost functional.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Module 9 of the RS forcing chain treats J-cost symmetry: recognition cost is ratio-symmetric, $J(x)=J(1/x)$. Status is structural (no sorry, no axioms).
The underlying cost is the standard RS functional $J(x)=\frac{1}{2}(x+x^{-1})-1$, also written $\cosh(\log x)-1$. Upstream definitions state it as the recognition cost of a positive ratio, with the companion facts that a genuine distinction (ratio not one) has strictly positive cost and that $J$ is nonnegative on positive reals. Domain cost simply specializes that functional to a mass-or-measure over energy-or-scale ratio $m/e$.
proof idea
Pure definitional wrapper: evaluate $J$ at the quotient $m/e$. No lemmas, no tactics, no proof obligations.
why it matters
Gives the local name for ratio cost inside Foundation RS Module 9, so later lemmas (equality at equal ratios, nonnegativity, canonical thresholds, and the module certificate) can speak about domain pairs without repeating the $J(m/e)$ formula. It sits under the T5 J-uniqueness landmark and the Recognition Composition Law setting, where cost depends only on dimensionless ratios. No downstream edges are recorded yet; the immediate consumers are the sibling facts in this module that close the structural theorem package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.