domainCost
plain-language theorem explainer
Domain cost assigns to a mass-energy pair the recognition cost of their ratio. Cosmologists in the RS Hubble-tension module use it as the scalar mismatch between local and CMB scales. It is a one-line specialization of the J-cost functional to m/e, with no extra hypotheses.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$.
background
This module treats the Hubble tension as a structural RS claim: the local-to-CMB ratio $H_{0,\mathrm{local}}/H_{0,\mathrm{CMB}}$ lies in $(1.075,1.091)$, with the SH0ES value $1.0837$ inside the band (status: structural theorem, zero sorry, zero axiom).
The underlying scalar is the recognition cost $J(x)=\frac{x+x^{-1}}{2}-1$, also written $\cosh(\log x)-1$. Upstream docs call it "the RS recognition cost of a positive ratio" and note that a genuine distinction (ratio not one) has strictly positive cost; non-negativity for positive $x$ is standard. Domain cost simply feeds the ratio of two reals into that functional.
In the forcing chain, $J$ is the unique cost fixed at T5 by the Recognition Composition Law. Here it measures how far a mass-to-energy (or scale-to-scale) ratio sits from unity.
proof idea
Definitional one-liner: expand as $J(m/e)$ with the standard $J$-cost. No tactics, no lemmas, no side conditions in the body. Downstream non-negativity and threshold facts will impose positivity of the arguments when needed.
why it matters
Gives the module its basic mismatch scalar for the Hubble-tension certificate (siblings: non-negativity of domain cost, equality-at-one, canonical threshold positivity, and the inhabited RSCosmo003Cert). Without a named cost on ratios, the structural claim that the local/CMB band sits near a fixed RS threshold has nothing to evaluate.
Framework-wise it is the cosmology-facing face of T5 $J$-uniqueness: the same $J$ that forces $\phi$ and the eight-tick structure is reused as the cost of a cosmological scale ratio. The module status (RS_PASS, structural) means this definition is load-bearing for a closed, axiom-free certificate rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.