domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain values incur zero recognition cost: domainCost(r,r)=0 whenever r≠0. Physicists checking the W-boson mass ladder (Module 12) cite this as the diagonal normalization of the cost used in threshold comparisons. The proof is a one-line unfold-and-rewrite to J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of $r$ against itself vanishes: $\mathrm{domainCost}(r,r) = 0$.
background
Module 12 of the RS physics stack records the structural W-boson mass match $M_W \approx 80.4,\mathrm{GeV} \sim \varphi^{13}\cdot 0.154 \approx 80.3,\mathrm{GeV}$. The local cost primitive is the standard Recognition J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$ on positives, imported from Cost.
Domain cost is the J-cost of a ratio of two real domain parameters. On the diagonal the ratio is identically 1 (when the common value is nonzero), so the cost collapses to the unit value of $J$. Upstream, $J(1)=0$ is already recorded as the elementary identity Jcost_unit0.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite $r/r=1$ by div_self using the hypothesis $r\neq 0$, then apply the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the normalization that lets later nonnegativity and threshold lemmas treat domain cost as a genuine defect: zero exactly on matched parameters, positive off-diagonal. In Module 12 that underwrites the structural certificate comparing the observed W mass to the $\varphi$-ladder prediction. No downstream consumers are wired yet in the graph; the lemma sits as local infrastructure beside domainCost_nonneg and canonicalThreshold. It is pure cost algebra (T5 J-uniqueness background), not a mass derivation itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.