domainCost
plain-language theorem explainer
Domain cost of a mass–energy pair is the recognition cost of their ratio m/e. Structural work on the RS count law (seven independent channels from D=3) uses it as the local scale-comparison functional. The declaration is a one-line definitional wrapper around J.
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
The recognition cost is $J(x)=\frac{1}{2}(x+x^{-1})-1$. Upstream modules record it as the unique cost forced by the Recognition Composition Law: it vanishes only at ratio one, and a genuine distinction (ratio not one) has strictly positive cost.
This file is Mathematics RS Structural Module 3. Its stated content is the RS Count Law $2^D-1=7$ independent channels, exact from the D=3 configuration dimension, status structural (zero sorry, zero axiom).
Domain cost simply specializes $J$ to the mass-to-energy ratio, giving a named scale comparison inside that structural setting.
proof idea
Definitional abbreviation only: the value on $(m,e)$ is declared equal to $J(m/e)$. No lemmas, tactics, or proof obligations.
why it matters
Supplies the cost primitive used by the rest of RS_MTH_Structural_003 (nonnegativity of domain cost, the canonical threshold, and the module certificate). It ties the seven-channel count law to the T5 J-uniqueness landmark and to the T8 forcing of three spatial dimensions that yields $2^3-1=7$. No external used-by edges are recorded yet; the declaration is local scaffolding for the structural certificate rather than a leaf of a larger proved chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.