Let \(t \in S_p\). Unfolding the definition of \(S_p\) as a filter, the first component of the predicate \(\operatorname {SpPred}(p)\) requires precisely that \(t.1^2 + t.2.1^2 + t.2.2.1^2 + t.2.2.2^2 = p\), which is the membership condition for \(\widetilde{S}_p\). Hence \(t \in \widetilde{S}_p\).

By \(\operatorname {Sp_card}\), we have \(|S_p| = p+1 \geq 2 {\gt} 0\), so \(S_p\) is nonempty. Rewriting with the cardinality: if \(S_p\) were empty then \(|S_p| = 0 \neq p+1\) (since \(p \geq 2\)), a contradiction by integer arithmetic. Obtaining \(t \in S_p\), by \(\operatorname {Sp_subset_SpTilde}\), \(t \in \widetilde{S}_p\), so \(\widetilde{S}_p\) is nonempty.

Assume for contradiction that \(S_p = \emptyset \). Then \(|S_p| = 0\). But by \(\operatorname {Sp_card}\), \(|S_p| = p+1\). Since \(p \geq 2\), we have \(p+1 \geq 3 {\gt} 0\), contradicting \(|S_p| = 0\) by integer arithmetic.

Unfolding the definition of \(M(a,b,c,d)\) and computing the \(2\times 2\) determinant using \(\det \begin{pmatrix} p & q \\ r & s \end{pmatrix} = ps - qr\), the result follows by a linear combination using the hypothesis \(x^2 + y^2 + 1 = 0\): specifically, \(\det M = \iota (a)^2 + \iota (b)^2 + \iota (c)^2 + \iota (d)^2\) after simplification via \(-(\iota (b)^2 + \iota (d)^2)(x^2 + y^2 + 1) = 0\).

By lpsMatrixVal_det, it suffices to show \(\iota (a)^2 + \iota (b)^2 + \iota (c)^2 + \iota (d)^2 \neq 0\) in \(\mathbb {Z}/q\mathbb {Z}\). Since \(t \in \widetilde{S}_p\), we have \(a^2 + b^2 + c^2 + d^2 = p\) in \(\mathbb {Z}\). Applying \(\iota : \mathbb {Z} \to \mathbb {Z}/q\mathbb {Z}\) and using \(\operatorname {push_cast}\), the sum equals \(\iota (p) = (p : \mathbb {Z}/q\mathbb {Z})\). We must show \((p : \mathbb {Z}/q\mathbb {Z}) \neq 0\), i.e. \(q \nmid p\). Since \(p\) and \(q\) are distinct primes, by primality of \(p\): \(q \mid p\) implies \(q = 1\) or \(q = p\), the former contradicting \(q\) prime and the latter contradicting \(p \neq q\).

Since \(t \in \widetilde{S}_p\), we have \(a^2 + b^2 + c^2 + d^2 = p\). For \(\bar{t} = (a,-b,-c,-d)\), we compute \(a^2 + (-b)^2 + (-c)^2 + (-d)^2 = a^2 + b^2 + c^2 + d^2 = p\) by the fact that squaring negates signs, which follows by a nonlinear arithmetic argument using \(b^2 \geq 0\).

We check equality entry by entry using extensionality. For each of the four entries \((i,j) \in \{ 0,1\} ^2\), unfolding the definitions of \(M(\bar{t})\) (with \((a,-b,-c,-d)\)) and of \(\operatorname {adj}(M(t))\) (using the \(2\times 2\) adjugate formula \(\operatorname {adj}\begin{pmatrix} p & q \\ r & s \end{pmatrix} = \begin{pmatrix} s & -q \\ -r & p \end{pmatrix}\)) and simplifying by ring arithmetic confirms equality.

When \(a = 0\), entry-by-entry verification using the definitions of \(M(\bar{t}) = M(0,-b,-c,-d)\) and \(-M(t) = -M(0,b,c,d)\) shows equality via ring arithmetic.

We unfold the membership condition for \(S_p\) for both \(t\) and \(\bar{t} = (a,-b,-c,-d)\), obtaining bounds and the predicate \(\operatorname {SpPred}\). The bounds \(-p \leq \pm b, \pm c, \pm d \leq p\) are preserved by negation. For the normalization condition: in both the \(p \equiv 1 \pmod{4}\) and \(p \equiv 3 \pmod{4}\) cases, since \(a {\gt} 0\) is unchanged and is the first coordinate, the condition \(a {\gt} 0\) (and \(a\) odd if \(p \equiv 1\)) is preserved, and \(\operatorname {firstNonzeroPositive}(\bar{t}) = \operatorname {Or.inl}(a {\gt} 0)\) holds.

