domainCost_at_eq
plain-language theorem explainer
For any nonzero real r, the domain cost of comparing r to itself is zero. Ratio-based RS cost arguments cite this as the diagonal normalization: equal arguments carry no defect. The proof unfolds the cost to J of the ratio, collapses r/r to 1, and applies J(1)=0.
Claim. For every real $r \neq 0$, the recognition domain cost of equal arguments vanishes: if $C(x,y)$ denotes the $J$-cost of the ratio $x/y$, then $C(r,r)=0$.
background
Recognition Science measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$ for $x>0$. The unit identity $J(1)=0$ is the normalization that a perfect match carries zero cost; that fact is the upstream lemma applied here.
This module is the second RS mathematics structural package. Its local theme is the golden-ratio recognition cost $J(\varphi)=\varphi-3/2\approx 0.118$, together with elementary structural properties of a domain-level cost built from $J$.
The domain cost of a pair of nonzero reals is the $J$-cost of their ratio. On the diagonal the ratio is identically 1, so the cost sits at the global minimum of $J$.
proof idea
One-line wrapper. Unfold the domain-cost definition (J of the ratio of the two arguments). Rewrite $r/r$ to $1$ with the nonzero hypothesis via div_self. Finish by the unit lemma $J(1)=0$.
why it matters
Diagonal vanishing is the elementary sanity check that self-comparison is free under the RS cost. It anchors sibling structural facts in the same module (nonnegativity of the domain cost, the canonical threshold, and the module certificate). In the forcing chain, T5 J-uniqueness and the Recognition Composition Law fix $J$ with unique minimum at 1; this lemma is the domain-level echo of that minimum. No external dependents are recorded yet; the result is packaged for the structural certificate rather than as a deep forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.