domainCost
plain-language theorem explainer
Domain cost of a pair (m, e) is the recognition cost of their ratio m/e. Cosmology and mass-ladder work cites it when comparing a mass scale to an energy or yardstick scale. The body is a one-line abbreviation of Jcost.
Claim. For real numbers $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 scales by the J-cost $J(x) = (x + x^{-1})/2 - 1$, equivalently $\cosh(\log x) - 1$. It vanishes only at $x = 1$ and is nonnegative for $x > 0$. Upstream modules (Cost, RefineTrigger, CoherenceCollapse) all expose this same functional.
This file is Cosmology RS Module 10. The module targets solar metallicity: the structural claim is that $J(\varphi)^2 \approx 0.01393$ matches $Z_\odot \approx 0.014$. Domain cost packages the ratio of two real parameters (mass-like over energy-like, or any two scales) so later lemmas can talk about nonnegativity and evaluation at equality without repeating the J formula.
proof idea
Pure definition: expand as the recognition cost of the quotient. No tactics, no lemmas beyond the shared Jcost abbreviation from Cost (and its cosmology/gravity aliases).
why it matters
Gives the module a named cost on scale pairs so sibling facts (nonnegativity, value at equal arguments) and the solar-metallicity certificate can cite a single symbol. In the forcing chain, J is the unique cost forced at T5; here it is applied to cosmological abundance ratios rather than abstract positive reals. Downstream use in this file is local (threshold and cert scaffolding around $J(\varphi)^2 \sim Z_\odot$); no external used_by edges are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.