domainCost
plain-language theorem explainer
Domain cost assigns to a mass-energy pair the recognition cost of their ratio: J(m/e). Lattice and forcing-chain arguments cite it as the local cost on the recognition lattice. It is a one-line definitional wrapper around the standard J-cost functional.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$.
background
Foundation RS Module 1 sets the recognition lattice: every physical prediction is to derive from the single cost $J(x)=\frac12(x+x^{-1})-1$, with zero sorry and zero axiom. That functional is the unique (up to scaling) continuous solution forced by the Recognition Composition Law and the T5 uniqueness step in the forcing chain.
Upstream, Jcost is defined uniformly as $(x+x^{-1})/2-1$: the RS recognition cost of a positive ratio. A genuine distinction (ratio not one) has strictly positive cost, and $J$ is nonnegative on positives. Domain cost simply specializes that cost to the ratio of two reals interpreted as mass and energy (or any two commensurate lattice coordinates).
proof idea
Definitional abbreviation only: expand the body to $J(m/e)$ and stop. No tactics, no lemmas, no hypotheses.
why it matters
Gives the module a named local cost on pairs so later structural facts (nonnegativity, evaluation identities, canonical thresholds, and the module certificate) can quote a single symbol rather than raw $J(m/e)$. It sits under T5 J-uniqueness and the RCL: once $J$ is forced, every lattice cost is an instance of it. Downstream siblings in the same file (domainCost_nonneg, domainCost_at_eq, canonicalThreshold, RSForcingChain001Cert) build the zero-sorry structural certificate for Module 1. No external used-by edges yet; the declaration is infrastructure for that certificate and for any later mass-ladder or coherence argument that needs cost of a ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.