domainCost
plain-language theorem explainer
Domain cost assigns the Recognition Science J-cost to a mass-to-energy ratio m/e. Cosmology and structural-forcing arguments cite it whenever a dimensionless mismatch between mass and energy scales must be scored. The definition is a one-line application of the unique cost functional J.
Claim. For real $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 scores dimensionless mismatches with the J-cost $J(x)=\frac{1}{2}(x+x^{-1})-1$. Upstream modules record that this is the unique cost forced by the Recognition Composition Law, and that $J(x)\ge 0$ for $x>0$ with equality only at $x=1$.
This file is Cosmology Structural Module 5. The module framing is the RS eight-tick: period $2^D=8$, one full traversal of the binary recognition lattice, with structural status (no sorry, no axiom).
Here the two arguments are a mass scale $m$ and an energy scale $e$. Their ratio is the natural dimensionless input to $J$, so domain cost is simply that evaluation.
proof idea
Pure definition: domain cost is the abbreviation $J(m/e)$. No lemmas or tactics; the body is the standard J-cost applied to the ratio.
why it matters
Gives the local cost primitive for RS cosmology structural claims in this module (siblings include non-negativity of domain cost, equality at matched scales, and a canonical positive threshold). It ties mass-energy mismatch to the T5 J-uniqueness landmark and to the eight-tick octave setting of the module. No downstream consumers are wired yet in the graph; the def is infrastructure for the structural certificate in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.