domainCost_at_eq
plain-language theorem explainer
For any nonzero real scale r, matching r against itself incurs zero domain cost. Cosmology and cost-geometry arguments cite this to fix the zero of the recognition cost on equal scales. The proof is a one-line wrapper: unfold the cost, reduce the self-ratio to 1, and apply the unit identity J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: the $J$-cost of the scale ratio $r/r$ equals $0$.
background
Recognition Science measures scale mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. This cost is nonnegative and vanishes only at the unit ratio $x=1$. In this module the domain cost on a pair of real scales is the J-cost of their ratio.
The local setting is Cosmology RS Structural Module 2, a zero-sorry structural pack around the golden-ratio recognition cost: $J(\varphi)=\varphi-3/2\approx 0.118$. The module records baseline identities for that cost geometry before threshold and certificate work.
Upstream, the unit lemma states $J(1)=0$ by direct simplification of the closed form of $J$. That single identity is the only external fact needed here.
proof idea
One-line wrapper. Unfold the domain-cost definition (J of the scale ratio), rewrite $r/r=1$ by division with the nonzero hypothesis, then apply the unit lemma $J(1)=0$.
why it matters
Fixes the calibrated zero of the cosmology domain cost on the diagonal, so nonnegativity, thresholds, and certificate packing in the same module sit on a known baseline. The module status is structural theorem (0 sorry, 0 axiom), centered on the golden-ratio cost $J(\varphi)=\varphi-3/2$.
No downstream consumers appear in the dependency graph yet; siblings include domain-cost nonnegativity, the canonical threshold, and the RS-COS-Structural-002 certificate. Framework landmark: T5 J-uniqueness forces this same $J$ as the unique cost obeying the Recognition Composition Law with unit minimum at 1, so the diagonal vanishing is not an extra axiom but a consequence of that forced cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.