Roth's discrepancy lower bound in Lean with no integrals: Haar functions on a dyadic grid + xor involutions

Roth's orthogonal-function proof (N points in [0,1)^2 ⇒ some box has (count − Nxy)^2 ≥ c log N) goes through in Mathlib almost entirely as finite sums, ~570 lines, most of it compiling first try. Replace the integral by the mean over grid points gc n i = (i + 1/2)/2^(n+1), i < 2^(n+1). A level-r box is a block of high bits of i (i / 2^(n+1-r)) times a block of j (j / 2^(r+1)). Its Rademacher signs are bit n−r of i and bit r of j (Nat.testBit). The key lemma is sum_involution with i ↦ i ^^^ 2^k. If flipping bit k negates the summand, the sum is 0. The lemmas you need: (i ^^^ 2^k)/2^m = i/2^m for k < m (prove by Nat.eq_of_testBit_eq + Nat.testBit_div_two_pow + Nat.testBit_xor + Nat.testBit_two_pow), Nat.xor_lt_two_pow, and testBit_two_pow_self/of_ne for the signs. Orthogonality of levels r < s: flip bit n−s of i. Counting term vs the Haar function of an empty box, for one point p: flip a bit of i if i's x-block differs from p's block, otherwise flip a bit of j. A point outside the block is on the same side of all grid points in it (via ⌊2^e·gc n i⌋₊ = i / 2^m). The box containing p is nonempty, so Haar is 0 there. The area term needs sums over blocks: write ∑_{i<2^(e+m)} f i = ∑_{a<2^e} ∑_{u<2^m} f (a*2^m+u) (induction with sum_range_add), plus Nat.testBit_two_pow_mul_add for the bits. Then apply Finset.sum_mul_sq_le_sq_mul_sq over range M ×ˢ range M. To rewrite only the outer range sum, use rw with the decomposition lemma, then simp_rw a second instance for the inner sum.