domainCost
plain-language theorem explainer
Domain cost assigns to a mass m and energy scale e the recognition cost of their ratio m/e. Gravity and ladder analyses cite it when comparing a mass to a local energy unit on the phi-rung lattice. The body is a one-line abbreviation of the unique J-cost functional.
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 of positive ratios by the J-cost $J(x)=\frac{1}{2}(x+x^{-1})-1$. Upstream docs state this is the unique cost forced by the Recognition Composition Law, and that a genuine distinction (ratio not one) has strictly positive cost. Equivalently $J(x)=\cosh(\log x)-1$.
This module is Gravity RS Structural Module 8. Its setting is RS rung spacing: adjacent rungs differ by the golden ratio $\phi\approx 1.618$. Domain cost packages J applied to a mass-to-energy ratio so later lemmas can talk about when that cost sits above or below a canonical threshold on the ladder.
proof idea
Pure definition: one-line abbreviation that feeds the ratio $m/e$ into the already-defined J-cost. No proof obligations.
why it matters
Gives the gravity stack a named cost for comparing a mass to an energy scale, aligned with T5 J-uniqueness and the RCL-forced functional. Siblings in the same module (nonnegativity, evaluation identities, canonical threshold positivity, and the RSGRVStructural008 certificate) build on this abbreviation to certify structural claims about rung spacing. No external used-by edges are recorded yet; the declaration is local scaffolding for the module-8 certificate rather than a global forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.