domainCost_at_eq
plain-language theorem explainer
On the diagonal of equal nonzero scales, domain cost vanishes. Anyone calibrating the D=3 configuration-cost apparatus cites this normalization. The proof unfolds the cost, reduces the ratio to 1, and applies the unit-zero identity for J.
Claim. For every real $r\neq 0$, the domain cost of the equal pair $(r,r)$ is zero.
background
The module proves a structural claim: $D=3$ from eight-tick closure. Period $8=2^3$ means the recognition cycle closes after exactly three binary recursions, the unique dimension for a minimal self-similar lattice (T7/T8 in the forcing chain).
Domain cost scores mismatch between two real scales by feeding their ratio into the RS cost $J$. The cost $J$ is the unique functional forced by the Recognition Composition Law, with closed form $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$). In particular $J(1)=0$.
The upstream lemma records exactly that unit zero: $J(1)=0$. Every diagonal vanishing identity for domain cost is a thin wrapper around this fact.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the claim becomes $J(r/r)=0$), rewrite $r/r=1$ by div_self using $r\neq 0$, then apply the upstream unit-zero lemma $J(1)=0$.
why it matters
Calibrates the local cost so pure scale coincidence contributes nothing; only mismatch is charged. Sibling facts (nonnegativity of domain cost, positivity of the canonical threshold) and the module certificate ConfigDimD3_v3Cert sit on top of this normalization. In the broader framework it keeps the configuration-space cost compatible with T5 J-uniqueness and with the T7/T8 story that $D=3$ is forced by eight-tick self-similarity. No external used-by edges are recorded yet; the lemma is infrastructure inside the D3 certificate session.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.