domainCost_at_eq
plain-language theorem explainer
When both domain arguments are the same nonzero real, the domain cost is exactly zero. Cosmology certificates that compare a scale factor (or density parameter) to itself rely on this normalization identity. The proof unfolds the cost, cancels the ratio to 1, and applies the unit root of the J-cost.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: if the cost is $J(r/r)$ with $J$ the Recognition cost, then $J(1)=0$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$ for $x>0$. A basic fact is that the unit is a root: $J(1)=0$.
This module (Cosmology RS Module 1) packages structural identities used in the RS dark-energy comparison $\Omega_\Lambda=11/16-\alpha/\pi\approx 0.685$ against Planck. The local domain cost is the J-cost of a ratio of two real domain parameters (scale factors, densities, or similar positive quantities), so equal nonzero arguments force the ratio to 1.
Upstream, Jcost_unit0 records exactly $J(1)=0$ by unfolding the definition of $J$.
proof idea
One-line wrapper. Unfold the domain-cost definition (ratio of the two arguments fed to $J$). Rewrite the ratio by div_self using $r\neq 0$, obtaining $J(1)$. Finish with the upstream lemma $J(1)=0$.
why it matters
Gives the diagonal normalization for domain cost inside the first cosmology certificate module. Without $J(1)=0$ on equal arguments, threshold and nonnegativity siblings cannot treat self-comparison as a zero baseline when certifying the $\Omega_\Lambda$ structural match (RS_PASS, 0.665$\sigma$ vs Planck). No downstream dependents are recorded yet; the lemma is infrastructure for the module's certificate bundle rather than a forcing-chain step (T5--T8). It sits on the cost layer imported from Constants/Cost, not on the eight-tick or $D=3$ landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.