domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain cost vanish. Cite this when normalizing BIT-kernel vacuum bookkeeping or any J-cost ratio on the diagonal. The proof unfolds the cost to J of a ratio, collapses the ratio to 1, and applies the unit-zero identity for J.
Claim. For every real $r\neq 0$, the domain cost of the pair $(r,r)$ is zero.
background
The module builds the BIT kernel family (deep v4) from the J-cost. In Recognition Science the cost is $J(x)=(x+x^{-1})/2-1$, equivalently $(x-1)^2/(2x)$, forced unique at T5 of the forcing chain and obeying the Recognition Composition Law. The upstream unit lemma states $J(1)=0$.
Domain cost is the J-cost of the ratio of two real scales. The module setting treats bosonic vacuum fluctuations as $J(\varphi)/45$ per recognition tick, with cumulative cosmic Z-aging linear in tick count. Diagonal vanishing is the normalization that equal scales carry no defect.
proof idea
One-line wrapper. Unfold domain cost (J of the ratio of its two arguments), rewrite $r/r=1$ from the nonzero hypothesis, and finish by the upstream lemma $J(1)=0$.
why it matters
Supplies the diagonal normalization for domain cost inside the BIT-kernel deep layer. Sibling results (nonnegativity, canonical threshold positivity, the BITKernel4 deep certificate) sit on the same cost surface; this fact pins the zero of that surface. It is foundation infrastructure for vacuum-fluctuation bookkeeping tied to J and $\varphi$, not a forcing-chain step itself. No external used-by edges are recorded yet; the lemma is local scaffolding for the module certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.