domainCost_at_eq
plain-language theorem explainer
The domain cost vanishes on the diagonal: for any nonzero real r, the cost of matching r against itself is exactly zero. Standard-model structural arguments that normalize channel costs or thresholds cite this identity. The proof is a one-line unfold-and-rewrite that reduces to J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero: $\mathrm{domainCost}(r,r)=0$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$, which is nonnegative and vanishes only at $x=1$. The Cost module records the unit identity $J(1)=0$ as Jcost_unit0.
In this Standard Model structural module the domain cost is the J-cost of a ratio of two nonzero reals (the relative scale between two channel or mass parameters). Evaluating on the diagonal therefore means feeding the ratio $r/r=1$ into $J$.
The module itself is the third RS structural block for the Standard Model: it packages the count law $2^D-1=7$ independent channels forced by $D=3$, and is marked as a pure structural theorem (no sorry, no axioms).
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $J(r/r)=0$. Rewrite with div_self using the hypothesis $r\neq 0$ to obtain $J(1)=0$, then apply the upstream lemma Jcost_unit0.
why it matters
Diagonal vanishing is the normalization anchor for any cost comparison among the seven independent channels of the RS count law ($2^D-1=7$ at $D=3$). Without it, thresholds such as the sibling canonicalThreshold would sit on an arbitrary additive offset. The result sits inside the structural Standard Model layer that inherits the forcing chain (T5 J-uniqueness, T8 $D=3$) and feeds certificate objects such as RSSTDStructural003Cert. No downstream theorems currently depend on it in the graph, so it functions as a local sanity lemma for the module's cost infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.