domainCost_at_eq
plain-language theorem explainer
When the two scale arguments of the cosmological domain cost coincide and are nonzero, the cost is exactly zero. Cosmologists in the Recognition Science vacuum model cite this as the on-diagonal normalization of domain cost. The proof is a one-line unfold: the ratio collapses to 1 and J(1)=0 finishes it.
Claim. For every real $r\neq 0$, the cosmological domain cost of the equal pair $(r,r)$ vanishes: the cost of matching scales is $0$.
background
The Recognition Science cost is the unique J-functional $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $J(x)=\frac{(x-1)^2}{2x}$. Its elementary normalization is $J(1)=0$ (lemma Jcost_unit0). In this cosmology module the domain cost of a pair of scales is $J$ of their ratio, so equal nonzero arguments feed $J(1)$.
The module develops structural RS vacuum consequences for late-time cosmology. Status is a structural theorem (0 sorry, 0 axiom): the dark-energy equation of state is forced to $w=-1$ exactly; any DESI Y3 deviation from $w=-1$ at $2\sigma$ would falsify RS.
proof idea
One-line wrapper. Unfold the domain-cost definition (ratio of the two arguments into $J$), rewrite $r/r=1$ from the nonzero hypothesis via div_self, and apply the upstream lemma $J(1)=0$.
why it matters
Pins the on-diagonal zero of domain cost: matching cosmological scales carry zero RS cost. That zero is the natural base point for nonnegativity and threshold lemmas in the same file (domain-cost nonnegativity, canonical threshold). The parent module aims at the exact $w=-1$ vacuum prediction from RS; no external dependents are recorded yet. The step rests on T5 J-uniqueness, which forces $J(1)=0$ as the unique minimum of the cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.