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 Recognition cost on ratios, cited whenever one needs the cost to vanish at identical nonzero scales. The argument unfolds the domain cost to J(r/r), cancels the ratio to 1, and applies the unit-zero lemma for J.
Claim. For every real $r \neq 0$, the domain cost satisfies $C_{\mathrm{dom}}(r,r) = 0$.
background
The Recognition cost $J$ is the unique nonnegative functional fixed by the Recognition Composition Law, with closed form $J(x) = (x-1)^2/(2x)$ (equivalently $(x+x^{-1})/2-1$). In particular $J(1)=0$: the cost of the unit ratio vanishes.
This module packages structural facts around $\varphi$-uniqueness (the self-similar fixed point $\varphi=1+1/(1+1/\cdots)$). The domain cost is the cost of a ratio of two nonzero reals: unfolding shows $C_{\mathrm{dom}}(x,y)=J(x/y)$. The present lemma is the diagonal case of that definition.
Upstream, Jcost_unit0 records $J(1)=0$ by direct simplification of the closed form.
proof idea
One-line wrapper. Unfold the domain cost to expose $J(r/r)$. Rewrite the ratio by div_self using $r\neq 0$, obtaining $J(1)$. Finish by the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the basic normalization any ratio cost must satisfy before nonnegativity, thresholds, or uniqueness arguments can run. In the RS forcing chain, $J$ is forced at T5 and $\varphi$ at T6; structural module 6 sits in that $\varphi$-uniqueness lane.
No downstream dependents are recorded yet. Sibling facts in the same file (nonnegativity of the domain cost, a canonical positive threshold, and the module certificate) are the natural consumers: they need the cost to be zero exactly when the two scales agree. The lemma closes a trivial but mandatory edge so those statements do not re-prove $J(1)=0$ inline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.