domainCost
plain-language theorem explainer
The domain cost of a mass–energy pair is the recognition cost of their ratio m/e. Cosmologists citing the RS structural count law (seven independent channels from D=3) use it as the local cost on dimensionless mass-to-energy ratios. It is a one-line definition wrapping the unique J-cost forced by the Recognition Composition Law.
Claim. For real numbers $m$ and $e$, define the domain cost by $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 cost $J(x)=\frac{1}{2}(x+x^{-1})-1$. Upstream modules record that this is the unique functional forced by the Recognition Composition Law, vanishes only at ratio one, and is nonnegative for $x>0$.
This module packages structural cosmology under the RS Count Law: configuration dimension $D=3$ yields $2^D-1=7$ independent channels, with status structural theorem (zero sorry, zero axiom).
Domain cost simply specializes $J$ to the mass-over-energy ratio, the natural dimensionless argument when a mass scale is compared to an energy scale in cosmological bookkeeping.
proof idea
One-line definition: evaluate the recognition cost $J$ at the quotient $m/e$. No lemmas and no proof obligations; the body is pure abbreviation of the upstream $J$-cost.
why it matters
Local cost primitive for the RS cosmology structural package. Sibling lemmas (nonnegativity, evaluation identities, canonical threshold, and the module certificate) sit on top of it. It ties cosmological mass–energy comparisons to the T5 $J$-uniqueness landmark and to the $D=3$ count $2^D-1=7$ stated in the module doc. No external used-by edges yet; the declaration exists to feed the in-module structural certificate rather than a downstream physics theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.