domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain arguments have vanishing domain cost. Cosmology and cost-functional arguments cite this as the diagonal zero of the scale-pair cost. The proof unfolds the definition, reduces the ratio to 1, and applies J(1)=0.
Claim. For every real $r\neq 0$, the domain cost of the pair $(r,r)$ is zero.
background
Recognition Science measures mismatch of positive scales by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $(x-1)^2/(2x)$. The unit identity $J(1)=0$ is the algebraic fixed point of that cost.
This module (Cosmology RS Module 6) is a structural, zero-sorry package around a dark-matter mass claim $M_W/45\approx 1.787,\mathrm{GeV}$ with a stated XENONnT falsifier window. The local domain cost is the J-cost of a ratio of two real scales; on the diagonal that ratio is 1 whenever the common value is nonzero.
Upstream, Jcost_unit0 records exactly $J(1)=0$ by unfolding the definition of $J$.
proof idea
One-line wrapper. Unfold the domain-cost definition so the goal is a J-cost of a ratio; rewrite that ratio by div_self using $r\neq 0$ to obtain $J(1)$; finish with the upstream lemma $J(1)=0$.
why it matters
Gives the cost functional its expected zero on equal arguments, the minimal sanity check before nonnegativity, thresholds, and certificate packing in the same module (siblings include domain-cost nonnegativity, a canonical threshold, and the RSCosmo006 certificate). In the broader RS forcing picture this is the unit case of T5 J-uniqueness: cost vanishes only at the self-similar fixed point of the ratio. The module frames a testable DM-mass claim; this lemma does not carry the numerics, only the diagonal identity those numerics sit on. No downstream dependents are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.