domainCost_at_eq
plain-language theorem explainer
When both arguments of the domain cost are the same nonzero real, the cost is exactly zero. Cosmologists auditing the RS CMB anisotropy certificate cite this as the on-diagonal normalization of the J-cost domain functional. The proof is a one-line unfold that reduces the ratio to 1 and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost evaluated on the diagonal pair $(r,r)$ is zero.
background
The module gives a structural account of CMB temperature anisotropy from the Recognition Science J-cost. The observational target is $\Delta T/T \sim 10^{-5}$; RS compares this to $J(\phi)^{D+1}=J(\phi)^4\approx 2\times 10^{-4}$ with $D=3$.
The cost $J$ is the unique nonnegative functional forced by the Recognition Composition Law. It satisfies $J(1)=0$ and admits the closed form $J(x)=(x-1)^2/(2x)$. Domain cost is the local specialization used by the matter-perturbation certificate in this file: it feeds $J$ a ratio of two real scales.
Upstream, the unit-root lemma records $J(1)=0$ by direct simplification of that closed form.
proof idea
One-line wrapper. Unfold the definition of domain cost (J applied to a ratio), rewrite $r/r$ to $1$ by the nonzero-division identity, then apply the unit-root lemma $J(1)=0$.
why it matters
Fixes the diagonal baseline: equal scales carry zero domain cost, so only mismatches generate cost. That baseline is what the MatterPert4 certificate and its nonnegativity/threshold siblings measure against when they compare RS J-cost amplitude to the observed $\Delta T/T$ band. The module is marked structural (zero sorry, zero axiom) and sits in the cosmology lane that links T5 J-uniqueness and T8 ($D=3$) to the eight-tick octave scaling $J(\phi)^4$. No external dependents are recorded yet; the result is local infrastructure for the same-file certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.