Suppose for contradiction that \(M = \operatorname {tupleToGL}(t) \in Z(\operatorname {GL}(2, \mathbb {Z}/q\mathbb {Z}))\), i.e. \(M\) commutes with every element. We construct the elementary matrices \(E_{12} = \begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}\) and \(E_{21} = \begin{pmatrix} 1 & 0 \\ 1 & 1 \end{pmatrix}\) as \(\operatorname {GL}\) elements (their determinants equal \(1 \neq 0\)). From commutativity \(E_{12} M_{\text{mat}} = M_{\text{mat}} E_{12}\): entry \((1,0)\) gives \(M_{10} = 0\) and entries \((0,0),(1,1)\) give \(M_{00} = M_{11}\). From \(E_{21} M_{\text{mat}} = M_{\text{mat}} E_{21}\): entry \((0,1)\) gives \(M_{01} = 0\).

Translating to the LPS matrix entries with \(\iota (b) = \bar{b}\), \(\iota (c) = \bar{c}\), \(\iota (d) = \bar{d}\): the equations yield \(\bar{c} = 0\) (from \(2\bar{c} = 0\) and \(2 \neq 0\) in \(\mathbb {Z}/q\mathbb {Z}\) since \(q\) is odd), \(\bar{d}x = \bar{b}y\), and \(\bar{b}x + \bar{d}y = 0\).

Since \(x^2 + y^2 = -1\), multiplying: \(\bar{b}(x^2+y^2) = 0\) by a linear combination \(-y(\bar{d}x - \bar{b}y) + x(\bar{b}x + \bar{d}y) = 0\), giving \(-\bar{b} = 0\) so \(\bar{b} = 0\). Similarly \(\bar{d} = 0\) (if \(\bar{d} \neq 0\) then both \(x = 0\) and \(y = 0\) from the equations, but then \(x^2 + y^2 = 0 \neq -1\), contradiction).

Now \(b, c, d\) all have \(\mathbb {Z}/q\mathbb {Z}\)-images zero, and each satisfies \(b^2 \leq p\) (from \(a^2 + b^2 + c^2 + d^2 = p\)). Since \(q {\gt} 2\sqrt{p}\), the lemma int_eq_zero_of_zmod_eq_zero_of_sq_le implies \(b = c = d = 0\) in \(\mathbb {Z}\). Then \(a^2 = p\), contradicting the fact that no prime is a perfect square (Nat.Prime.not_perfect_square).

It suffices to show \(\pi _{\operatorname {PGL}}(g \cdot g') = 1\) where \(g = \operatorname {tupleToGL}(t)\) and \(g' = \operatorname {tupleToGL}(\bar{t})\). We compute \(g \cdot g'\) using \(g'.{\rm val} = \operatorname {adj}(g.{\rm val})\) (from lpsMatrixVal_negConj): \(g.{\rm val} \cdot g'.{\rm val} = M(t) \cdot \operatorname {adj}(M(t)) = \det (M(t)) \cdot I\). Thus \(g \cdot g'\) is a scalar matrix \(\det (M(t)) \cdot I\). A scalar matrix lies in the center of \(\operatorname {GL}(2, \mathbb {Z}/q\mathbb {Z})\), so it maps to \(1 \in \operatorname {PGL}_2(q)\) via \(\pi _{\operatorname {PGL}} = \operatorname {QuotientGroup.mk’}\).

Let \(g = \operatorname {tupleToGL}(t)\) and \(g' = \operatorname {tupleToGL}(\bar{t})\). We show \(\pi _{\operatorname {PGL}}(g') = \pi _{\operatorname {PGL}}(g)\), equivalently \(g^{\prime -1} g \in Z(\operatorname {GL}(2, \mathbb {Z}/q\mathbb {Z}))\). Since \(a = 0\), by lpsMatrixVal_negConj_zero_fst, \(g'.{\rm val} = -g.{\rm val}\). We compute \((g^{\prime -1} g).{\rm val}\): from \((-g.{\rm val})(g^{\prime -1}.{\rm val} \cdot g.{\rm val}) = g.{\rm val}\) (using \(g' \cdot g^{\prime -1} = 1\)), it follows that \(g.{\rm val} \cdot (g^{\prime -1}.{\rm val} \cdot g.{\rm val}) = -g.{\rm val}\). Multiplying on the left by \(g^{-1}.{\rm val}\) and using \(g^{-1} \cdot g = 1\), we get \((g^{\prime -1}g).{\rm val} = -(1)\). Since \(-I\) commutes with every matrix, \(g^{\prime -1}g \in Z(\operatorname {GL}(2, \mathbb {Z}/q\mathbb {Z}))\).

