domainCost_at_eq
plain-language theorem explainer
For any nonzero real r, the domain cost of the pair (r,r) is zero. Lattice and forcing-chain arguments cite this as the normalization that equal domain values carry no defect. The proof is a one-line unfold that reduces the ratio to 1 and applies J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: the cost of the ratio $r/r$ equals $0$.
background
Recognition Science derives physics from the single cost $J(x)=\frac12(x+x^{-1})-1$, also written $J(x)=(x-1)^2/(2x)$. The ambient module is Foundation RS Module 1: the recognition lattice, structural theorems only, zero sorry and zero axioms.
Domain cost is the lattice cost of a pair of reals, obtained by feeding their ratio into $J$. The upstream unit lemma records the calibration $J(1)=0$: equal arguments produce the identity ratio and therefore zero defect.
proof idea
One-line wrapper. Unfold domain cost (which applies $J$ to the ratio of its two arguments), rewrite $r/r=1$ from the nonzero hypothesis via div_self, and finish by the unit lemma $J(1)=0$.
why it matters
Structural hygiene for the RS cost calculus that underpins the forcing chain (T5 J-uniqueness and the Recognition Composition Law). It certifies that domain cost is a true defect measure: it vanishes on the diagonal. Sibling results in the same module (nonnegativity of domain cost, the canonical threshold) sit on the same foundation. No recorded downstream edges yet; the lemma is local scaffolding for later lattice identities rather than a paper proposition by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.