domainCost_at_eq
plain-language theorem explainer
When both scale arguments of the domain cost are the same nonzero real, the cost is exactly zero. Cosmology arguments that need a vanishing baseline at matched reionization scales cite this identity. The proof is a one-line unfold of the cost, reduction of the ratio to 1, and the unit root of J.
Claim. For every real $r \neq 0$, the domain cost evaluated on the diagonal pair $(r,r)$ equals $0$.
background
Module 8 of the RS cosmology stack treats reionization as a structural match of the $\phi$-ladder window $\phi^4$ to $\phi^5$ (numerically about $6.85$–$11.09$) against observed $z_{\mathrm{reion}}\sim 7$–$10$. The local cost primitive is the Recognition $J$-cost $J(x)=(x+x^{-1})/2-1$, equivalently $(x-1)^2/(2x)$, which vanishes only at the unit ratio.
In this file the domain cost of a pair of positive scales is the $J$-cost of their ratio. The upstream lemma Jcost_unit0 records the normalization $J(1)=0$, which is the algebraic root of every diagonal vanishing statement in the cost calculus.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite the ratio by div_self using $r\neq 0$, obtaining $J(1)=0$, then close by the upstream lemma that $J(1)=0$.
why it matters
Diagonal vanishing is the zero baseline for any comparison of reionization scales: without it, nonnegativity and threshold certificates in the same module have no calibrated origin. The module is marked structural (zero sorry, zero axiom) and sits in the cosmology forcing path that ties the $\phi$-ladder window $\phi^4$–$ \phi^5$ to the observed reionization redshift band. Sibling facts (nonnegativity of domain cost, positivity of the canonical threshold, and the module certificate) rest on this identity even though no downstream edge is recorded yet. It is the cost-side instance of the T5 normalization $J(1)=0$ inside the cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.