domainCost
plain-language theorem explainer
Domain cost assigns to a mass m and energy scale e the recognition cost of their ratio m/e. Cosmology proofs that compare baryon or matter scales to a reference energy cite it as the local cost functional. The body is a one-line abbreviation of Jcost at m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$ is the recognition cost of a positive ratio.
background
Recognition Science measures mismatch of positive ratios by the J-cost $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream modules (Cost, RefineTrigger, CoherenceCollapse) all expose this same functional: cost vanishes only at ratio one and is nonnegative for $x>0$.
This file is Cosmology RS Module 9, whose structural claim is that $J(\varphi)(1-J(\varphi))/2\approx 0.052$ matches the observed baryon density $\Omega_b\approx 0.0493$. Domain cost is the local wrapper that feeds mass-to-energy ratios into that J-cost before thresholds and certificates are applied.
proof idea
Pure definition: expand as the existing J-cost evaluated at the quotient $m/e$. No lemmas, tactics, or side conditions appear in the body.
why it matters
Module 9 is marked STRUCTURAL (zero sorry, zero axiom) and targets the baryon-density match $J(\varphi)(1-J(\varphi))/2\sim\Omega_b$. Domain cost is the named entry point that turns a mass/energy pair into a J-value so sibling lemmas (nonnegativity, evaluation at equality, canonical threshold, and the RSCosmo009 certificate) can reason about that cost without reopening the Cost module. It sits on the T5 J-uniqueness landmark: once J is forced, every cosmological density comparison is a special case of $J$ on a ratio. No downstream consumers are wired yet in the graph; the immediate consumers are the in-module siblings that build the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.