domainCost_at_eq
plain-language theorem explainer
The domain cost of any nonzero real against itself is zero. Scale-comparison arguments in the Recognition cost calculus cite this diagonal identity as a baseline sanity check. The proof unfolds the ratio definition, reduces to the unit argument, and applies the known vanishing of J at 1.
Claim. For every real number $r \neq 0$, the domain cost evaluated at equal arguments vanishes: the cost of the pair $(r,r)$ is $0$.
background
Recognition Science measures scale mismatch by the J-cost $J(x)=(x-1)^2/(2x)$, equivalently $(x+x^{-1})/2-1$, which is zero only at the unit $x=1$. The upstream lemma records exactly that unit identity: $J(1)=0$.
Domain cost applies $J$ to a ratio of two real scales, so it vanishes precisely when those scales agree (and the ratio is defined). This module sits in the physics layer whose stated goal is a structural solution of the strong CP problem: QCD $\theta=0$ forced by eight-tick uniqueness, with status structural theorem (zero sorry, zero axiom).
proof idea
One-line wrapper. Unfold the domain-cost definition (J of the argument ratio), rewrite $r/r=1$ from the nonzero hypothesis, and discharge with the lemma $J(1)=0$.
why it matters
Module 8 claims QCD $\theta=0$ from eight-tick uniqueness (forcing-chain landmark T7, the period-$2^3$ octave). A zero diagonal for domain cost is a prerequisite sanity fact: identical nonzero scales must carry zero recognition cost before cost comparisons can force CP-odd phases to vanish. No recorded downstream dependents yet; the result sits with sibling facts (nonnegativity, canonical threshold) that feed the module certificate. It does not itself solve strong CP; it clears a definitional obligation inside that structural argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.