domainCost_at_eq
plain-language theorem explainer
For any nonzero real scale r, the domain cost of the pair (r,r) is exactly zero. Mass-ladder and Z-boson certificate work cites this as the baseline: a perfectly matched scale incurs no J-defect. The proof unfolds the cost to J of the ratio, collapses the ratio to 1, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of comparing $r$ to itself vanishes: the cost of the pair $(r,r)$ equals $0$.
background
Physics RS Module 11 records the structural Z-boson match $M_Z \approx \phi^{13}\cdot 0.175 \approx 91.2,\mathrm{GeV}$ as a zero-sorry theorem. Comparisons of mass (or other) scales are scored by a domain cost built from the Recognition cost $J$.
By the forcing chain, $J$ is the unique nonnegative cost compatible with the Recognition Composition Law, normalized so $J(1)=0$. Equivalently $J(x)=(x+x^{-1})/2-1$, or as a squared ratio $J(x)=(x-1)^2/(2x)$. Domain cost applies $J$ to a ratio of two nonzero reals, so it measures mismatch between a predicted scale and a reference.
The upstream lemma used here states exactly that unit root: $J(1)=0$.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J$ of the ratio $r/r$. Rewrite that ratio by the field identity $\mathrm{div_self}$ (using $r\neq 0$) to obtain $J(1)$. Discharge with the upstream unit lemma $J(1)=0$.
why it matters
Supplies the diagonal vanishing identity that any matched-scale certificate in this module needs: zero defect on the nose when the two arguments agree. Sibling lemmas (nonnegativity of domain cost, positivity of the canonical threshold) and the module certificate RSPhysics011Cert sit on top of this baseline. In the broader RS picture it is the local instance of $J(1)=0$ inside mass-ladder language, consistent with T5 J-uniqueness and the phi-ladder mass formula. No external dependents are recorded yet; the result is infrastructure for the Z-boson structural match claimed by the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.