domainCost_at_eq
plain-language theorem explainer
For any nonzero real scale r, the domain cost of matching r against itself is exactly zero. Forcing-chain and eight-tick arguments that need a zero baseline on equal scales cite this identity. The proof is a one-line wrapper: unfold the cost, cancel the ratio to 1, and apply the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: the $J$-cost of the self-ratio equals zero.
background
Module 2 of the RS forcing chain records the eight-tick structural layer: period $2^D = 2^3 = 8$ recognition states per epoch, forced once spatial dimension is $D=3$. Status is structural (no sorry, no axioms).
The cost functional $J$ is the unique nonnegative defect on positive reals fixed by the Recognition Composition Law; equivalently $J(x)=(x-1)^2/(2x)$, and $J(1)=0$. Domain cost of two nonzero scales is the $J$-cost of their ratio. The upstream lemma Jcost_unit0 states exactly $J(1)=0$, which is the algebraic root used here.
proof idea
One-line wrapper. Unfold the definition of domain cost (ratio form), rewrite $r/r=1$ by div_self using the hypothesis $r\neq 0$, then close by the upstream unit identity $J(1)=0$.
why it matters
Supplies the diagonal vanishing identity for domain cost inside the eight-tick forcing module. That module packages the T7 landmark (period $2^3=8$ states per recognition epoch, forced by $D=3$). No downstream theorem edges are recorded yet; the result sits beside nonnegativity and canonical-threshold lemmas that feed the module certificate RSForcingChain002Cert. Without diagonal zero, equal-scale comparisons would carry a spurious positive defect and break the zero-baseline of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.