domainCost
plain-language theorem explainer
Domain cost is the recognition cost of a mass-to-energy (or observable-to-reference) ratio: J(m/e) with the unique RS cost J(x)=(x+x^{-1})/2-1. Anyone building relational QM frames from J-cost cites it as the observer-local cost of a ratio. 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{x+x^{-1}}{2}-1$ is the Recognition Science cost of a positive ratio.
background
The module develops relational quantum mechanics in the Rovelli sense from Recognition Science: each observer's recognition system supplies a J-cost frame. Observers need not share absolute scales; they agree on costs of ratios of observables to local references.
The upstream cost is the standard RS functional $J(x)=\frac{1}{2}(x+x^{-1})-1$, forced by the Recognition Composition Law (T5 uniqueness). It vanishes only at ratio one and is nonnegative for positive arguments. Domain cost simply specializes that functional to the ratio of two reals $m$ and $e$ (mass and energy, or more generally observable and reference in the observer's frame).
proof idea
Pure definition: one-line abbreviation that applies the imported J-cost functional to the quotient $m/e$. No lemmas, tactics, or proof obligations.
why it matters
This is the local cost primitive for the relational-QM-from-J-cost development (module status: structural theorem, zero sorry). It encodes the RS claim that different observers agree on $J(\mathrm{observable}/\mathrm{reference})$ rather than on absolute values. Sibling lemmas (nonnegativity, evaluation identities, canonical threshold, and the RelationalQM3 certificate) build on this abbreviation. Framework landmark: T5 J-uniqueness and the RCL, which force the same $J$ used here. No downstream edges are recorded yet; the definition is the entry point for the module's certificate stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.