domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain scales incur zero recognition cost: the pairwise domain cost of a real scale against itself is identically zero. Anyone normalizing D=3 combinatorial cost functionals or checking gauge-fixed baselines will cite this. The proof unfolds the cost, cancels the ratio to 1, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: $\mathrm{domainCost}(r,r) = 0$. Equivalently, if the cost is $J(r/r)$ with $J$ the recognition cost, then $J(1) = 0$.
background
The module develops D=3 combinatorics in Recognition Science: three spatial dimensions, three colors, three families, and related ternary structure, all forced from configDim = D = 3 (forcing chain T8). Status is structural: zero sorry, zero axioms.
The recognition cost $J$ (also written Jcost) is the unique nonnegative functional fixed by the Recognition Composition Law, with closed form $J(x) = (x+x^{-1})/2-1 = (x-1)^2/(2x)$ for $x>0$. In particular $J(1)=0$: the unit ratio is a perfect match.
Here domainCost pairs two real scales and scores their mismatch via $J$ of their ratio. The equal-argument case is the baseline that every later nonnegativity or threshold argument must recover.
proof idea
One-line wrapper. Unfold domainCost so the goal is a statement about $J$ of a ratio; rewrite with div_self using $r\neq 0$ to replace $r/r$ by $1$; finish by the upstream lemma Jcost_unit0, which is the direct simplification $J(1)=0$.
why it matters
Zero self-cost is the normalization anchor for domain-scale comparisons inside the D=3 combinatorics layer. Without it, nonnegativity of domainCost and positivity of the canonical threshold would float relative to an arbitrary offset.
It sits under the Foundation forcing picture: T5 uniqueness of $J$, T8 forcing of $D=3$, and the structural claim that ternary counting (colors, families, charge types) inherits a well-normalized cost. No downstream dependents are recorded yet; the lemma is infrastructure for the sibling certificates (domainCost_nonneg, canonicalThreshold_pos, D3CombinatoricsV2Cert).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.