domainCost_at_eq
plain-language theorem explainer
The domain cost of any nonzero real scale against itself is zero. Anyone normalizing recognition costs on the phi-ladder or checking that the diagonal of a two-argument cost vanishes will cite this. The proof unfolds the cost, cancels the ratio by nonzero division, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of $r$ against itself is zero: $\mathrm{domainCost}(r,r) = 0$. Equivalently, after reducing the ratio $r/r$ to $1$, one recovers $J(1) = 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)$ for $x > 0$. The unit identity $J(1) = 0$ is the algebraic fixed point of that cost (lemma Jcost_unit0).
In this module the two-argument domain cost is the J-cost of a ratio of real scales: evaluating it on a pair $(r,s)$ reduces to $J(r/s)$ (when $s \neq 0$). The present statement is the diagonal specialization.
Module 5 is the structural QCD count-law package: the one-loop coefficient $b_0 = 7 = 2^D - 1$ forced by spatial dimension $D = 3$ (forcing chain T8). Domain-cost identities sit underneath any later comparison of running scales or thresholds in that package.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r) = 0$. Rewrite the ratio by div_self using $r \neq 0$, obtaining $J(1) = 0$. Discharge by the upstream lemma Jcost_unit0, which is itself a one-line simplification of the closed form of $J$.
why it matters
A normalization lemma: any cost used to compare physical scales must vanish when the two arguments coincide. Without it, later nonnegativity and threshold statements in the same module (domainCost_nonneg, canonicalThreshold_pos, and the RSPhysics005Cert bundle) would not sit on a coherent zero of the cost.
In the broader RS chain this is the cost-side counterpart of T5 J-uniqueness and the Recognition Composition Law: $J$ is pinned so that the self-ratio is exactly the unit root. The module itself targets the Count Law $b_0^{\mathrm{QCD}} = 7 = 2^D-1$ forced by $D=3$; a clean diagonal zero keeps scale comparisons honest before that coefficient is read off.
No downstream dependents are recorded yet; the lemma is infrastructure for the Module 5 certificate rather than a cited parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.