domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain cost vanish. Anyone verifying that Recognition cost is a true defect (zero on the diagonal) cites this. The proof unfolds the definition, reduces the self-ratio to 1, and applies J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$), forced unique by the T5 step of the forcing chain. It vanishes only at the unit $x=1$.
This module (Structural 010) packages calibration facts once $E_{\mathrm{coh}}$ is fixed by the electron mass, so later predictions stay parameter-free. The domain cost is the local comparison functional built from $J$ on a ratio of two reals: evaluating it on a pair $(r,s)$ reduces to $J(r/s)$ (with $s\neq 0$).
The sole upstream fact used here is $J(1)=0$, the unit-normalization of the cost.
proof idea
One-line wrapper. Unfold the domain-cost definition so the goal is $J(r/r)=0$. Rewrite $r/r=1$ by the nonzero self-division rule, then apply the lemma $J(1)=0$.
why it matters
Diagonal vanishing is the first sanity check that domain cost behaves as a defect rather than an arbitrary functional. In the RS stack it underwrites later nonnegativity and threshold statements in the same structural module (siblings on nonnegativity and the canonical threshold), and it aligns with T5 J-uniqueness: cost is zero precisely on perfect self-similarity.
No downstream dependents are recorded yet; the lemma is infrastructure for the module certificate that Structural 010 is fully proved (0 sorry, 0 axiom) under the single electron-mass calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.