domainCost_at_eq
plain-language theorem explainer
The recognition cost of comparing a domain value to itself is zero for every nonzero real. Ratio-based J-cost arguments cite this as the diagonal normalization. Proof is a one-line unfold: the self-ratio collapses to 1, then J(1)=0 applies.
Claim. For every real $r \neq 0$, the domain recognition cost of the pair $(r,r)$ vanishes: the cost of the self-ratio is $0$.
background
This module records structural facts about Recognition Science J-cost symmetry: $J(x)=J(1/x)$, so recognition cost depends only on the ratio of its arguments. Status is a pure structural theorem (no sorry, no axioms).
The underlying cost is the unique J forced by the Recognition Composition Law. Upstream, $J(1)=0$ is recorded as a one-line simplification of the explicit form $J(x)=(x-1)^2/(2x)$ (equivalently $(x+x^{-1})/2-1$). Domain cost is the specialization of that J to a ratio of two real domain values; the equal-argument case is exactly the unit input of J.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose J of the ratio; rewrite $r/r=1$ by the nonzero hypothesis; finish with the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the normalization any ratio-symmetric recognition cost must satisfy: identical domain values incur zero cost. It sits in Foundation structural module 7 beside nonnegativity and the canonical threshold, and is packaged into the module certificate. In the forcing chain this is the unit case of T5 J-uniqueness (J vanishes at the identity ratio). No external dependents are wired yet; the lemma is local infrastructure for the rest of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.