domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain (ratio) cost vanish: the J-cost of r/r is zero. Cited by anyone building ratio-symmetric recognition cost or the J(x)=J(1/x) structural layer. Proof is a one-line unfold of the domain cost, reduction of the ratio to 1, and the unit identity J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero. Equivalently, if domain cost is the recognition $J$-cost of the ratio of its arguments, then $J(r/r)=0$.
background
Module 9 of the RS forcing chain records the structural fact that recognition cost is ratio-symmetric: $J(x)=J(1/x)$. The cost functional is the standard RS $J$-cost (also written $\cosh(\log x)-1$), forced uniquely at T5 of the unified forcing chain.
Domain cost is the in-module wrapper that evaluates $J$ on a ratio of two reals. The only upstream lemma used here is Jcost_unit0: $J(1)=0$, which follows by direct simplification of the squared-ratio form $J(x)=(x-1)^2/(2x)$ at the unit point.
The local setting is purely algebraic: no measure theory, no dynamics, only the cost identity on $\mathbb{R}\setminus{0}$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite the ratio by div_self using $r\neq 0$, obtaining $J(1)=0$. Discharge with the upstream unit lemma Jcost_unit0.
why it matters
Closes the diagonal case of domain cost inside the J-symmetry module (Foundation RS Module 9, structural, zero sorry). That module underwrites the Recognition Composition Law and the T5 uniqueness of $J(x)=(x+x^{-1})/2-1$. Vanishing on the diagonal is the baseline that makes nonnegativity and the $J(x)=J(1/x)$ symmetry meaningful: cost measures deviation from ratio one, not absolute scale.
No downstream consumers are wired in this slice (used_by empty), so the lemma is presently a local structural brick rather than a cited parent. It pairs with sibling nonnegativity and the canonical threshold facts in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.