Dedekind's reciprocity law for s(h,k)+s(k,h)

Let $h$ and $k$ be natural numbers with $h>0$, $k>0$ and $\gcd(h,k)=1$. Here dedekindSaw is the sawtooth function on $\mathbb{Q}$, defined to be $0$ when the fractional part $\operatorname{fract}(x)$ vanishes and $\operatorname{fract}(x)-\tfrac12$ otherwise, and for an integer $a$ and a natural number $m$ the Dedekind sum dedekindSum a m is the finite rational sum $\sum_{r=0}^{m-1} \mathrm{saw}(r/m)\,\mathrm{saw}(a r/m)$, the summands being computed in $\mathbb{Q}$. The assertion is the equality of rational numbers

where $s(h,k)$ is dedekindSum applied to the image of $h$ in $\mathbb{Z}$ and to the modulus $k$, and $s(k,h)$ is dedekindSum applied to the image of $k$ in $\mathbb{Z}$ and to the modulus $h$; the right-hand side is formed from the rational casts of $h$ and $k$, as $((h/k)+(k/h)+1/(hk))/12-1/4$. Note that in this formulation both arguments of each Dedekind sum are positive integers, the first being taken modulo nothing and simply cast.

This is Dedekind's reciprocity law for the Dedekind sums $s(h,k)$, the elementary counterpart of the transformation behaviour of $\log\eta$ under $\mathrm{SL}_2(\mathbb{Z})$. It is the basic arithmetic input for the congruence and level computations for the Rademacher function $\Phi$ in this development, being cited by the congruence of $s(h,k)$ with a Jacobi symbol modulo $8$ and by the determinations of $\Phi$ modulo $120$.