domainCost_at_eq
plain-language theorem explainer
On the diagonal the domain cost vanishes: for any nonzero real r, comparing r to itself costs zero under the Recognition cost. Anyone normalizing ratio-based mismatch functionals in the RS foundation would cite this. The argument unfolds the domain-cost definition, cancels the self-ratio to 1, and applies the unit identity 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
The Recognition cost $J$ is the unique nonnegative functional fixed by the Recognition Composition Law. Explicitly $J(x)=(x+x^{-1})/2-1=(x-1)^2/(2x)$ for $x>0$, so the unit point is a zero: $J(1)=0$. That unit identity is the sole upstream lemma used here.
Domain cost is the cost of a ratio of two nonzero reals: it applies $J$ to the quotient of its two arguments. The present module (Foundation RS Module 12) records structural dimensionless identities for RS, including the exact evaluation $J(\varphi)=\varphi-3/2$, and is marked as a structural theorem block with zero sorry and zero axiom.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes $J(r/r)=0$), rewrite the self-ratio to $1$ by the nonzero hypothesis, and finish by the upstream unit lemma $J(1)=0$.
why it matters
Pins the normalization that self-comparisons carry no cost, so domain cost measures genuine mismatch rather than absolute scale. Lives in the Foundation forcing-chain modules that lock down $J$ and the golden-ratio fixed point (T5 J-uniqueness, T6 $\varphi$ as self-similar fixed point). Module status is structural theorem (0 sorry, 0 axiom). No recorded downstream dependents yet; sibling results cover nonnegativity of domain cost and the canonical threshold. Supports later dimensionless claims such as the exact value $J(\varphi)=\varphi-3/2$ by keeping the cost calibrated at the unit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.