domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain arguments carry zero recognition cost: the diagonal of domain cost vanishes. Anyone normalizing eight-tick comparisons or J-cost ratios would cite this identity. The proof is a one-line unfold-and-cancel that reduces to the known root J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of $r$ against itself is zero. Equivalently, feeding the self-ratio $r/r$ into the Recognition cost $J$ yields $J(1)=0$.
background
Recognition Science measures mismatch by the cost $J(x)=\frac{x+x^{-1}}{2}-1$, also written $\frac{(x-1)^2}{2x}$ for $x>0$. By construction $J(1)=0$, and T5 forces this $J$ as the unique symmetric cost obeying the Recognition Composition Law.
This module packages eight-tick applications that all stem from $2^D=8$ with $D=3$: octave notes, color/flavor counting, the SU(3) adjoint, and related eights. Domain cost compares two real scales by sending their ratio into $J$. The upstream lemma records the unit root: $J(1)=0$.
proof idea
One-line wrapper. Unfold the definition of domain cost to expose $J(r/r)$. Rewrite the self-division to $1$ via the hypothesis $r\neq 0$. Finish by the upstream unit lemma $J(1)=0$.
why it matters
Fixes the diagonal of domain cost at zero, so identical domain values incur no recognition penalty. That is bookkeeping hygiene for the eight-tick application suite (musical octave, eight gluons, eightfold way, and the other $2^3$ counts listed in the module header), all of which rest on T7's eight-tick octave and T8's $D=3$.
No downstream dependents appear in the current graph; the lemma feeds the structural certificate of the v2 module rather than a named parent theorem. It sits under the T5 J-uniqueness landmark: once $J$ is forced, its unit root is free and must be available on every self-comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.