domainCost_at_eq
plain-language theorem explainer
For any nonzero real r, the domain cost of the pair (r,r) is zero. This is the diagonal normalization of the RS ratio cost, cited wherever self-comparison must vanish before thresholds or nonnegativity arguments. The proof is a one-line wrapper: unfold the definition, reduce the self-ratio to 1, and apply the unit identity J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of comparing $r$ to itself vanishes: if the domain cost is the $J$-cost of the ratio, then $J(r/r) = 0$.
background
Recognition Science fixes a unique nonnegative cost on positive ratios, written $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ (equivalently $(x-1)^2/(2x)$). The module records structural consequences of that choice: $J$ itself, the golden-ratio fixed point, and the forced spatial dimension $D=3$.
Domain cost is the cost of a pair of nonzero reals via their ratio: it evaluates $J$ at $a/b$. The elementary unit identity $J(1)=0$ is already proved upstream as Jcost_unit0 by direct simplification of the closed form. The present statement is the diagonal case of that identity under the domain-cost packaging.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite $r/r=1$ with the nonzero hypothesis, then finish by the upstream lemma $J(1)=0$.
why it matters
This is a structural normalization lemma in the first RS mathematics structural module (status: proved, zero sorry). It anchors the claim that self-ratios carry zero cost before any threshold or positivity work on the same cost (sibling facts include nonnegativity of domain cost and a canonical positive threshold). In the forcing chain it sits under T5 $J$-uniqueness: once $J$ is fixed by the composition law, the identity $J(1)=0$ is forced and must hold on every self-ratio. No downstream consumers are wired yet; the lemma is infrastructure for later ratio-cost arguments rather than a paper-level theorem on its own.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.