Square-difference recurrence for finite colourings ($\varphi (a)=\varphi (a+b^2),a,b>0$)

Every finite colouring of the positive integers contains a pair with nonzero square difference. One proof takes limits of the colour autocorrelations and represents the resulting positive-definite sequence by a positive spectral measure. Its atom at zero has mass at least the sum of squared colour densities. Averaging along squares kills irrational frequencies; a common multiple makes finitely many rational atomic frequencies equal to one. The remaining rational atomic mass can be made arbitrarily small, leaving a positive average correlation.