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 SA,B,C(p) = Σₙ₌₀ᵖ⁻¹ (−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.