domainCost_at_eq
plain-language theorem explainer
On any nonzero real scale r, the domain cost of the diagonal pair (r,r) is exactly zero. Cosmology arguments that need a clean zero baseline when two scale factors coincide (e.g. equal Hubble or expansion ratios) cite this identity. The proof is a one-line unfold of the domain cost to J of a ratio, cancel the ratio to 1, and apply the unit root of J.
Claim. For every real number $r \neq 0$, the domain cost of the diagonal pair equals zero: if the cost is the $J$-cost of the ratio of its two arguments, then that cost at $(r,r)$ is $0$.
background
Recognition Science measures scale mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. By construction $J(1)=0$, and that is the unique nonnegative root on the positive reals. The present module (Cosmology RS Module 3) collects structural identities used around the Hubble-tension band $H_{0,\mathrm{local}}/H_{0,\mathrm{CMB}}\in(1.075,1.091)$, with SH0ES 1.0837 inside; status is a structural theorem pack with no sorry and no axioms.
Domain cost is the J-cost of the ratio of two real arguments. The only upstream fact needed here is the unit-root lemma: $J(1)=0$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite with div_self using $r\neq 0$ to replace the ratio by $1$. Finish by the upstream lemma $J(1)=0$.
why it matters
Gives the diagonal zero for domain cost inside the cosmology module that targets the Hubble tension ratio band. No downstream dependents are recorded yet; siblings include nonnegativity of domain cost, a canonical threshold, and the module certificate RSCosmo003Cert. In the broader RS chain this is local bookkeeping for J (T5 J-uniqueness / RCL), not a new forcing step: it only guarantees that equal nonzero scales carry zero mismatch cost before thresholds or pass/fail certificates are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.