domainCost_at_eq
plain-language theorem explainer
The domain cost of any nonzero real against itself is zero. Mass-ratio and scale-comparison arguments in the RS physics stack cite this as the diagonal normalization of the cost. The proof unfolds the cost to J of a ratio, collapses the ratio to 1, and applies the unit-zero lemma for J.
Claim. For every real $r\neq 0$, the domain cost of the pair $(r,r)$ vanishes: the cost of matching a nonzero scale to itself is $0$.
background
Recognition Science measures scale mismatch by the J-cost
$J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$, which is zero only at the unit $x=1$. The upstream lemma Jcost_unit0 records exactly that identity: $J(1)=0$.
This module (Physics RS Module 9) is the structural treatment of the proton-electron mass ratio, with the native ladder value $\phi^{12}\approx 321.9$ and an acknowledged factor-$\sim 5.7$ gap to the experimental $\sim 1836$. Domain cost is the J-cost of a ratio of two nonzero real scales; evaluating it on equal arguments is the basic normalization that the cost is a true defect relative to identity matching.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J$ of the ratio $r/r$. Rewrite that ratio to $1$ by div_self (using $r\neq 0$), then finish by the upstream unit-zero lemma $J(1)=0$.
why it matters
Gives the diagonal vanishing law for domain cost inside the Module 9 structural certificate (proton-electron mass ratio, status: structural theorem, zero sorry). No downstream dependents are wired yet; siblings cover nonnegativity, the canonical threshold, and the module certificate pack.
In the broader forcing chain this is the local instance of T5 J-uniqueness at the unit: cost is a genuine defect, zero precisely when the compared scales match. It does not close the $\phi^{12}$ versus $1836$ gap noted in the module header; it only certifies that the cost geometry used for that comparison is normalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.