domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain arguments incur zero domain cost. Formalizations of RS wave-function collapse as J-cost minimization to a rung cite this diagonal identity. Proof unfolds the cost, reduces the self-ratio to 1, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of the diagonal pair $(r,r)$ equals zero.
background
The module frames wave-function collapse as ledger posting: a recognition event. Collapse is J-cost minimization onto the nearest rung; the eight-tick cycle fixes the minimal recognition time. Status is structural (0 sorry, 0 axiom).
The cost $J$ obeys $J(1)=0$ (lemma Jcost_unit0), with the squared-ratio form $J(x)=(x-1)^2/(2x)$. Domain cost is the $J$-cost of a ratio of two real domain parameters. On the diagonal the ratio is 1, so the cost vanishes and the landscape is a true defect measure for mismatch.
proof idea
One-line wrapper. Unfold the domain-cost definition, rewrite the self-ratio $r/r$ to $1$ by div_self (using $r\neq 0$), then apply Jcost_unit0, which states $J(1)=0$.
why it matters
Local structural fact in the RS wave-function collapse development. It pins the diagonal of the domain-cost landscape at zero, so cost genuinely measures mismatch between domain values. Sibling lemmas (domainCost_nonneg, canonicalThreshold, the collapse certificate) build nonnegativity and threshold structure on this zero-on-diagonal pattern. Fits the module claim that measurement is pure J-cost minimization with no hidden variables, consistent with the Recognition forcing chain (T5 J-uniqueness).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.