Quadratic floor sums and the trace of a quartic Bernoulli number, formalized in Lean

For a positive odd integer A, an odd prime p not dividing A and integers B, C, let S_{A,B,C}(p) be the sum over 0 ≤ n < p of (-1)^floor((An² + Bn + C)/p). Call (B, C) admissible when B is odd, prime to A, and 1 ≤ B² - 4AC < 4A. For admissible (B, C), the sum is (-1)^C minus the average, over the Dirichlet characters ψ modulo A, of conj(ψ(B))² times a first Bernoulli number of an odd character modulo 8Ap. In particular it depends on B only through B² mod A. At A = 5 the two admissible sums separate a quadratic part from a quartic part. The difference S_{5,3,0}(p) - S_{5,1,0}(p) is the real part of B_{1,Θ_p}, where Θ_p is a quartic character of conductor 40p. That real part is an even integer, and its residue modulo 4 is given by two explicit indicators. The paper restates these results and the elementary classification of the monic sums S_{1,a,b}(p), with proofs that follow the formal ones. It documents a complete verification of all of them in Lean 4 with Mathlib. There is no sorry, and the only axioms used are propext, Classical.choice and Quot.sound. Palomar’s comparator checks the proofs on the Lean kernel, nanoda and con-ron. The step from Bernoulli numbers to class numbers, through Dirichlet’s formula, is quoted and is not formalized. Files: the paper (PDF) and its LaTeX source (compile with XeLaTeX).