domainCost
plain-language theorem explainer
Domain cost of a mass-energy pair is the recognition cost J of the ratio m/e. Cosmology arguments that score matter versus radiation scales cite this as the local cost functional. It is a one-line abbreviation of the standard J-cost on that quotient.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Recognition Science measures dimensionless ratios by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$, the unique cost forced by the Recognition Composition Law (T5). Upstream modules define the same functional as the recognition cost of a positive ratio and record that genuine distinctions (ratio not one) have strictly positive cost.
This module treats matter-radiation equality: $\phi^{17}\cdot 0.95$ matches the empirical $z_{eq}\sim 3400$. Domain cost specializes $J$ to a mass-over-energy ratio, the natural dimensionless comparison between matter and radiation scales in that setting.
proof idea
Definitional abbreviation only: evaluate the standard J-cost on the quotient $m/e$. No lemmas, no tactics, no proof obligations.
why it matters
Gives the cost functional used by sibling facts in the same module (equality at the ratio, non-negativity) and by the module certificate that the matter-radiation equality match is a structural theorem (zero sorry, zero axiom). Anchors the cosmology layer to the global J-cost of the forcing chain (T5) and the Recognition Composition Law, so later redshift and ladder comparisons share one cost language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.