domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio: J(m/e). Foundation work on RS rung spacing cites it as the local cost of a scale mismatch. The declaration is a one-line definition wrapping the unique J-cost forced by the Recognition Composition Law.
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 cost of a positive ratio.
background
Recognition Science measures mismatch by the J-cost $J(x)=\frac12(x+x^{-1})-1$. Upstream docs state that this is the unique cost functional forced by the Recognition Composition Law, and that a genuine distinction (ratio not one) has strictly positive cost. The same formula appears across Cost, Cosmology, Gravity, and Spiral modules.
This module is Foundation RS Structural Module 8: RS rung spacing, with adjacent rungs separated by the golden ratio $\varphi\approx 1.618$. Status is structural theorem (zero sorry, zero axiom). Domain cost is the local cost of comparing a mass scale $m$ to an energy (or reference) scale $e$ via their ratio.
proof idea
Pure definition: domain cost of $(m,e)$ is defined to be $J(m/e)$. No proof obligations; the body is the single application of the shared J-cost functional to the quotient.
why it matters
Gives the structural module a named cost of scale mismatch before nonnegativity and threshold lemmas (siblings such as domainCost_nonneg and canonicalThreshold). Ties directly to T5 J-uniqueness in the forcing chain: the same $J$ that satisfies the RCL is the cost used for rung-spacing comparisons. No downstream used_by edges are recorded yet; the definition is infrastructure for the module's certificate and threshold statements rather than a leaf theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.