domainCost_at_eq
plain-language theorem explainer
For any nonzero real r, the domain cost of r against itself is zero. Anyone verifying that Recognition domain cost is a true defect (vanishes on the diagonal) cites this. The proof unfolds the cost to J of a ratio, cancels r/r to 1, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of matching $r$ to itself vanishes: the cost evaluates to $0$.
background
The ambient module is a Recognition Science structural certificate (FinalModule_1397): a milestone pack with zero sorry and zero axioms, aimed at domain-coverage bookkeeping rather than new physics constants.
The cost in play is the standard Recognition J-cost. Upstream, $J(1)=0$ is recorded as a one-line simplification of the closed form $J(x)=(x-1)^2/(2x)$ (equivalently $J(x)=\cosh(\log x)-1$). Domain cost is the local wrapper that feeds a ratio of two reals into that J-cost; the present lemma is the diagonal specialization.
The nonzero hypothesis is forced by the ratio: without $r\neq 0$ the quotient is undefined, so the statement is exactly the defect property on the punctured line.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J$ of a ratio; rewrite the ratio by div_self using $r\neq 0$ to obtain $J(1)$; finish by the upstream lemma $J(1)=0$.
why it matters
Inside the FinalModule_1397 milestone, this pins the elementary sanity check that domain cost is a true defect: zero precisely when the two arguments coincide (here, on the diagonal). That is prerequisite bookkeeping for any later claim that a canonical threshold or coverage certificate is measuring genuine mismatch rather than an offset.
No downstream consumers are wired yet in the graph; the lemma sits as local infrastructure beside canonicalThreshold and the MilestoneCert bundle. Framework-wise it rests only on the T5 J-cost (unique cost solving the Recognition Composition Law) and its unit root, not on phi, the eight-tick octave, or the dimension forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.