domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain cost vanish: the cost of comparing a scale to itself is zero. Anyone building the RS gap-45 / D=3 forcing chain cites this as the diagonal normalization of the cost. The proof unfolds the cost, cancels the ratio to 1, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero: $\mathrm{domainCost}(r,r)=0$. Equivalently, if the cost is $J(r/r)$ with $J$ the Recognition cost, then $J(1)=0$.
background
Module 3 of the RS forcing chain records the structural gap $g_D=D^2(D+2)$, which equals 45 at $D=3$, the minimum depth for self-reference. The local cost used here is the domain cost: on nonzero reals it is the Recognition cost $J$ evaluated at the ratio of the two arguments.
The Recognition cost $J$ (also written $J_{\mathrm{cost}}$) is the unique nonnegative generator fixed by the Recognition Composition Law; one closed form is $J(x)=(x-1)^2/(2x)$, equivalently $(x+x^{-1})/2-1$. Upstream, $J(1)=0$ is already recorded as the unit root of that cost. The present lemma is the diagonal specialization: when both domain arguments coincide and are nonzero, the ratio is 1 and the cost collapses to that unit root.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite the ratio by $r/r=1$ (using $r\neq 0$), then apply the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the normalization that any cost-based forcing step needs before comparing distinct scales. In this module it sits beside nonnegativity of the domain cost and the canonical threshold, feeding the structural certificate that $g_D=45$ at $D=3$ (T8 in the forcing chain: three spatial dimensions). No downstream theorems are wired yet in the graph; the lemma is infrastructure for the gap-45 self-reference argument rather than a leaf identity. It does not itself force $D=3$; it only clears the equal-argument case of the cost used in that argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.