For distinct (i,j),(I,J) in [0,q)^2, their frequencies differ; give a nonzero quadratic norm and rational lower bound >=1/(3q) on the absolute gap.
Method: native-order. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.