domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain arguments give vanishing domain cost: the J-cost of the self-ratio is zero. Cosmology and cost-structure arguments cite this as the diagonal baseline before comparing distinct scales. The proof unfolds the cost definition, reduces the ratio to 1, and applies the unit-zero lemma for J.
Claim. For every real $r \neq 0$, the domain cost at equal arguments vanishes: the cost of the pair $(r,r)$ equals $0$.
background
Recognition Science measures scale mismatch with the J-cost $J(x)=\frac{(x-1)^2}{2x}$ (equivalently $\frac{x+x^{-1}}{2}-1$), which is zero only at the unit ratio. In this module the domain cost is that J-cost applied to a ratio of two domain parameters, so equal nonzero arguments reduce to $J(1)$.
The local setting is Cosmology RS Structural Module 3: the RS count law $2^D-1=7$ independent channels forced by configuration dimension $D=3$, packaged as a structural theorem with no sorry and no axioms. The present identity is a local algebraic fact used when a domain parameter is compared to itself.
Upstream, Jcost_unit0 records $J(1)=0$ by direct simplification of the cost definition.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J$ of the ratio $r/r$. Rewrite that ratio to $1$ by div_self (using $r\neq 0$). Finish with the upstream lemma $J(1)=0$.
why it matters
Supplies the diagonal zero for domain cost inside the structural cosmology certificate of this module (siblings cover nonnegativity, the canonical threshold, and the inhabited certificate). Zero self-cost is the baseline against which nonzero cost signals genuine scale mismatch on the phi-ladder and in channel-counting arguments.
It sits under the T5 J-uniqueness landmark: $J$ is the unique cost compatible with the recognition composition law, and $J(1)=0$ is its normalization. No external used-by edges are recorded yet; the lemma is consumed locally by the module's certificate stack rather than by a named parent theorem outside the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.