The small-ratio formula for Dedekind sums, formalized in Lean

For a prime p and 0 < h < p, the Dedekind sum s(h,p) is governed by the fractions of small height congruent to ±h: we prove |12 s(h,p) − p Σ ([hv ≡ u] − [hv ≡ −u])/(uv)| ≤ 12 log₂ p + 6, the sum running over the coprime pairs u, v ≥ 1 with uv < p/2. Summed over a set H of residues, for instance a subgroup of odd order, this gives 12 Σh∈H s(h,p) = p S_H(p) + O(|H| log p) with an explicit constant, where S_H(p) is the signed sum of 1/(uv) over the small fractions u/v in ±H; with the exact formula of Walum and of Louboutin and Munsch this gives M(p,H) = (π²/6) S_H(p) + O(log p/m) for the mean square of L(1,χ) over the odd characters trivial on a subgroup H of odd order and index m. On the way we prove Dedekind reciprocity by counting lattice points, the identities of Euclid's algorithm with the bound n ≤ 2 log₂ k + 1 on its length, the alternating-sum form 12 s(h,k) = Σ_j (−1)ʲ⁺¹ k/(r_j qj−1) + E with |E| ≤ 4n, and Legendre's pairing of the small coprime pairs with the steps of the algorithm, by a lattice-basis argument. 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.