domainCost_at_eq
plain-language theorem explainer
On the diagonal, the domain cost of any nonzero real scale against itself is zero. Cosmology arguments that normalize a density or length to the same reference cite this identity. The proof is a one-line unfold: the ratio collapses to 1 and the J-cost of the unit is zero.
Claim. For every real number $r \neq 0$, the domain cost of $r$ compared with itself vanishes: the J-cost of the self-ratio equals zero.
background
Recognition Science measures scale mismatch by the J-cost $J(x)=(x-1)^2/(2x)$, equivalently $(x+x^{-1})/2-1$, which is nonnegative and vanishes only at the fixed point $x=1$. In this module the domain cost of two real arguments is that J-cost applied to their ratio, so equal nonzero arguments force the unit ratio.
The local setting is Cosmology RS Module 9, a structural (zero-sorry) certificate for baryon density: $J(\varphi)(1-J(\varphi))/2\approx 0.052$ against the observed $\Omega_b\approx 0.0493$. Diagonal vanishing is the normalization fact needed before comparing unequal scales or thresholds.
Upstream, the unit lemma records $J(1)=0$ by direct simplification of the closed form of $J$.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(r/r)$. Rewrite the ratio to $1$ by division-by-self (using $r\neq 0$). Finish by the unit lemma $J(1)=0$.
why it matters
Lives in Cosmology RS Module 9, the structural baryon-density block. No recorded downstream dependents yet; it underwrites sibling facts (nonnegativity of domain cost, positivity of the canonical threshold) that support the $\Omega_b$ match. Framework-wise it is the diagonal case of the Recognition cost, consistent with T5 J-uniqueness: the unique admissible cost vanishes at the self-similar fixed point 1. It does not itself produce the baryon fraction; that evaluation is $J(\varphi)(1-J(\varphi))/2$ elsewhere in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.