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 SA,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 S5,3,0(p) - S5,1,0(p) is the real part of B1,Θ_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 S1,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).