Unfolding the filter condition for \(S_p\): in the case \(p \equiv 1 \pmod{4}\), the predicate requires \(a {\gt} 0\), so \(a \geq 0\). In the case \(p \equiv 3 \pmod{4}\), the predicate requires \(\operatorname {firstNonzeroPositive}(t)\), which by case analysis gives either \(a {\gt} 0\) (so \(a \geq 0\)), or \(a = 0\) (so \(a \geq 0\)) in all remaining cases.

By the defining property of legendreSqrt via ZMod.isSquare_of_jacobiSym_eq_one.choose_spec, the chosen element \(r\) satisfies \(r \cdot r = (p : \mathbb {Z}/q\mathbb {Z})\), which equals \(r^2\) by definition of squaring.

Suppose \(r = 0\). Then \(r^2 = 0\). But by legendreSqrt_sq, \(r^2 = (p : \mathbb {Z}/q\mathbb {Z})\). So \((p : \mathbb {Z}/q\mathbb {Z}) = 0\), meaning \(q \mid p\). Since \(p, q\) are distinct primes, by primality of \(p\): either \(q = 1\) (contradicting \(q\) prime) or \(q = p\) (contradicting \(p \neq q\)). Contradiction.

By definition, \(\operatorname {tupleToSL}(\bar{t}).{\rm val} = r^{-1} \operatorname {adj}(M(t))\) (using lpsMatrixVal_negConj) and \(\operatorname {tupleToSL}(t).{\rm val} = r^{-1} M(t)\). Their product is \(r^{-1} \operatorname {adj}(M(t)) \cdot r^{-1} M(t) = r^{-1} r^{-1} (\operatorname {adj}(M(t)) \cdot M(t)) = r^{-2} \det (M(t)) \cdot I\). By legendreSqrt_sq, \(\det M(t) = r^2\). So the product equals \(r^{-2} r^2 \cdot I = I\). Setting \(r^{-1} \cdot r^{-1} \cdot r^2 = (r^{-1} \cdot r^{-1} \cdot r) \cdot r = r^{-1} \cdot 1 \cdot r = 1\) by repeated use of \(r^{-1} \cdot r = 1\).

Let \(\operatorname {nc} = \operatorname {tupleToSL}(\bar{t})\) and \(\operatorname {tt} = \operatorname {tupleToSL}(t)\). We show \(\operatorname {nc}^{-1} \cdot \operatorname {tt} \in Z(\operatorname {SL}(2, \mathbb {Z}/q\mathbb {Z}))\).

By tupleToSL_negConj_mul_self_eq_one, \(\operatorname {nc} \cdot \operatorname {tt} = 1\), so \(\operatorname {nc}^{-1} = \operatorname {tt}\), hence \(\operatorname {nc}^{-1} \cdot \operatorname {tt} = \operatorname {tt}^2\).

We compute \((\operatorname {tt}^2).{\rm val}\): since \(\operatorname {tt}.{\rm val} = r^{-1} M(t)\), we get \((\operatorname {tt}^2).{\rm val} = r^{-2} M(t)^2\). Since \(a = 0\), \(\operatorname {adj}(M(t)) = -M(t)\) by lpsMatrixVal_negConj_zero_fst, so \(M(t)^2 = -\det (M(t)) \cdot I\). Using \(\det (M(t)) = r^2\): \((\operatorname {tt}^2).{\rm val} = r^{-2} \cdot (-r^2 \cdot I) = -I\).

Since \(-I\) commutes with every matrix (as \((-I)g = g(-I)\) for all \(g\)), \(\operatorname {tt}^2 \in Z(\operatorname {SL}(2, \mathbb {Z}/q\mathbb {Z}))\), completing the proof.

By cayleyGraph_isRegularOfDegree, the Cayley graph \(\operatorname {cayleyGraph}(S)\) is \(|S|\)-regular for any symmetric generating set \(S\). Applying this to \(S = S_{p,q}^{\operatorname {PGL}}\) and rewriting with lpsGenSetPGL_card (which gives \(|S_{p,q}^{\operatorname {PGL}}| = p+1\)), we obtain the \((p+1)\)-regularity.

By cayleyGraph_isRegularOfDegree, applying it to \(S = S_{p,q}^{\operatorname {PSL}}\) and rewriting with lpsGenSetPSL_card (giving \(|S_{p,q}^{\operatorname {PSL}}| = p+1\)) yields \((p+1)\)-regularity.