domainCost_at_eq
plain-language theorem explainer
On the diagonal, the domain cost vanishes: for any nonzero real r, the cost of comparing r to itself is zero. Anyone normalizing recognition costs or checking positivity of the J-cost on ratios will cite this. The proof is a one-line unfold plus the unit identity J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero: $\mathrm{domainCost}(r,r)=0$. Equivalently, if the domain cost is $J(x/y)$ with $J$ the Recognition cost, then $J(r/r)=J(1)=0$.
background
The Recognition cost $J$ is the unique nonnegative functional fixed by the Recognition Composition Law, normalized so $J(1)=0$ and $J(x)=(x-1)^2/(2x)$ (equivalently $\cosh(\log x)-1$). The unit identity $J(1)=0$ is the lemma Jcost_unit0.
In this module the domain cost of a pair of nonzero reals is the $J$-cost of their ratio. The module itself is Structural Module 3 of the RS mathematics layer: it records the count law $2^D-1=7$ independent channels forced by $D=3$, and packages elementary cost identities used by that count.
The present statement is the diagonal vanishing of that cost: comparing a scale to itself incurs zero recognition cost.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes $J(r/r)=0$), rewrite $r/r=1$ by div_self using $r\neq 0$, then apply the unit lemma $J(1)=0$.
why it matters
Diagonal vanishing is the baseline sanity check for any cost used as a defect or distance on positive reals: identical configurations must score zero. In the RS forcing chain this is the $J$-normalization that sits under T5 (uniqueness of $J$) and under every later mass or coupling formula that measures deviation from a reference rung on the $\phi$-ladder.
The module packages this identity next to nonnegativity and the canonical threshold for the count-law certificate ($2^D-1=7$ channels at $D=3$). No downstream theorems currently depend on it in the graph, so it is infrastructure for the structural certificate rather than a step in a longer derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.