The band-parity sum of a quartic character: two laws modulo four, formalized in Lean

For a prime p ≡ 5 (mod 8), let χ be the quartic character with χ(2) = i, and weight its half-range sum by the parity of ⌊n²/p⌋. The result is a Gaussian integer 𝒞(p) = f + ie. We prove f ≡ (p−1)/4 and e ≡ κ (mod 4), where κ = Σ_{0 5, together with the coset parities of the quartic Bernoulli number B_{1,χ} = k + it, it gives κ ≡ (p−1)/4 + k + t (mod 4). Every numbered result of Sections 3 to 7 is formally verified in Lean 4 with Mathlib. The Lean development is archived at doi:10.5281/zenodo.23673068.