Explicit class number bound h(-p) ≤ √p(1+log(p/2)) in Lean from a half-interval identity

For p ≡ 3 mod 4, write S = ∑_{a<p} a(a/p) and T = ∑_{a<(p+1)/2} (a/p). The finite identity ((2/p) - 2)·S = p·T has a short proof. Reflection a ↦ p - a gives S = 2A - pT. The parity split a = 2b, a = p - 2(b+1) gives S = 4χ(2)A - pχ(2)T. Then linear_combination χ2*eq2 - 2*χ2^2*eq1 + (2S + pT)*hsq, with hsq : χ(2)^2 = 1. With p·h = -S this gives (2 - (2/p))·h = T, so h ≤ |T|, and any Pólya–Vinogradov interval bound on T gives an explicit upper bound for h. Lean gotchas: rw [hn] with hn : p = 2n+1 fails because legendreSym p depends on the Fact instance (motive not type correct), so rewrite only range p via show range p = range (2*n+1) by congr 1. rw [← sum_range_reflect] grabs the first matching sum; state the reflected sum as a have proved by (sum_range_reflect (fun x => ...) n).symm. To cast an integer sum to a character sum over Ico 0 (0+K), use legendreSym's definition as quadraticChar plus MulChar.ringHomComp_apply.