domainCost_at_eq
plain-language theorem explainer
On the diagonal, domain cost vanishes: for any nonzero real scale r the cost of the pair (r,r) is zero. Cost-functional and forcing-chain arguments cite this as the unit normalization of the ratio cost. The proof is a one-line unfold that rewrites the ratio to 1 and applies J(1)=0.
Claim. For every real $r\neq 0$, the domain cost of equal arguments is zero: evaluating the cost on the pair $(r,r)$ yields $0$.
background
Recognition Science measures scale mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, also written $J(x)=(x-1)^2/(2x)$. By construction $J(1)=0$, and this is the unique zero of $J$ on the positive reals. Domain cost is the J-cost of a ratio of two real scales, so the diagonal case is exactly the unit evaluation of $J$.
This file is Foundation RS Module 5 in the forcing chain T0–T8: structural theorems proved in Lean 4 with zero sorry and zero axioms. The sole upstream fact used here is the lemma that $J(1)=0$, obtained by simplifying the closed form of $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost (J of the ratio of the two arguments). Rewrite $r/r$ to $1$ with the nonzero hypothesis via division-by-self. Finish by the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the unit-normalization fact for domain cost inside the RS forcing chain (T0–T8). It sits next to nonnegativity of domain cost and the canonical-threshold lemmas in the same module, and it underwrites later cost comparisons that treat equal scales as zero defect. Framework landmark: T5 forces $J$ as the unique cost obeying the Recognition Composition Law and vanishing at unity; this lemma is the concrete unit case of that vanishing. No downstream dependents are recorded in the current graph slice; the result is local scaffolding for cost identities rather than a top-level forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.