domainCost_at_eq
plain-language theorem explainer
The domain cost of any nonzero real scale against itself is zero. Cosmology arguments that treat the RS cost as a true mismatch measure cite this diagonal vanishing. The proof is a one-line unfold of the ratio cost, rewrite to the unit, and the unit root of J.
Claim. For every real $r\neq 0$, the domain cost of the scale $r$ relative to itself vanishes: the cost of the ratio $r/r$ is zero.
background
Recognition Science measures scale mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. This functional is nonnegative and vanishes only at the unit $x=1$ (the lemma $J(1)=0$).
In this cosmology module the two-argument domain cost is the J-cost of the ratio of the two scales. The module itself is a structural package recording that the RS tensor-to-scalar ratio $r=2/(44\phi^2)\approx 0.0174$ lies under the Planck bound $0.036$, with status "structural theorem" (zero sorry, zero axiom).
Diagonal vanishing is the baseline sanity check: a domain matched to itself must carry zero recognition cost before off-diagonal bounds or thresholds are used.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(r/r)$. Rewrite the ratio to $1$ by division-by-self (using $r\neq 0$). Finish by the unit-root lemma $J(1)=0$.
why it matters
Diagonal vanishing is local infrastructure for any RS cosmology cost: without it, the cost would not be a genuine mismatch functional. The same file packages nonnegativity of domain cost, a canonical positive threshold, and the Module-5 certificate that the RS-predicted tensor ratio sits under the Planck bound. No downstream dependents are wired yet; the lemma supports the structural consistency claim of the module rather than a named parent theorem in the forcing chain. It does not touch T0-T8 directly, but it inherits the J-cost fixed by T5 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.