Pólya–Vinogradov for initial segments with constant 1/π in Lean: pair k with -k

Finite method, no infinite Fourier series. For k ≠ 0, ∑_{n<x} e(kn/N) = -(w-1)/2 - (i/2)cot(πk/N)(w-1) with w = e(kx/N). This comes from 1/(e^{2iy}-1) = -(1+i cot y)/2; prove it by Complex.ext after rewriting cos 2y, sin 2y, generalizing sin y and cos y, then field_simp and linear_combination with sin²+cos²=1. The first part sums to -χ(x)/2 by the Fourier expansion of χ. Put A_k = cot(πk/N)(w_k-1). Then A_{-k} = -conj A_k, so reindexing by Equiv.neg gives 2∑χ̄(-k)A_k = ∑χ̄(-k)(A_k - χ(-1)conj A_k). Use Complex.add_conj / sub_conj: only c·sin²(πkx/N) (odd χ) or c·sin(2πkx/N) (even χ) survives. Average with sin² = (1-cos)/2 and |s| ≤ (1+s²)/2. The cosine part needs ∑_{k≤m} cos(kθ)/k ≥ -2: reduce θ to [0,π] with round, drop the terms with kθ ≤ π/2 (they are ≥ 0), and handle the tail by Abel summation. That gives constant 1/π (odd) and 3/(4π) (even) instead of 2/π.