domainCost_at_eq
plain-language theorem explainer
For any nonzero real r, the domain cost of matching r against itself is zero. Vacuum-counting and landscape-normalization arguments in the RS string-landscape module rely on this diagonal vanishing. 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 cost evaluates to $0$.
background
The ambient module compares the string-theory vacuum landscape (~$10^{500}$ vacua) with an RS phi-ladder count, treating the comparison as a structural theorem (no sorry, no axioms). Costs are measured by the Recognition J-functional from the Cost import.
Upstream, $J$ is the unique cost fixed by the Recognition Composition Law; in closed form $J(x)=(x-1)^2/(2x)$, and the unit lemma records $J(1)=0$. The local domain cost is the J-cost of a ratio of two real scales: after unfolding, the diagonal case is exactly $J(r/r)$.
The nonzero hypothesis is required so the ratio is defined and equals 1 by cancellation.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose a J-cost of a quotient; rewrite the quotient by div_self using $r\neq 0$, obtaining $J(1)$; finish by the upstream unit lemma Jcost_unit0, which states $J(1)=0$.
why it matters
Diagonal vanishing is the normalization that lets landscape comparisons treat self-matched domains as zero-defect baselines rather than free parameters. In the RS string-landscape module it sits beside nonnegativity of domain cost and the canonical threshold, feeding the structural certificate that the RS vacuum count is not a $10^{500}$-scale landscape. It is the cost-side counterpart of the T5 J-uniqueness landmark: once $J$ is fixed, self-ratios must cost nothing. No downstream theorems currently cite it; its role is local hygiene inside the landscape certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.