domainCost_at_eq
plain-language theorem explainer
On the diagonal, domain cost vanishes: for any nonzero real scale r the cost of the matched pair (r,r) is zero. Calibration and threshold arguments that need a zero baseline for equal ratios cite this identity. The proof unfolds the cost definition, cancels the ratio to 1, and applies the unit root of J.
Claim. For every real number $r \neq 0$, the domain cost of the matched pair equals zero: $C_{\mathrm{dom}}(r,r)=0$.
background
Module 10 of the RS foundation chain treats calibration: $E_{\mathrm{coh}}$ is the single free parameter, fixed by the electron mass at rung 3. The module is marked structural (no sorry, no axioms).
The cost function $J$ (also written $J_{\mathrm{cost}}$) is the unique nonnegative functional forced by the Recognition Composition Law, with closed form $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. In particular $J(1)=0$. Domain cost is the local specialization that feeds a ratio of two real scales into $J$; on equal nonzero arguments that ratio is identically 1.
Upstream, the lemma $J(1)=0$ is the only external fact required.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $J(r/r)=0$. Rewrite $r/r=1$ by the nonzero-division identity, then finish with the unit root lemma $J(1)=0$.
why it matters
Gives the zero baseline for matched scales inside the Module 10 calibration layer. Sibling results (nonnegativity of domain cost, positivity of the canonical threshold, and the module certificate) sit on top of this identity: without a clean diagonal zero, threshold comparisons and certificate packing would need ad-hoc case splits.
In the broader forcing chain this is the local echo of T5 (J-uniqueness): the same $J$ that is forced globally has a unit root, so equal ratios carry zero recognition cost. No downstream consumers are wired yet in the graph; the lemma is infrastructure for the structural certificate of the module rather than a step in a longer named theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.