domainCost_at_eq
plain-language theorem explainer
When both scale arguments of the domain cost agree and are nonzero, the cost is exactly zero. Cosmology arguments that need a clean diagonal baseline for equal-domain comparisons cite this identity. The proof is a one-line unfold of the cost, rewrite of the self-ratio to 1, and the unit root of J.
Claim. For every real number $r \neq 0$, the domain cost of the equal pair vanishes: the cost of $(r,r)$ equals $0$.
background
Recognition Science measures scale mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$, also written $(x-1)^2/(2x)$. That cost is nonnegative and vanishes only at the unit $x=1$. The cosmology modules package a two-argument domain cost that feeds a ratio of scales into $J$.
This file is Cosmology RS Module 7, whose structural target is matter-radiation equality: $\varphi^{17}\cdot 0.95$ recovers $z_{\mathrm{eq}}\sim 3400$, matching the empirical value. Equal-domain comparisons need a zero when the two arguments coincide.
Upstream, the Cost library records $J(1)=0$ as a one-line simplification of the definition of $J$.
proof idea
One-line wrapper. Unfold the domain-cost definition (it applies $J$ to the ratio of its two arguments). Rewrite $r/r=1$ by division-by-self, using the hypothesis $r\neq 0$. Close with the Cost lemma $J(1)=0$.
why it matters
Supplies the diagonal vanishing law for domain cost inside the Module 7 cosmology certificate stack (matter-radiation equality on the $\varphi$-ladder). No recorded downstream dependents yet; sibling facts cover nonnegativity, the canonical threshold, and the inhabited certificate. In the broader forcing picture this is local cost geometry, not a T0-T8 step, but it underwrites clean equal-scale baselines used when matching $z_{\mathrm{eq}}\sim 3400$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.