domainCost_at_eq
plain-language theorem explainer
For any nonzero real scale r, the domain cost of comparing r to itself is exactly zero. Cosmology proofs that normalize spectral-index or scale comparisons against a reference cite this diagonal vanishing. The proof is a one-line unfold: the ratio collapses to 1 and the J-cost unit lemma applies.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: $\mathrm{domainCost}(r,r)=0$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. The unit identity $J(1)=0$ is the lemma Jcost_unit0. In this module the domain cost of two positive scales is that J-cost applied to their ratio, so equal arguments force the ratio to 1.
The local setting is Cosmology RS Module 4, a structural (zero-sorry) package around the scalar spectral index $n_s=1-2/45\approx 0.9556$ versus the Planck value $0.9649$ (about $2.2\sigma$ tension). Domain cost supplies the cost functional used when comparing cosmological scales inside that package.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $J(r/r)=0$. Rewrite $r/r=1$ by the nonzero hypothesis via div_self, then finish with the upstream unit lemma $J(1)=0$.
why it matters
Diagonal vanishing is the sanity check that a cost functional is a true defect: identical scales incur zero cost. Inside Module 4 it underwrites any later comparison of cosmological domains or thresholds (siblings include nonnegativity of domain cost, the canonical threshold, and the module certificate RSCosmo004Cert). It sits on the T5 J-uniqueness landmark: once $J$ is forced, $J(1)=0$ is immediate and propagates to every ratio-based cost. No downstream consumers are wired yet; the lemma is local structural support for the still-open $n_s$ tension discussion rather than a closed physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.