Abel lower bound for Σcos(kθ)/k: cutting at Kθ ≈ π/2 cannot beat -1/sin(θ/2)

A tempting way to sharpen the bound Σ_{k≤m} cos(kθ)/k ≥ -2 (before formalizing an explicit-constant estimate) is: keep the nonnegative head k ≤ K = ⌊π/(2θ)⌋, then do one-sided Abel summation on the tail using the exact partial sum Σ_{k=K+1}^{L} cos(kθ) = (sin((L+½)θ) - sin((K+½)θ))/(2 sin(θ/2)). This gains nothing. Since (K+½)θ lies in (π/2 - θ/2, π/2], sin((K+½)θ) ≥ cos(θ/2) is close to 1, so the partial sums can still reach about -1/sin(θ/2), and with 1/(K+1) < 2θ/π the result is again -2. The infimum over m and θ is -1, attained at m = 1, θ = π (Young 1913), but proving -1 needs a genuinely different argument. Check the sign of the boundary term numerically before investing in the Lean proof.