A congruence modulo 16 for sums of Dedekind sums over subgroups of odd order

Let k >= 3 and let H be a subgroup of odd order n of (Z/kZ)^x. We prove that 12k times the sum of the Dedekind sums s(h,k) over h in H is congruent to n(k-1)(k-2) modulo 16, and that the modulus 16 is best possible. The proof is elementary: Meyer's formula expresses 12k s(h,k) through the number of inversions of the permutation x -> hx of {1, ..., k-1}, every element of H is a square in H, so each such permutation is even, and inverse elements give the same number of inversions. For a prime p > 3 this yields 2S(H,p) = n(p-1)/2 modulo 8, a refinement of Louboutin's theorem that 2S(H,p) is an integer of the parity of (p-1)/2; equivalently, his quantity N(H,p) = 12S(H,p) - p, which governs the mean square of L(1,chi) over the odd characters trivial on H, satisfies N(H,p) = 3n(p-1) - p modulo 48. Our proof of the integrality of 2S(H,p) is also elementary. As an application, the lattice that the congruence imposes on N(H,p) accounts, under a probabilistic model, for the size of the excess over 1/2 in Louboutin's published data on his Conjecture 3(ii). Theorems 1.1 and 1.2, the optimality of the modulus, and all lemmas of Sections 2 to 4 have been formally verified in Lean 4 with Mathlib.