domainCost_at_eq
plain-language theorem explainer
On the diagonal, the domain cost of any nonzero real scale against itself is exactly zero. Normalization and threshold arguments for Recognition cost on matched scales cite this fact. The proof is a one-line unfold that reduces the ratio to 1 and applies J(1)=0.
Claim. For every real number $r\neq 0$, the domain cost of the pair $(r,r)$ vanishes: evaluating the cost of the self-ratio yields $0$.
background
Recognition Science uses a unique symmetric cost $J$ on positive scales, forced by the Recognition Composition Law. In the library this is Jcost, with the elementary normalization $J(1)=0$ (equivalently $J(x)=(x+x^{-1})/2-1$, or the squared-ratio form $(x-1)^2/(2x)$). The domain cost is the cost of a ratio of two nonzero scales: comparing $r$ to $s$ is $J(r/s)$.
This module is the 2026 state-of-the-art certificate for the foundation layer: structural theorems only, zero sorries, forcing chain T0-T8 complete. The present fact is the diagonal normalization of that domain cost.
Upstream, Jcost_unit0 records $J(1)=0$ by direct simplification of the cost definition.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(r/r)$. Rewrite the self-ratio to $1$ via div_self and the hypothesis $r\neq 0$. Finish by the lemma $J(1)=0$.
why it matters
Diagonal vanishing is the baseline sanity check for any ratio cost used in Recognition matching: identical nonzero scales incur zero cost. It sits beside the nonnegativity and canonical-threshold siblings in the same certificate module, and is consistent with T5 J-uniqueness (the cost is minimized exactly at the self-similar point 1).
No external used_by edges are recorded yet; the lemma is local infrastructure for the RS 2026 structural certificate rather than a step in a longer published derivation. It closes the obvious normalization obligation before threshold or positivity arguments are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.