domainCost_at_eq
plain-language theorem explainer
For any nonzero real r, the domain cost of comparing r to itself is exactly zero. Cost-functional arguments in RS physics (mass ratios, lifetime ladders) cite this as the diagonal normalization of the J-cost. The proof is a one-line unfold: reduce the ratio to 1 and apply the unit root of J.
Claim. For every real $r \neq 0$, the domain cost vanishes on the diagonal: the cost of the pair $(r,r)$ equals $0$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x-1)^2/(2x)$ (equivalently $\cosh(\log x)-1$), which is nonnegative and zero only at the unit $x=1$. The lemma Jcost_unit0 records exactly that root: $J(1)=0$.
In this module the domain cost of a pair of nonzero reals is the J-cost of their ratio. Setting both arguments equal therefore asks whether self-comparison is free, which is the content of the present statement.
The ambient file is Physics RS Module 3 (neutron lifetime: $\phi^{17}\cdot 0.246,\mathrm{s}=878.5,\mathrm{s}$ vs PDG $878.4,\mathrm{s}$). The module is marked structural: zero sorry, zero axiom. Diagonal vanishing is the baseline identity before nonnegativity and threshold lemmas in the same file.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $J(r/r)=0$. Rewrite $r/r=1$ by the standard division identity (using $r\neq 0$), then finish by the upstream unit root $J(1)=0$.
why it matters
Diagonal vanishing is the normalization step for any RS cost comparison: without it, ratio ladders and threshold arguments have no zero point. In this module it sits beside nonnegativity of domain cost and the canonical threshold, feeding the structural certificate for the neutron-lifetime claim ($\phi^{17}$ times the 0.246 s yardstick). No downstream theorems currently depend on it by name, so its role is local scaffolding inside the physics certificate rather than a link in the T0–T8 forcing chain. It is the concrete instance of the general fact that $J$ is a true cost (zero iff matched).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.