domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the Recognition J-cost of their ratio. Cosmology structural certificates cite it as the local cost on mass-to-energy ratios. The body is a one-line definition: apply the forced cost J to m/e.
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
This module records the structural fact that Recognition cost is ratio-symmetric: $J(x)=J(1/x)$. The cost itself is the unique functional forced by the Recognition Composition Law (forcing chain T5): $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$ on positives.
Upstream, every copy of Jcost is the same formula: the RS recognition cost of a positive ratio, strictly positive when the ratio is not one, and nonnegative for $x>0$. Domain cost simply specializes that functional to a mass-over-energy argument, the natural dimensionless ratio in the cosmology setting.
proof idea
Pure definition, no proof obligations. The body applies the shared J-cost functional to the single ratio $m/e$. No lemmas, tactics, or hypotheses are involved.
why it matters
Gives the local cost object for RS Cosmology Structural Module 7 (J-cost symmetry / ratio symmetry). Sibling facts built on it include nonnegativity of domain cost, evaluation at equal arguments, and the module certificate RSCOSStructural007Cert. In the broader framework it is the T5 J-cost restricted to mass–energy ratios, so later cosmology claims can quote a named cost rather than reopening the composition law. No downstream theorems are wired yet in the graph; the definition is scaffolding for those siblings and the structural certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.