domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain arguments incur zero cost: comparing a scale to itself is free. Physicists checking that the RS domain-cost functional is a true defect (vanishes on the diagonal) would cite this. The proof is a one-line unfold-and-cancel: the ratio becomes 1 and J(1)=0 applies.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero. Equivalently, if domain cost is $J(x/y)$ with $J$ the Recognition cost, then $J(r/r)=J(1)=0$.
background
The module is a structural milestone certificate (FinalModule_1399, Plan v7): zero sorry, zero axioms, aimed at domain-coverage bookkeeping in Recognition Science physics.
The cost functional $J$ (here Jcost) is the unique nonnegative defect fixed by the Recognition Composition Law and T5 uniqueness: $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. Upstream lemma Jcost_unit0 records the normalization $J(1)=0$.
Domain cost is the pairwise comparison obtained by feeding the ratio of the two domain values into $J$. On the diagonal $r/r$ the ratio is the multiplicative unit, so the cost must vanish whenever $r\neq 0$.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio of the two arguments). Rewrite $r/r=1$ via div_self using the hypothesis $r\neq 0$. Finish by the upstream unit lemma $J(1)=0$.
why it matters
Places the domain-cost functional on the same footing as the abstract $J$-cost: it is a true defect, zero exactly when the two domain scales coincide (nonzero). That is the minimal sanity check before any threshold or coverage certificate can treat unequal domains as costly.
The module frames this as part of a structural domain-coverage milestone (no sorry, no axioms). No downstream dependents are recorded yet; sibling declarations (canonicalThreshold, MilestoneCert, cert) are the natural consumers for positivity and certificate packing.
Framework link: rests on T5 $J$-uniqueness and the unit normalization of $J$, not on the later forcing steps (phi, eight-tick, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.