Dedekind's congruence modulo 8 for 12k s(h,k)

Let $h$ and $k$ be natural numbers, with $k$ odd and $h$ coprime to $k$. Here the Dedekind sum $s(h,k)$ is the rational number $\sum_{r=0}^{k-1} \big(\!\big(\tfrac{r}{k}\big)\!\big)\,\big(\!\big(\tfrac{hr}{k}\big)\!\big)$, where the sawtooth function $\big(\!\big(x\big)\!\big)$ is defined to be $0$ when the fractional part of $x$ vanishes and $\{x\} - \tfrac12$ otherwise; the arguments $r/k$ and $hr/k$ are formed in $\mathbb{Q}$ with $h$ viewed as an integer. The assertion is that there exists an integer $t$ with

as an identity in $\mathbb{Q}$, where $\left(\frac{h}{k}\right)$ is the Jacobi symbol of $h$ modulo $k$, an integer cast into $\mathbb{Q}$. Thus $12k\,s(h,k)$ is in particular a rational integer for odd $k$, and it is congruent to $k + 1 - 2\left(\frac{h}{k}\right)$ modulo $8$. Note that oddness of $k$ forces $k \geq 1$, so no separate positivity hypothesis appears.

This is Dedekind's classical congruence linking Dedekind sums to the Jacobi symbol, the source of the quadratic-residue information carried by the Rademacher phase. It is used in the proof of ModularCurve.sharpUnitNecessary_of_mod_oneTwenty_eq_one_or_fortyNine, where a witness at prime level congruent to $1$ modulo $8$ must be a quadratic residue.