domainCost_at_eq
plain-language theorem explainer
On the diagonal, the real domain cost vanishes: for any nonzero r, the cost of the pair (r,r) is zero. Neutron-proton difference arguments in this module use that zero as the reference point of the cost functional. The proof is a one-line unfold-and-rewrite that reduces the ratio to 1 and cites J(1)=0.
Claim. For every real $r\neq 0$, the domain cost of the equal pair equals zero: if the two arguments coincide, $\mathrm{cost}(r,r)=0$.
background
This module sits in the RS foundation layer that treats the neutron-proton mass split as a pure cost evaluation: the structural claim is $m_n-m_p=1.293,\mathrm{MeV}$ recovered from $J(\varphi)$ times a fixed MeV yardstick (with a W-mass correction form stated as exact in the module header).
The cost primitive is the standard RS J-cost on positive reals (equivalently $J(x)=(x-1)^2/(2x)$ in the Cost module). The lemma Jcost_unit0 records the normalization $J(1)=0$. The local domainCost is the bivariate wrapper that feeds a ratio of its two real arguments into that J-cost; the present theorem is the diagonal specialization of that wrapper.
No extra positivity or continuity hypotheses appear: only $r\neq 0$ so the ratio is defined.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes a J-cost of the ratio $r/r$. Rewrite that ratio to $1$ by div_self using $r\neq 0$. Finish by the upstream lemma $J(1)=0$.
why it matters
Pins the zero of the domain cost on equal arguments, which is the algebraic baseline any neutron-proton (or more general mass-difference) cost comparison in this file must sit on. The module presents itself as a structural, sorry-free RS5 certificate that $J(\varphi)$ times the stated MeV scale reproduces the empirical $1.293,\mathrm{MeV}$ split; a clean diagonal zero is the first sanity check before off-diagonal evaluations and threshold comparisons among the sibling lemmas (domainCost_nonneg, canonicalThreshold, the NeutProtonDiff5Cert bundle).
In the broader forcing chain this is local bookkeeping rather than a T5-T8 step: it inherits J-uniqueness and the $\varphi$ fixed point from upstream Cost/Constants, and only specializes them to the equal-argument case needed by the mass-difference certificate. No downstream dependents are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.