domainCost_at_eq
plain-language theorem explainer
Equal nonzero scales incur zero domain cost: the cost of the pair (r,r) vanishes for every r≠0. Cited by anyone normalizing the eight-tick completeness cost or checking that matched scales sit at the J-minimum. Proof is a one-line unfold-and-rewrite to J(1)=0.
Claim. For every real $r\neq 0$, the domain cost of equal arguments is zero: evaluating the cost on the pair $(r,r)$ yields $0$.
background
Recognition Science measures scale mismatch by the unique cost $J$ fixed by the composition law, with closed form $J(x)=(x+x^{-1})/2-1$ (equivalently a squared ratio). The unit root is $J(1)=0$. In this module the domain cost of two real scales is that $J$ applied to their ratio, so equal nonzero arguments reduce to the unit case.
The surrounding development is eight-tick completeness: the period-8 lattice covers all $2^D=8$ binary states exactly once per cycle, and no shorter period does. Status is structural (no sorry, no axioms). The lemma that $J(1)=0$ is the sole upstream fact used here.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J$ of the ratio $r/r$. Rewrite that ratio to $1$ by division-by-self under the hypothesis $r\neq 0$. Finish by the upstream unit lemma $J(1)=0$.
why it matters
Gives the diagonal normalization of the cost used in the eight-tick completeness certificate: matched scales sit at zero cost, so the functional only penalizes genuine mismatch. Sits with the sibling nonnegativity and canonical-threshold facts that underwrite the completeness claim. Framework landmark is T7 (eight-tick octave, period $2^3$), the minimum period that covers all binary states once. No downstream dependents are recorded yet; the result is local scaffolding for the structural completeness theorem rather than a bridge into later physics layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.