Dedekind-sum witness for levels ℓ≡ 7(mod 12)

For every natural number $j$, write $\ell = 12j+7$, $a = 3j+2$ and $d = 4$. Here $s(h,k) = \sum_{r=0}^{k-1}\big(\!\!\big(\tfrac{r}{k}\big)\!\!\big)\big(\!\!\big(\tfrac{hr}{k}\big)\!\!\big)$ is dedekindSum, built from the sawtooth $\big(\!\!\big(x\big)\!\!\big)$ which is $0$ when the fractional part of $x$ vanishes and $\{x\} - \tfrac12$ otherwise. The assertion is a conjunction of two statements about rationals and naturals. First, the identity

where $\ell-1$ is formed by truncated subtraction in $\mathbb{N}$, i.e. equals $12j+6$, and the right-hand factor is the image of the integer $-(j+1)$ in $\mathbb{Q}$. Second, the natural numbers $|-(j+1)| = j+1$ and $(\ell-1)/\gcd(\ell-1,12)$, the quotient taken in $\mathbb{N}$, are coprime. Since $\gcd(12j+6,12) = 6$, the two clauses say concretely that the left-hand side equals $-6(j+1)$ and that $j+1$ is coprime to $2j+1$.

The bracketed expression is the difference of values of Rademacher's $\Phi$-function attached to the eta multiplier system, evaluated at a matrix of determinant one with lower row $(\ell,4)$ and upper left entry $3j+2$; the theorem records its exact value together with the coprimality needed to realise it as a generator. It supplies the numerical witness used by ModularCurve.sharpUnitNecessary_of_mod_twelve_eq_seven for levels congruent to $7$ modulo $12$.