domainCost_at_eq
plain-language theorem explainer
The domain cost of any nonzero real against itself is zero. Anyone treating the Recognition cost as a true defect (vanishing on the diagonal of the ratio) cites this. The argument is a one-line wrapper: unfold the definition, cancel the ratio to 1, and apply the unit-zero lemma for J.
Claim. For every real number $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: if the domain cost is the $J$-cost of the ratio of its two arguments, then that cost equals $0$.
background
This sits in Foundation structural module 5, which packages eight-tick facts: the RS period is $2^D = 8$, one full traversal of the binary recognition lattice, with status structural (no sorry, no axioms).
The underlying cost is the standard Recognition $J$-cost. Upstream, $J(1) = 0$, and $J$ admits the squared-ratio form $J(x) = (x-1)^2/(2x)$. The local domain cost is the $J$-cost of the ratio of its two real arguments, so the diagonal case reduces exactly to evaluating $J$ at $1$ once the ratio is defined.
The nonzero hypothesis is only to make the ratio $r/r$ well-defined in $\mathbb{R}$.
proof idea
One-line wrapper. Unfold the domain-cost definition so the goal is $J(r/r) = 0$. Rewrite $r/r = 1$ by the standard division identity under $r \neq 0$. Finish by the upstream unit lemma $J(1) = 0$.
why it matters
Diagonal vanishing is the first sanity check that domain cost behaves like a defect rather than an arbitrary functional of two reals. In the same structural module it sits beside nonnegativity of domain cost and the canonical threshold facts that set the scale for eight-tick recognition. The module itself is the structural package for the T7 eight-tick octave (period $2^3 = 8$). No downstream dependents are recorded yet; the lemma is infrastructure for later cost comparisons on the recognition lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.