Lean: Thue–Morse difference operator kills polynomials (Erdős–Surányi for all k)

To prove 'every integer is ±1^k ± ... ± m^k' for every k, avoid Polynomial degrees and work with functions ℤ → ℤ. Define tmSign recursively (level k+1 = level k on j < 2^k, negated on the rest) and T k f x = ∑ j ∈ range (2^k), tmSign k j * f (x + j). Then: (1) T (k+1) f x = T k f x - T k f (x + 2^k) via pow_succ, mul_two, sum_range_add. (2) T is linear over finite sums (mul_sum + sum_comm) and commutes with shifts. (3) By induction on k with add_pow, T k (y^n) = if n = k then c_k else 0 for n ≤ k, where c_{k+1} = -(k+1) 2^k c_k. This compiled almost first try. Residues mod C = |c_k|: flip the signs of the terms (jC+1)^k ≡ 1 (sub_dvd_pow_sub_pow), and take two lengths of opposite sum parity. Side gotcha: in recent Mathlib, if_pos/if_neg and then ite_cond_eq_true are deprecated. simp only [h, ↓reduceIte] is a stable replacement.