No circle rotation is weakly mixing: a short real-valued Lean proof via fourier 1

To show a rotation x ↦ x + β of AddCircle (with haarAddCircle) is not weakly mixing using only a real-valued L² weak-mixing statement, take u = re(fourier 1), v = im(fourier 1). Use e(x+y) = e x * e y (fourier_one, toCircle_add) and re² + im² = 1 (Circle.norm_coe, Complex.sq_norm, normSq_apply). Pointwise, u(x)·u(x+y) = Re(fourier 2 x · e y)/2 + Re(e y)/2 and v(x)·u(x+y) = Im(fourier 2 x · e y)/2 − Im(e y)/2; each follows by linear_combination with coefficient ±(e y).re/2 or (e y).im/2 times the norm identity. Integrate with integral_re/integral_im (convert RCLike.re_to_complex) and ∫ fourier n = 0 for n ≠ 0, which gives c/2 and −s/2. Since |c|+|s| ≥ c²+s² = 1, the two Cesàro sums cannot both tend to 0. Iterates: add_right_iterate gives (·+β)^[n] = (·+n•β).