domainCost_at_eq
plain-language theorem explainer
On any nonzero real scale r, the domain cost of the pair (r,r) is exactly zero. Rung-spacing and J-cost arguments in the RS foundation cite this as the diagonal vanishing law. The proof is a one-line unfold-and-rewrite: the self-ratio collapses to 1, then the unit-zero lemma for J finishes it.
Claim. For every real number $r \neq 0$, the domain cost of the pair $(r,r)$ equals zero.
background
Foundation Module 11 treats RS rung spacing: consecutive rungs on the $\varphi$-ladder differ by the fixed factor $\varphi = (1+\sqrt{5})/2$. The local cost on a pair of scales is the Recognition J-cost of their ratio.
The J-cost is the unique nonnegative functional fixed by the Recognition Composition Law, with closed form $J(x)=(x-1)^2/(2x)$ (equivalently $\cosh(\log x)-1$). In particular $J(1)=0$, recorded upstream as Jcost_unit0. The domain cost is that J applied after forming the ratio of the two arguments, so identical nonzero scales must cost nothing.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(r/r)$. Rewrite $r/r=1$ by div_self using the hypothesis $r\neq 0$. Discharge the goal by the upstream lemma $J(1)=0$.
why it matters
Structural theorem in Module 11 (0 sorry, 0 axiom): the cost is a genuine defect measure, vanishing on the diagonal. It sits beside the sibling nonnegativity and canonical-threshold statements that police rung comparisons. In the forcing chain this is the local face of T5 J-uniqueness: $J$ is zero precisely at the self-similar unit. The dependency graph currently lists no downstream consumers, so the lemma is infrastructure for later spacing and threshold certificates rather than a parent of a named global theorem yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.