domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain values carry zero recognition cost: the cost of the pair (r,r) vanishes for every r ≠ 0. Cited wherever the domain-cost functional is used as a baseline for thresholds or nonnegativity. 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 matched pair $(r,r)$ is zero. Equivalently, if domain cost is the Recognition cost $J$ of the ratio of its two arguments, then that cost at equal nonzero inputs is $J(1)=0$.
background
The Recognition cost $J$ is the unique symmetric cost fixed by the Recognition Composition Law. Closed forms used here are $J(x)=(x+x^{-1})/2-1$ and the squared-ratio form $J(x)=(x-1)^2/(2x)$ (for $x>0$). A primitive fact is the unit root $J(1)=0$.
This module is Foundation structural module 3: it packages consequences of the RS count law $2^D-1=7$ independent channels, exact once spatial dimension is fixed at $D=3$. Domain cost is the local pairing that feeds $J$ the ratio of two real domain values; the diagonal identity below is the zero-cost sanity check for that pairing.
Upstream, the only dependency is the lemma that $J(1)=0$, proved by direct simplification of the closed form.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes $J(r/r)=0$), rewrite the ratio to $1$ by div_self using the hypothesis $r\neq 0$, and finish with the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the baseline that equal configurations incur zero recognition cost, so later nonnegativity and threshold statements in the same module sit on a consistent zero. The module is marked a structural theorem (0 sorry, 0 axiom) for the RS count law $2^D-1=7$ coming from the $D=3$ configuration dimension (forcing-chain landmark T8, after T5 J-uniqueness). No recorded downstream dependents yet; the lemma is local infrastructure beside domain-cost nonnegativity and the structural certificate in this file. It does not itself prove the count law; it only anchors the cost side of that structural package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.