domainCost_at_eq
plain-language theorem explainer
On the diagonal, the domain cost vanishes: for any nonzero real r, the cost of comparing r to itself is zero. Gravity structural proofs cite this as the baseline identity that a matched scale incurs no J-penalty. The argument is a one-line wrapper: unfold the cost, cancel the ratio to 1, and apply the unit-zero lemma for J.
Claim. For every real $r \neq 0$, the domain cost of $r$ against itself is zero: $C_{\mathrm{dom}}(r,r) = 0$.
background
This module is Gravity RS Structural Module 10: RS calibration with $E_{\mathrm{coh}}$ fixed once by the electron mass, so structural gravity statements are parameter-free. Status is a structural theorem block (no sorry, no axioms).
The cost functional is the Recognition Science J-cost. Upstream, $J(1) = 0$ is recorded as Jcost_unit0, and the algebraic form $J(x) = (x-1)^2/(2x)$ makes the unit root immediate. The local domainCost is the two-argument cost used on radial (or scale) pairs in this gravity layer; on equal nonzero arguments it reduces to $J$ of a self-ratio.
Sibling facts in the same file include nonnegativity of the domain cost and a positive canonical threshold, so the diagonal zero sits inside a small package of cost calculus for RS-GR structural claims.
proof idea
One-line wrapper. Unfold domainCost so the goal is a J-cost of a ratio of the two arguments. Rewrite with div_self using $r \neq 0$, obtaining $J(1)$. Discharge by the upstream lemma Jcost_unit0 ($J(1) = 0$), proved by simp on the definition of $J$.
why it matters
In Recognition Science the J-cost (T5 uniqueness: $J(x) = (x+x^{-1})/2 - 1$) is the unique nonnegative cost with $J(1) = 0$ compatible with the Recognition Composition Law. Gravity structural work needs that matched scales pay zero cost before thresholds or inequalities are applied.
This lemma is the on-diagonal normalization for domainCost in the RS-GRV structural 010 package. No downstream edges are recorded yet; siblings (domainCost_nonneg, canonicalThreshold_pos, the RSGRVStructural010Cert bundle) are the natural consumers. It closes the trivial but mandatory base case so later structural gravity identities can treat cost as a true defect from equality of scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.