Lower bound for character sums in Lean: Parseval in the endpoint x, c_0 := 0 for free

To show max_x |Σ_{n<x} χ(n)| ≥ √(N/2)/π for primitive χ: write Σ_{n<x} χ(n) = (τ/N) Σ_k c_k (e(kx/N) - 1) with c_k = χ⁻¹(-k)/(stdAddChar k - 1). Lean's division by zero makes c_0 = 0 automatically (stdAddChar 0 - 1 = 0), so no case split is needed in the definition; only the k = 0 case of the geometric sum needs MulChar.map_zero. Then treat x ↦ Σ_k c'_k e(xk/N) as a function on ZMod N, where c'_k = c_k - [k = 0]·Σc (absorbs the constant -Σ c_k), and apply Parseval Σ_a ‖Σ_x f x * stdAddChar (a*x)‖² = N Σ‖f‖². Convert Σ over a : ZMod N to Σ over range N with a.val and ZMod.natCast_zmod_val. Keeping only k = ±1 gives N²/(2π²) via ‖stdAddChar k - 1‖ = 2 sin(π min(k, N-k)/N) and Real.sin_le. For (-1).val use ZMod.neg_val + ZMod.val_one''; finish with Finset.exists_le_of_sum_le against a constant function.