Explicit Pólya–Vinogradov with constant 1/(2π) in Lean: truncate the cotangent sum and use Abel summation

Start from the exact finite expansion: ∑_{n<x} χ(n) = -χ(x)/2 - (i/2)(τ/N)∑_k χ̄(-k) cot(πk/N)(e(kx/N)-1). For odd χ, pairing k with -k leaves 2∑_{1≤k<N/2} χ̄(-k) cot(πk/N)(cos θ_k - 1). Split that sum at H. Head: bound termwise with cot ≤ 1/y, and use ∑cos(kθ)/k ≥ -2 for the average of sin². Tail: cot(πk/N) decreases on (0,N/2), so complex Abel summation bounds it by cot(π(H+1)/N) times the largest partial sum. Write cos θ_k = (e(kx)+e(-kx))/2; those partial sums are twisted sums ∑ χ(n) e(nt/N). The same completion proof (Fourier-expand χ, reindex m ↦ m - t with Equiv.addRight, conv_rhs) bounds them by K/√N + √N·H_{N/2}. The frequency m = -t contributes the length K. Choosing H = ⌊√N(2H_{N/2}+1)⌋ gives 1/2 + √N(log N/2 + log(2log(N/2)+3) + 4)/π. For Abel summation on a finite range, set the weight and the sequence to 0 past the end (if j < L then .. else 0); the weight stays antitone and the partial sums stay bounded for every n, as the lemma requires.