Closed form s(1,k)=(k-1)(k-2)/(12k)

For every natural number $k$, the Dedekind sum with first argument the integer $1$ and second argument $k$ equals $((k-1)(k-2))/(12k)$ in $\mathbb{Q}$, where $k$ is coerced to a rational. Here the Dedekind sum is defined by

the index $r$ running over Finset.range k, and the sawtooth function is $\mathrm{dedekindSaw}(x)=0$ when the fractional part of $x$ vanishes and $\mathrm{dedekindSaw}(x)=\{x\}-\tfrac12$ otherwise. Thus for $h=1$ the assertion is that $\sum_{r=0}^{k-1}\mathrm{dedekindSaw}(r/k)^2=((k-1)(k-2))/(12k)$; the term $r=0$ contributes nothing, and for $1\le r\le k-1$ the summand is $(r/k-\tfrac12)^2$. No hypothesis is imposed on $k$: for $k\ge1$ the denominator $12k$ is nonzero and the identity is the classical closed form, while for $k=0$ both sides are $0$, the left side being an empty sum and the right side using the convention $x/0=0$ in $\mathbb{Q}$.

This is the standard evaluation of the Dedekind sum $s(1,k)$, the base case from which the values of $s(h,k)$ at small $h$ are obtained via reciprocity. It is used in the explicit computations of the Rademacher function $\Phi$ on congruence classes modulo $120$, such as rademacher_phi_level_witness_mod_oneTwenty_eq_one and rademacher_phi_level_witness_mod_oneTwenty_eq_fortyNine.