domainCost_at_eq
plain-language theorem explainer
When both arguments of the domain cost are the same nonzero real scale r, the cost vanishes. Cosmology and RS cost users cite this as the diagonal normalization of the two-argument domain cost. The proof is a one-line unfold: the ratio becomes 1 and Jcost_unit0 applies.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero: $\mathrm{domainCost}(r,r) = 0$. Equivalently, the $J$-cost of the self-ratio $r/r$ is $J(1) = 0$.
background
Module RS_Cosmo_Module_010 is a structural cosmology certificate linking solar metallicity to a pure $J$-cost identity: $J(\varphi)^2 \approx 0.01393$ matches $Z_\odot \approx 0.014$. The local toolkit is the two-argument domain cost built from the Recognition $J$-cost on scale ratios, together with a canonical threshold and a certificate package.
The $J$-cost is the unique nonnegative cost forced by the Recognition Composition Law, with closed form $J(x) = (x-1)^2/(2x)$ (equivalently $\cosh(\log x)-1$). Upstream, Jcost_unit0 records the unit normalization $J(1)=0$. The domain cost of two nonzero scales is the $J$-cost of their ratio; evaluating on the diagonal therefore reduces exactly to that unit identity.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite $r/r$ to $1$ by div_self using $r\neq 0$. Finish by the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the sanity check that the domain cost is a genuine relative cost on cosmological scales: identical scales incur zero cost. In this module it underwrites nonnegativity and threshold comparisons used by the solar-metallicity structural certificate (MATCH of $J(\varphi)^2$ to $Z_\odot$). It sits on the cost layer imported from Constants/Cost rather than on the T0–T8 forcing chain itself, but it inherits the forced $J$ uniqueness (T5) and the unit fixed point of that cost. No downstream dependents are recorded yet; the lemma is local scaffolding for the module certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.