domainCost_at_eq
plain-language theorem explainer
The domain cost of a nonzero real against itself is zero. Anyone normalizing recognition cost on a shared scale factor cites this diagonal identity. The proof is a one-line unfold that cancels the ratio to the unit and applies J(1)=0.
Claim. For every real number $r \neq 0$, the domain cost of the pair $(r,r)$ equals zero.
background
Recognition Science measures scale mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, also written $(x-1)^2/(2x)$. This cost is nonnegative and vanishes only at the fixed point $x=1$. Domain cost compares two real scale factors by feeding their ratio into $J$; equal arguments therefore force the unit ratio whenever the common value is nonzero.
The surrounding Foundation module collects structural RS identities (session 3; zero sorry, zero axiom). Its headline numerical check is $\alpha_s(M_Z)=J(\phi)\approx 0.11803$ against the PDG value 0.1179. Upstream, the unit lemma states $J(1)=0$ by direct simplification of the closed form of $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $J(r/r)=0$. Rewrite the ratio by cancellation of $r$ (using $r\neq 0$) to obtain $J(1)=0$, then finish with the unit lemma for $J$.
why it matters
Diagonal vanishing is the baseline normalization for domain cost: any nontrivial scale mismatch is strictly costly once nonnegativity is in hand. It sits among the Foundation structural facts that underwrite the RS cost calculus (T5 J-uniqueness in the forcing chain; RCL as the composition law for $J$). No recorded downstream dependents yet; sibling facts in the same file (nonnegativity of domain cost, the canonical threshold and its positivity) are the natural consumers. The module-level $\alpha_s$ match is independent numerical context, not a logical parent of this identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.