domainCost_at_eq
plain-language theorem explainer
On the diagonal, the domain cost vanishes: for any nonzero real r, the cost of comparing r to itself is zero. Anyone working the RS forcing chain or J-cost identities will cite this as the normalization that the self-ratio sits at the unit of J. The proof is a one-line unfold-and-rewrite: r/r becomes 1, and J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero: $\mathrm{domainCost}(r,r)=0$. Equivalently, after reducing the self-ratio $r/r$ to $1$, one recovers $J(1)=0$.
background
Module 8 of the RS forcing chain records structural facts around $\varphi$-uniqueness: $\varphi=(1+\sqrt{5})/2$ as the unique fixed point of the recognition recursion (status: structural theorem, zero sorry, zero axiom).
The cost function $J$ is the unique nonnegative functional forced by the Recognition Composition Law; in the Cost module it is written $J(x)=(x-1)^2/(2x)$ (equivalently $\cosh(\log x)-1$). The lemma $J(1)=0$ is the unit normalization of that cost.
Domain cost is the pairwise comparison built from $J$ on a ratio of nonzero reals. Evaluating on the diagonal therefore reduces to the unit case of $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is a statement about $J$ of a ratio; rewrite the self-ratio $r/r$ to $1$ via div_self (using $r\neq 0$); finish by the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the baseline sanity check for any cost used in the forcing chain: self-comparison must carry zero defect before one talks about thresholds, nonnegativity, or $\varphi$-fixed-point uniqueness in this module. It sits next to the sibling nonnegativity fact for domain cost and the canonical-threshold positivity lemmas that feed the Module 8 certificate. In the broader T0–T8 chain it is the local instance of T5's $J$-normalization ($J(1)=0$) inside a ratio-based domain cost, not a new forcing step. No downstream dependents are recorded yet; the lemma is infrastructure for the module certificate rather than a cited parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.