domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain cost vanish: the cost of the self-ratio is zero. Cost-normalization and forcing-chain arguments cite this as the diagonal baseline. Proof is a one-line unfold-and-rewrite to the unit-zero lemma for J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero. Equivalently, if domain cost is the $J$-cost of the argument ratio, then $J(r/r) = 0$.
background
Module 6 of the RS forcing chain records the structural claim that spatial dimension $D=3$ is forced by the eight-tick period $2^3$, with no free parameters (status: structural theorem, zero sorry, zero axiom).
The underlying cost is the Recognition $J$-functional $J(x)=(x+x^{-1})/2-1$, also written $(x-1)^2/(2x)$. It is the unique cost compatible with the Recognition Composition Law. Domain cost applies that functional to a ratio of two real scales: on the diagonal the ratio is $1$.
Upstream, Jcost_unit0 states the normalization $J(1)=0$, obtained by direct simplification of the closed form.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite $r/r=1$ by the nonzero self-division rule, then discharge with the unit-zero lemma $J(1)=0$.
why it matters
Gives the diagonal baseline for domain cost inside the $D=3$ forcing module (T7 eight-tick octave, T8 three spatial dimensions). Sibling facts on nonnegativity and the canonical threshold sit on the same cost; this lemma pins the zero of that cost at equal scales. No external used-by edges are recorded yet; the result is local certificate infrastructure for the structural chain rather than a paper-level proposition on its own.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.