domainCost_at_eq
plain-language theorem explainer
Equal nonzero radii incur zero domain cost: comparing a scale to itself is free. Cosmology modules that calibrate thresholds or certify structural certificates cite this identity as the zero anchor of the cost. The proof is a one-line unfold-and-rewrite that reduces the ratio to 1 and applies the unit root of J.
Claim. For every real number $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: evaluating the cost on a scale against itself yields $0$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. The unit root is elementary: $J(1)=0$. In this cosmology structural module the domain cost of two positive scales is that J-cost applied to their ratio, so equal arguments collapse to the unit.
The module sets the coherence energy once from the electron mass and then runs parameter-free structural claims. Status is a pure structural theorem block: zero sorry, zero axiom. Upstream, the Cost library already records $J(1)=0$ as Jcost_unit0, which is the only lemma this identity needs.
proof idea
One-line wrapper. Unfold the domain-cost definition (ratio of the two arguments fed to J). Rewrite $r/r=1$ by the nonzero-division identity, then finish with the upstream unit root $J(1)=0$.
why it matters
Gives the zero locus of the domain cost used throughout the RS cosmology structural stack (siblings include nonnegativity of the cost, the canonical threshold, and the structural certificate for module 10). Without a clean zero at equal scales, threshold comparisons and calibration statements would float. It sits on the T5 J-uniqueness landmark: the same J forced by the Recognition Composition Law is the cost whose unit root anchors free self-comparison. No downstream consumers are wired yet in the graph; the lemma is local infrastructure for the certificate and for any later inequality that subtracts the equal-scale baseline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.