domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain arguments yield zero domain cost. Anyone verifying that the diagonal of the domain-cost functional vanishes would cite this. The proof is a one-line unfold-and-cancel: the ratio becomes 1 and J(1)=0 finishes it.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero.
background
The Recognition cost $J$ 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$). Its unit root is elementary: $J(1)=0$.
In this milestone module the domain cost is the $J$-cost of a ratio of two real domain parameters. Evaluating on the diagonal therefore reduces to $J$ at the multiplicative identity, once the common nonzero value cancels.
The module is a structural certificate (Plan v7, 109th pass) for domain-coverage milestones: zero sorry, zero axiom, purely algebraic bookkeeping around $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost (which applies $J$ to a ratio of its two arguments). Rewrite $r/r=1$ by div_self using $r\neq 0$. Discharge the resulting goal $J(1)=0$ by the upstream lemma Jcost_unit0.
why it matters
Supplies the diagonal vanishing identity needed for domain-coverage bookkeeping in FinalModule_1398. Without it, equal-domain pairs would not be certified as zero-cost, breaking the structural certificate that the milestone claims (0 sorry, 0 axiom).
No downstream consumers are recorded yet; the lemma is local scaffolding for the module's own certificate objects (MilestoneCert, cert). It sits downstream of the T5 $J$-uniqueness landmark only indirectly, via the shared $J$-cost API. It does not itself force $\phi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.