domainCost
plain-language theorem explainer
Domain cost scores a mass-to-energy ratio by the RS recognition cost J(m/e). Cosmologists working the Li-7 Spite plateau band use it as the local mismatch measure between a predicted mass scale and an energy scale. The definition is a one-line specialization of J-cost to the ratio m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=(x+x^{-1})/2-1$ is the recognition cost of a positive ratio.
background
Module RS_Cosmo_Module_012 treats the lithium-7 Spite plateau as a structural RS cosmology claim: the RS band $(4.69,4.86)\times 10^{-10}$ sits inside the observed window $(4.0,5.2)\times 10^{-10}$, status RS_PASS with no sorry and no axioms.
The recognition cost $J$ is the unique cost forced by the Recognition Composition Law and the T5 uniqueness step: $J(x)=\frac{1}{2}(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream docs state it as "the RS recognition cost of a positive ratio" and note that a genuine distinction (ratio not one) has strictly positive cost; $J$ is nonnegative on positive reals.
Domain cost simply feeds the dimensionless ratio of a mass-like parameter $m$ to an energy-like parameter $e$ into that same $J$. Sibling lemmas in the module (nonnegativity, evaluation identities, canonical thresholds) build on this abbreviation.
proof idea
Pure definitional abbreviation: no proof body. It applies the shared $J$-cost functional to the single argument $m/e$. Downstream facts about nonnegativity or equality at matched scales follow from the corresponding properties of $J$, not from extra work here.
why it matters
In the cosmology module this is the local cost functional against which Spite-plateau mass/energy mismatch is measured. It ties the Li-7 structural certificate to the same $J$ that appears in the forcing chain (T5 J-uniqueness) and in gravity/coherence modules, so cosmological band checks reuse the global recognition cost rather than an ad hoc distance.
No downstream edges are recorded yet; siblings such as domainCost_nonneg, canonicalThreshold, and RSCosmo012Cert are the immediate consumers. The declaration does not itself prove the Spite band inclusion; it only names the cost those certificates evaluate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.