domainCost_at_eq
plain-language theorem explainer
For any nonzero real scale r, the domain cost of r against itself is zero. Mass-ladder and Higgs-matching arguments in RS Module 10 cite this as the zero-defect baseline on the diagonal. The proof unfolds the cost to J of the ratio, reduces r/r to 1, and applies J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of $r$ against itself vanishes: the cost of the pair $(r,r)$ equals $0$.
background
Recognition Science measures scale mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $(x-1)^2/(2x)$, which is zero only at the unit ratio $x=1$. In this module the domain cost of two real scales is that J-cost applied to their ratio.
Module 10 is the structural Higgs package: $m_H\approx 125.25,\mathrm{GeV}$ is matched to a $\varphi$-ladder rung ($\varphi^{13}$ scaled into GeV). The local setting is zero-sorry structural theorems around that match, not a numerical fit.
Upstream, Jcost_unit0 records the unit identity $J(1)=0$, the exact algebraic fact needed once a ratio collapses to one.
proof idea
One-line wrapper. Unfold the domain-cost definition so the goal is $J(r/r)=0$. Rewrite $r/r=1$ by div_self under the hypothesis $r\neq 0$. Finish by the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the sanity baseline for any cost used to compare mass or coupling scales on the $\varphi$-ladder. Sibling facts (nonnegativity, canonical threshold positivity) and the module certificate RSPhysics010Cert sit on top of a well-behaved cost; without $C(r,r)=0$ those comparisons would be offset. The underlying $J$ is the T5 unique cost from the forcing chain and the Recognition Composition Law. No downstream edges are recorded yet; the lemma is infrastructure inside the Higgs structural module rather than a cited paper proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.