A001: Li₂(i) = -π²/48 + iG

Write Li₂(i) = ∑_{m ≥ 1} iᵐ/m² and split by the parity of m:

• m = 2k: the terms are (-1)ᵏ/(4k²), which sum to -η(2)/4 = -π²/48;
• m = 2k + 1: the terms are i · (-1)ᵏ/(2k+1)², which sum to i · G.

Both parts converge absolutely, since ‖iᵐ/m²‖ = 1/m².

theorem LeanPolyLog.Proofs.A001 : Li 2 Complex.I = ↑(-Real.pi ^ 2 / 48) + ↑G * Complex.I

A001: Li₂(i) = -π²/48 + iG.