domainCost_at_eq
plain-language theorem explainer
On the diagonal, domain cost vanishes: for any nonzero real r the cost of comparing r to itself is zero. Anyone citing the J-cost equilibrium (minimum at ratio 1) uses this. The proof unfolds the cost, cancels r/r to 1, and applies the unit lemma J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of $r$ against itself is zero: $\mathrm{domainCost}(r,r)=0$. Equivalently, the J-cost of the self-ratio is the unit value $J(1)=0$.
background
Module 4 of the RS forcing chain records the structural facts about the Recognition J-cost: its global minimum is at ratio 1, where $J(1)=0$ (equilibrium), and the golden-ratio evaluation $J(\varphi)=\varphi-3/2$. Status is a structural theorem block with no sorry and no axioms.
The cost $J$ is the unique continuous solution forced by the Recognition Composition Law (T5). One algebraic form is $J(x)=(x-1)^2/(2x)$; equivalently $J(x)=(x+x^{-1})/2-1$. Domain cost is the J-cost of a ratio of two nonzero reals, so the self-comparison is exactly $J(r/r)$.
The sole upstream fact is Jcost_unit0: $J(1)=0$, proved by direct simplification of the squared-ratio formula.
proof idea
One-line wrapper. Unfold the definition of domain cost (J-cost of the ratio), rewrite $r/r=1$ via div_self using $r\neq 0$, then apply the unit lemma $J(1)=0$.
why it matters
Pins the equilibrium point of the RS cost: self-comparison carries zero defect. That is the content of the module's first structural claim ("J(1)=0 at ratio=1. Equilibrium") and is the base case for nonnegativity and threshold arguments in the same module (domainCost_nonneg, canonicalThreshold). In the forcing chain it sits under T5 (J-uniqueness): once $J$ is forced, the diagonal identity is immediate and anchors later ladder and mass constructions that measure deviation from ratio 1. No downstream users are recorded yet; the lemma is local scaffolding for the Module 4 certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.