domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain arguments force the domain cost to vanish. Anyone checking the pure-interference (wave) limit of RS wave-particle duality cites this. The proof is a one-line unfold: the ratio collapses to 1 and J(1)=0.
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 ratio of the two arguments, then $J(r/r)=0$.
background
The module treats wave-particle duality as a continuous transition in the Recognition Science $J$-cost between a pure-interference (wave) limit and a pure-detection (particle) limit. Module status is structural: zero sorry, zero axiom.
The cost functional is the unique $J$ forced by the Recognition Composition Law, normalized so $J(1)=0$ and $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$). Domain cost is the $J$-cost of a ratio of two real path/domain quantities (interference versus detection amplitudes or measures).
Upstream, Jcost_unit0 records the unit normalization $J(1)=0$, which is the algebraic content of the pure-interference fixed point.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the claim becomes $J(r/r)=0$), rewrite $r/r=1$ by div_self using $r\neq 0$, then apply the unit lemma $J(1)=0$.
why it matters
Anchors the wave end of the RS complementarity story: pure interference is exactly the $J=0$ locus, matching the module claim that complementarity is a continuous $J$-cost transition from wave ($J=0$) to particle ($J=1$). It sits in the Foundation layer that derives wave-particle structure from $J$-uniqueness (forcing-chain T5) rather than from a separate dual ontology.
No downstream edges are recorded yet; sibling lemmas (nonnegativity of domain cost, canonical threshold positivity, the WPDuality3 certificate) are the natural consumers. Closes the equal-argument base case needed before any threshold or certificate argument can treat the interference limit as identically cost-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.