domainCost_at_eq
plain-language theorem explainer
Equal nonzero scales incur zero domain cost: the cost of comparing a real r to itself vanishes. Anyone treating domain cost as a defect measure (zero on the diagonal) would cite this. The proof is a one-line wrapper: unfold the ratio-based definition, cancel r/r to 1, and apply the unit-zero lemma for J.
Claim. For every real $r \neq 0$, the domain cost of the diagonal pair $(r,r)$ is zero.
background
Module FinalModule_1395 is a structural certificate (0 sorry, 0 axiom) for a Recognition Science domain-coverage milestone under Plan v7.
The J-cost is the unique nonnegative cost forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. Upstream lemma records the unit value: $J(1)=0$.
Domain cost compares two real scales by feeding their ratio into J. On the diagonal the ratio is 1, so the cost must vanish whenever the common scale is nonzero (so the ratio is defined).
proof idea
One-line wrapper. Unfold the definition of domain cost (J applied to the ratio of the two arguments). Rewrite $r/r=1$ by the nonzero hypothesis. Finish with the upstream lemma $J(1)=0$.
why it matters
Sanity check inside the FinalModule_1395 structural certificate: domain cost behaves as a true defect (zero when the two scales agree). Sibling declarations in the same module (canonical threshold positivity, MilestoneCert) package the broader domain-coverage milestone; no external dependents are recorded yet.
In the forcing chain this sits under T5 J-uniqueness: the forced cost is calibrated so the self-similar unit is the unique zero. Without diagonal vanishing, later threshold and coverage certificates would not be interpretable as defect bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.