domainCost_at_eq
plain-language theorem explainer
Equal nonzero real scales incur zero domain cost: the J-cost of the ratio r/r vanishes. Anyone normalizing recognition cost on a common yardstick cites this identity. The proof is a one-line unfold-and-rewrite to the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero: $\mathrm{domainCost}(r,r)=0$. Equivalently, if domain cost is the J-cost of the ratio of the two arguments, then $J(r/r)=J(1)=0$.
background
Recognition Science measures mismatch between positive scales by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. The unit root is elementary: $J(1)=0$ (lemma Jcost_unit0).
In this structural module the domain cost of two reals is that J-cost applied to their ratio (undefined only at zero). The local setting is Foundation structural module 9 of the RS forcing chain (T5 J-uniqueness through T8, $D=3$), marked as a fully discharged structural theorem package (0 sorry, 0 axiom).
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite the ratio by div_self using $r\neq 0$, obtaining $J(1)=0$, then apply the upstream unit lemma Jcost_unit0.
why it matters
Zero self-cost is the normalization anchor for any later comparison of scales on the phi-ladder or in the eight-tick octave. It sits inside the T5 J-uniqueness segment of the forcing chain: once $J$ is fixed, equal arguments must score zero, otherwise the cost functional would not be a genuine defect. No downstream consumers are wired yet in the graph; the lemma is infrastructure for nonnegativity and threshold certificates in the same module (domainCost_nonneg, canonicalThreshold).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.