domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain cost vanish: matching a scale against itself carries zero recognition cost. Anyone normalizing J-cost on ratio space cites this diagonal identity. The proof is a one-line unfold reducing the equal case to J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero. Equivalently, feeding the self-ratio $r/r$ into the Recognition cost $J$ yields $J(1)=0$.
background
Recognition Science measures mismatch by the cost $J(x)=\frac{x+x^{-1}}{2}-1$, also written $J(x)=\frac{(x-1)^2}{2x}$ for $x>0$. This functional is nonnegative and vanishes only at the unit ratio $x=1$. The upstream lemma records exactly that baseline: $J(1)=0$.
This module (Foundation RS Structural Module 2) collects structural facts about $J$, including its value at the golden ratio where $J(\varphi)=\varphi-3/2\approx 0.118$. Domain cost is the local wrapper that sends a pair of reals to $J$ of their ratio; the present result is the diagonal normalization of that wrapper.
proof idea
One-line wrapper. Unfold the definition of domain cost (which applies $J$ to the ratio of its two arguments), rewrite $r/r=1$ from the hypothesis $r\neq 0$, and finish by the lemma $J(1)=0$.
why it matters
Fixes the zero baseline on the diagonal: equal domains carry no recognition cost. That is the structural counterpart of T5 J-uniqueness (unique minimum of $J$ at unit ratio) inside the forcing chain. The module frames the surrounding story as golden-ratio recognition cost, $J(\varphi)=\varphi-3/2$. No downstream dependents are recorded yet; the result sits as a local structural certificate beside the nonnegativity and canonical-threshold siblings in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.