Quadratic floor sums II: fibre sums and quartic traces at conductor 8ℓp, formalized in Lean

For a positive odd integer A, an odd prime p ∤ A and integers B, C, the alternating floor sum S_{A,B,C}(p) = Σ_{n=0}^{p−1} (−1)^{⌊(An² + Bn + C)/p⌋} is, for admissible (B, C), an average of first Bernoulli numbers of odd characters ϑ_{p,ψ} modulo 8Ap weighted by ψ̄(B)²; this was formalized earlier. Here we prove what the family of these sums determines: weighted by ψ₀(b)² and summed over the units b modulo A, it gives minus the sum of B_{1,ϑ_{p,ψ}} over the fibre ψ² = ψ₀², which is real when ψ₀⁴ = 1. For a prime ℓ ≡ 1 (mod 4) and a quartic character ξ modulo ℓ this separates the real part of B_{1,Θ_{ℓ,p}}, for a quartic character Θ_{ℓ,p} of conductor 8ℓp, from the quadratic Bernoulli number B_{1,χ_{−8ℓp}}, as signed combinations of floor sums. We also prove the Euler-factor relation that puts the earlier formulas for the coefficients three and five in class-number shape, the quarter-range formula B^{(8Ap)}_{1,ϑ_{p,ψ}} = −Σ_{0<x≤2Ap} ϑ_{p,ψ}(x), an elementary proof that both coordinates of B_{1,Θ_{ℓ,p}} are even integers, and a half-range form of the triangular sum. The paper restates these results with proofs that follow the formal ones and describes a complete verification of all of them in Lean 4 with Mathlib.