domainCost_at_eq
plain-language theorem explainer
On the diagonal, the domain cost of any nonzero real scale against itself is zero. Gravity and recognition-cost arguments cite this as the structural vanishing of mismatch when the two arguments coincide. The proof is a one-line wrapper: unfold the cost, cancel the ratio to 1, and apply J(1)=0.
Claim. For every real number $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: the cost of $r$ against itself equals $0$.
background
Recognition Science measures scale mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, also written $(x-1)^2/(2x)$, which is uniquely zero at the unit $x=1$ (T5 uniqueness). In this gravity module the domain cost of a pair of scales is the J-cost of their ratio, so equal nonzero arguments yield the unit input.
The module is a structural gravity layer under the RS eight-tick octave: one full traversal of the binary recognition lattice has period $2^D=8$. Status is fully proved (no sorry, no axioms). The sole upstream fact used here is the elementary identity $J(1)=0$.
proof idea
One-line wrapper. Unfold the domain-cost definition so the goal becomes $J(r/r)=0$. Rewrite $r/r$ to $1$ by the field identity div_self (using $r\neq 0$). Finish by the upstream lemma $J(1)=0$.
why it matters
Supplies the diagonal zero for the domain-cost primitive used throughout the RS gravity structural certificate stack in this module (siblings include nonnegativity of domain cost, the canonical threshold, and the inhabited structural cert). It is the elementary consistency check that equal scales carry zero recognition cost, which any later comparison of domain cost against a positive threshold relies on.
Framework landmarks: T5 J-uniqueness (only the unit has zero cost) and the module's eight-tick structural setting ($2^D=8$). No recorded downstream edges yet; the lemma is local scaffolding for the structural cert rather than a paper-level forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.