domainCost
plain-language theorem explainer
Domain cost assigns to a mass-energy pair the recognition cost of their ratio. Cosmology workers in the RS spectral-index module use it as the local cost on domain parameters. The body is a one-line definition that feeds the ratio into the standard J-cost.
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 mismatch of positive ratios by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$, also written $\cosh(\log x)-1$. Upstream modules (Cost, RefineTrigger, CoherenceCollapse) fix this same functional: it vanishes only at ratio one and is nonnegative for $x>0$. That uniqueness is the T5 landmark of the forcing chain.
This file is Cosmology RS Module 4, aimed at the scalar spectral index $n_s=1-2/45\approx 0.9556$ against Planck $0.9649$ (about $2.2\sigma$). The module is marked structural (zero sorry, zero axiom) and still OPEN on the tension. Domain cost is the cost primitive on which later threshold and certificate lemmas in the same file sit.
proof idea
Pure definition: apply the imported J-cost to the quotient $m/e$. No lemmas, no tactics, no hypotheses.
why it matters
Gives the module a named cost on mass-energy ratios so sibling facts (equality at equal arguments, nonnegativity, canonical threshold positivity, and the RSCosmo004 certificate) can quote a single symbol rather than raw $J(m/e)$. In the broader framework it is the local instance of the T5 J-functional inside the cosmology lane that targets $n_s$. It does not itself close the Planck tension; it only supplies the cost language the structural certificate uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.