Definition 21: LPS Expander Graphs

Main Results

• PGL2: The projective general linear group PGL(2, q).
• PSL2: The projective special linear group PSL(2, q).
• SpTilde: The set S̃_p = {(a,b,c,d) ∈ ℤ⁴ | a² + b² + c² + d² = p}.
• Sp: The normalized subset S_p ⊆ S̃_p with |S_p| = p + 1.
• lpsMatrix: The matrix M(a,b,c,d) in GL(2, 𝔽_q).
• lpsGenSetPGL: The generating set S_{p,q} ⊆ PGL(2,q).
• lpsGenSetPSL: The generating set S_{p,q} ⊆ PSL(2,q).
• lpsGraphPGL: The LPS Cayley graph on PGL(2,q).
• lpsGraphPSL: The LPS Cayley graph on PSL(2,q).

Group definitions

@[reducible, inline]

abbrev LPS.PGL2 (q : ℕ) : Type

The projective general linear group PGL(2, q) = GL(2, 𝔽_q) / center(GL(2, 𝔽_q)). Defined as the quotient of GL(2, ZMod q) by its center.

Equations

• LPS.PGL2 q = (GL (Fin 2) (ZMod q) ⧸ Subgroup.center (GL (Fin 2) (ZMod q)))

@[reducible, inline]

abbrev LPS.PSL2 (q : ℕ) : Type

The projective special linear group PSL(2, q) = SL(2, 𝔽_q) / center(SL(2, 𝔽_q)).

Equations

• LPS.PSL2 q = (Matrix.SpecialLinearGroup (Fin 2) (ZMod q) ⧸ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) (ZMod q)))

instance LPS.PGL2.instGroup (q : ℕ) : Group (PGL2 q)

Equations

• LPS.PGL2.instGroup q = inferInstance

instance LPS.PSL2.instGroup (q : ℕ) : Group (PSL2 q)

Equations

• LPS.PSL2.instGroup q = inferInstance

instance LPS.PGL2.instFintype (q : ℕ) [Fact (Nat.Prime q)] : Fintype (PGL2 q)

Equations

• LPS.PGL2.instFintype q = inferInstance

instance LPS.PSL2.instDecidableEqSL (q : ℕ) [Fact (Nat.Prime q)] : DecidableEq (Matrix.SpecialLinearGroup (Fin 2) (ZMod q))

Equations

• LPS.PSL2.instDecidableEqSL q a b = decidable_of_iff (↑a = ↑b) ⋯

instance LPS.PSL2.instDecidableCommMul (q : ℕ) [Fact (Nat.Prime q)] (z : Matrix.SpecialLinearGroup (Fin 2) (ZMod q)) : Decidable (∀ (g : Matrix.SpecialLinearGroup (Fin 2) (ZMod q)), g * z = z * g)

Equations

• LPS.PSL2.instDecidableCommMul q z = Fintype.decidableForallFintype

instance LPS.PSL2.instDecidablePredCenter (q : ℕ) [Fact (Nat.Prime q)] : DecidablePred fun (x : Matrix.SpecialLinearGroup (Fin 2) (ZMod q)) => x ∈ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) (ZMod q))

Equations

• LPS.PSL2.instDecidablePredCenter q z = Subgroup.decidableMemCenter z

instance LPS.PSL2.instFintype (q : ℕ) [Fact (Nat.Prime q)] : Fintype (PSL2 q)

Equations

• LPS.PSL2.instFintype q = QuotientGroup.fintype (Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) (ZMod q)))

instance LPS.PGL2.instDecidableEq (q : ℕ) [Fact (Nat.Prime q)] : DecidableEq (PGL2 q)

Equations

• LPS.PGL2.instDecidableEq q = inferInstance

instance LPS.PSL2.instDecidableLeftRel (q : ℕ) [Fact (Nat.Prime q)] : DecidableRel ⇑(QuotientGroup.leftRel (Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) (ZMod q))))

Equations

• LPS.PSL2.instDecidableLeftRel q a b = ⋯.mpr (LPS.PSL2.instDecidablePredCenter q (a⁻¹ * b))

instance LPS.PSL2.instDecidableEq (q : ℕ) [Fact (Nat.Prime q)] : DecidableEq (PSL2 q)

Equations

• LPS.PSL2.instDecidableEq q = Quotient.decidableEq

The set S̃_p and the normalized subset S_p

def LPS.SpTilde (p : ℕ) : Set (ℤ × ℤ × ℤ × ℤ)

The set S̃_p = {(a,b,c,d) ∈ ℤ⁴ | a² + b² + c² + d² = p} of integer 4-tuples whose sum of squares equals p.

Equations

• LPS.SpTilde p = {t : ℤ × ℤ × ℤ × ℤ | t.1 ^ 2 + t.2.1 ^ 2 + t.2.2.1 ^ 2 + t.2.2.2 ^ 2 = ↑p}

instance LPS.instDecidablePredProdIntMemSetSpTilde (p : ℕ) : DecidablePred fun (x : ℤ × ℤ × ℤ × ℤ) => x ∈ SpTilde p

Equations

• LPS.instDecidablePredProdIntMemSetSpTilde p t = inferInstanceAs (Decidable (t.1 ^ 2 + t.2.1 ^ 2 + t.2.2.1 ^ 2 + t.2.2.2 ^ 2 = ↑p))

def LPS.firstNonzeroPositive (t : ℤ × ℤ × ℤ × ℤ) : Prop

Predicate for the first nonzero element being positive (for p ≡ 3 mod 4 case).

Equations

• LPS.firstNonzeroPositive t = (t.1 > 0 ∨ t.1 = 0 ∧ t.2.1 > 0 ∨ t.1 = 0 ∧ t.2.1 = 0 ∧ t.2.2.1 > 0 ∨ t.1 = 0 ∧ t.2.1 = 0 ∧ t.2.2.1 = 0 ∧ t.2.2.2 > 0)

instance LPS.instDecidablePredProdIntFirstNonzeroPositive : DecidablePred firstNonzeroPositive

Equations

• LPS.instDecidablePredProdIntFirstNonzeroPositive t = id inferInstance

def LPS.SpPred (p : ℕ) (t : ℤ × ℤ × ℤ × ℤ) : Prop

The normalized subset predicate for S_p. When p ≡ 1 (mod 4): a is positive and odd. When p ≡ 3 (mod 4): a is even and the first nonzero element is positive.

Equations

• LPS.SpPred p t = (t.1 ^ 2 + t.2.1 ^ 2 + t.2.2.1 ^ 2 + t.2.2.2 ^ 2 = ↑p ∧ if p % 4 = 1 then t.1 > 0 ∧ t.1 % 2 = 1 else t.1 % 2 = 0 ∧ LPS.firstNonzeroPositive t)

instance LPS.instDecidablePredProdIntSpPred (p : ℕ) : DecidablePred (SpPred p)

Equations

• LPS.instDecidablePredProdIntSpPred p t = id inferInstance

def LPS.Sp (p : ℕ) [Fact (Nat.Prime p)] (hoddp : p % 2 = 1) : Finset (ℤ × ℤ × ℤ × ℤ)

The normalized subset S_p ⊆ S̃_p. Defined as the set of integer 4-tuples (a,b,c,d) with a² + b² + c² + d² = p satisfying the normalization condition. Each coordinate is bounded by √p ≤ p, so we filter from [-p, p]⁴.

Equations

• LPS.Sp p hoddp = Finset.filter (LPS.SpPred p) (Finset.Icc (-↑p) ↑p ×ˢ Finset.Icc (-↑p) ↑p ×ˢ Finset.Icc (-↑p) ↑p ×ˢ Finset.Icc (-↑p) ↑p)

theorem LPS.Sp_subset_SpTilde (p : ℕ) [Fact (Nat.Prime p)] (hoddp : p % 2 = 1) (t : ℤ × ℤ × ℤ × ℤ) : t ∈ Sp p hoddp → t ∈ SpTilde p

Every element of S_p lies in S̃_p.

axiom LPS.Sp_card (p : ℕ) [Fact (Nat.Prime p)] (hoddp : p % 2 = 1) : (Sp p hoddp).card = p + 1

This follows from Jacobi's four-square theorem: r₄(p) = 8(p+1) for odd prime p, and the normalization conditions select exactly (p+1) representatives. Jacobi's four-square theorem is not available in Mathlib.

Witness lemmas for set non-emptiness

theorem LPS.SpTilde_nonempty_three : (SpTilde 3).Nonempty

Witness: SpTilde p is non-empty for any prime p ≥ 2. For p = 3, the tuple (1, 1, 1, 0) satisfies 1² + 1² + 1² + 0² = 3.

theorem LPS.SpTilde_nonempty (p : ℕ) [Fact (Nat.Prime p)] (hoddp : p % 2 = 1) : (SpTilde p).Nonempty

For any odd prime p, SpTilde p is non-empty (follows from Sp being non-empty and Sp_subset_SpTilde).

theorem LPS.Sp_nonempty (p : ℕ) [Fact (Nat.Prime p)] (hoddp : p % 2 = 1) : (Sp p hoddp).Nonempty

Sp p is non-empty for any odd prime p, since |S_p| = p + 1 ≥ 4 > 0.

Satisfiability witnesses for Sp

theorem LPS.Sp_satisfiable : ∃ (p : ℕ) (_ : Fact (Nat.Prime p)), p % 2 = 1

Witness: Sp premises are satisfiable (p = 3 works).

The matrix M(a,b,c,d) and the LPS generating set

theorem LPS.exists_sum_sq_eq_neg_one (q : ℕ) [Fact (Nat.Prime q)] (hoddq : q % 2 = 1) : ∃ (x : ZMod q) (y : ZMod q), x ^ 2 + y ^ 2 + 1 = 0

The existence of x, y ∈ 𝔽_q with x² + y² + 1 = 0. For an odd prime q, by ZMod.sq_add_sq there exist a, b with a² + b² = -1, i.e. a² + b² + 1 = 0.

def LPS.lpsMatrixVal (q : ℕ) (x y : ZMod q) (t : ℤ × ℤ × ℤ × ℤ) : Matrix (Fin 2) (Fin 2) (ZMod q)

The LPS matrix M(a,b,c,d) as a 2×2 matrix over ZMod q.

Equations

• LPS.lpsMatrixVal q x y t = !![↑t.1 + ↑t.2.1 * x + ↑t.2.2.2 * y, -↑t.2.1 * y + ↑t.2.2.1 + ↑t.2.2.2 * x; -↑t.2.1 * y - ↑t.2.2.1 + ↑t.2.2.2 * x, ↑t.1 - ↑t.2.1 * x - ↑t.2.2.2 * y]

theorem LPS.lpsMatrixVal_det (q : ℕ) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) : (lpsMatrixVal q x y t).det = ↑t.1 ^ 2 + ↑t.2.1 ^ 2 + ↑t.2.2.1 ^ 2 + ↑t.2.2.2 ^ 2

The determinant of M(a,b,c,d) equals ι(a² + b² + c² + d²).

theorem LPS.lpsMatrixVal_det_ne_zero (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) : (lpsMatrixVal q x y t).det ≠ 0

For (a,b,c,d) ∈ S̃_p with p ≠ q (both prime), M(a,b,c,d) is invertible.

def LPS.projPGL (q : ℕ) : GL (Fin 2) (ZMod q) →* PGL2 q

The canonical projection from GL(2, ZMod q) to PGL(2, q).

Equations

• LPS.projPGL q = QuotientGroup.mk' (Subgroup.center (GL (Fin 2) (ZMod q)))

def LPS.projPSL (q : ℕ) : Matrix.SpecialLinearGroup (Fin 2) (ZMod q) →* PSL2 q

The canonical projection from SL(2, ZMod q) to PSL(2, q).

Equations

• LPS.projPSL q = QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) (ZMod q)))

def LPS.matToGL (q : ℕ) [Fact (Nat.Prime q)] (M : Matrix (Fin 2) (Fin 2) (ZMod q)) (hdet : M.det ≠ 0) : GL (Fin 2) (ZMod q)

Lift a matrix with nonzero determinant to GL(2, ZMod q).

Equations

• LPS.matToGL q M hdet = ⋯.unit

def LPS.tupleToGLElement (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) : GL (Fin 2) (ZMod q)

Map a tuple to PGL(2,q) via the LPS matrix, given membership in SpTilde.

Equations

• LPS.tupleToGLElement q p hpq x y hxy t ht = LPS.matToGL q (LPS.lpsMatrixVal q x y t) ⋯

Helper lemmas for generating set properties

theorem LPS.Nat.Prime.not_perfect_square (p : ℕ) (hp : Nat.Prime p) (a : ℤ) : a ^ 2 ≠ ↑p

A prime is not a perfect square.

theorem LPS.int_eq_zero_of_zmod_eq_zero_of_sq_le {q p : ℕ} [Fact (Nat.Prime q)] (hq_gt : ↑q > 2 * √↑p) (n : ℤ) (hn_zmod : ↑n = 0) (hn_sq : n ^ 2 ≤ ↑p) : n = 0

If (n : ZMod q) = 0 and n² ≤ p and q > 2√p, then n = 0.

theorem LPS.sq_le_of_sum_four_sq_eq {a b c d : ℤ} {p : ℕ} (h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑p) : b ^ 2 ≤ ↑p ∧ c ^ 2 ≤ ↑p ∧ d ^ 2 ≤ ↑p

From a² + b² + c² + d² = p, each squared term is at most p.

@[simp]

theorem LPS.matToGL_val (q : ℕ) [Fact (Nat.Prime q)] (M : Matrix (Fin 2) (Fin 2) (ZMod q)) (hdet : M.det ≠ 0) : ↑(matToGL q M hdet) = M

The underlying matrix of matToGL is the input matrix.

@[simp]

theorem LPS.tupleToGLElement_val (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) : ↑(tupleToGLElement q p hpq x y hxy t ht) = lpsMatrixVal q x y t

The underlying matrix of tupleToGLElement is lpsMatrixVal.

theorem LPS.lpsMatrix_not_in_center (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) : tupleToGLElement q p hpq x y hxy t ht ∉ Subgroup.center (GL (Fin 2) (ZMod q))

If M(a,b,c,d) is in the center of GL(2, ZMod q), derive a contradiction.

def LPS.negConj (t : ℤ × ℤ × ℤ × ℤ) : ℤ × ℤ × ℤ × ℤ

The conjugate tuple (a, -b, -c, -d).

Equations

• LPS.negConj t = (t.1, -t.2.1, -t.2.2.1, -t.2.2.2)

theorem LPS.negConj_mem_SpTilde {p : ℕ} {t : ℤ × ℤ × ℤ × ℤ} (ht : t ∈ SpTilde p) : negConj t ∈ SpTilde p

The conjugate tuple is in SpTilde whenever the original is.

theorem LPS.lpsMatrixVal_negConj (q : ℕ) (x y : ZMod q) (t : ℤ × ℤ × ℤ × ℤ) : lpsMatrixVal q x y (negConj t) = (lpsMatrixVal q x y t).adjugate

The LPS matrix of the conjugate tuple is the adjugate of the original.

theorem LPS.lpsMatrixVal_negConj_zero_fst (q : ℕ) (x y : ZMod q) (t : ℤ × ℤ × ℤ × ℤ) (ha : t.1 = 0) : lpsMatrixVal q x y (negConj t) = -lpsMatrixVal q x y t

When a = 0, M(0,-b,-c,-d) = -M(0,b,c,d).

theorem LPS.negConj_mem_Sp_of_fst_pos {p : ℕ} [Fact (Nat.Prime p)] (hoddp : p % 2 = 1) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ Sp p hoddp) (ha_pos : t.1 > 0) : negConj t ∈ Sp p hoddp

Negating b, c, d preserves the Sp predicate when a > 0 (both p ≡ 1 and p ≡ 3 cases).

theorem LPS.projPGL_negConj_eq_inv (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) : (projPGL q) (tupleToGLElement q p hpq x y hxy (negConj t) ⋯) = ((projPGL q) (tupleToGLElement q p hpq x y hxy t ht))⁻¹

The PGL image of tupleToGLElement(negConj t) equals the inverse of tupleToGLElement(t). This follows from adj(M(t)) * M(t) = det(M(t)) • I, and negConj gives the adjugate.

theorem LPS.projPGL_negConj_eq_self_of_fst_zero (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) (ha : t.1 = 0) : (projPGL q) (tupleToGLElement q p hpq x y hxy (negConj t) ⋯) = (projPGL q) (tupleToGLElement q p hpq x y hxy t ht)

In the a=0 case, M(negConj t) = -M(t), so their PGL images coincide.

theorem LPS.Sp_fst_nonneg {p : ℕ} [Fact (Nat.Prime p)] (hoddp : p % 2 = 1) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ Sp p hoddp) : t.1 ≥ 0

For t ∈ Sp, either a > 0 (and negConj t ∈ Sp) or a = 0 (and s⁻¹ = s).

def LPS.lpsGenSetPGL (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : CayleyGraph.SymmGenSet (PGL2 q)

The LPS generating set in PGL(2, q), as a SymmGenSet.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LPS.matToSL (q : ℕ) [Fact (Nat.Prime q)] (M : Matrix (Fin 2) (Fin 2) (ZMod q)) (r : ZMod q) (hr_ne : r ≠ 0) (hr_sq : r ^ 2 = M.det) : Matrix.SpecialLinearGroup (Fin 2) (ZMod q)

Scale a matrix by the inverse of a square root of its determinant to get an SL element.

Equations

• LPS.matToSL q M r hr_ne hr_sq = ⟨r⁻¹ • M, ⋯⟩

noncomputable def LPS.legendreSqrt (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hleg : legendreSym q ↑p = 1) : ZMod q

Get a square root of (p : ZMod q) from the Legendre symbol condition.

Equations

• LPS.legendreSqrt q p hpq hleg = Exists.choose ⋯

theorem LPS.legendreSqrt_sq (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hleg : legendreSym q ↑p = 1) : legendreSqrt q p hpq hleg ^ 2 = ↑↑p

theorem LPS.legendreSqrt_ne_zero (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hleg : legendreSym q ↑p = 1) : legendreSqrt q p hpq hleg ≠ 0

noncomputable def LPS.tupleToSLElement (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hleg : legendreSym q ↑p = 1) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) : Matrix.SpecialLinearGroup (Fin 2) (ZMod q)

Construct an SL element from the LPS matrix using the Legendre symbol square root.

Equations

• LPS.tupleToSLElement q p hpq hleg x y hxy t ht = LPS.matToSL q (LPS.lpsMatrixVal q x y t) (LPS.legendreSqrt q p hpq hleg) ⋯ ⋯

theorem LPS.tupleToSL_negConj_mul_self_eq_one (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hleg : legendreSym q ↑p = 1) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) : tupleToSLElement q p hpq hleg x y hxy (negConj t) ⋯ * tupleToSLElement q p hpq hleg x y hxy t ht = 1

tupleToSLElement(negConj t) * tupleToSLElement(t) = 1 in SL.

theorem LPS.projPSL_negConj_eq_self_of_fst_zero (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddq : q % 2 = 1) (hleg : legendreSym q ↑p = 1) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) (t : ℤ × ℤ × ℤ × ℤ) (ht : t ∈ SpTilde p) (ha : t.1 = 0) : (projPSL q) (tupleToSLElement q p hpq hleg x y hxy (negConj t) ⋯) = (projPSL q) (tupleToSLElement q p hpq hleg x y hxy t ht)

In PSL, projPSL(negConj t) = projPSL(t) when a = 0 (since M(negConj t) = -M(t)).

def LPS.lpsGenSetPSL (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (hleg : legendreSym q ↑p = 1) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : CayleyGraph.SymmGenSet (PSL2 q)

The LPS generating set in PSL(2, q).

Equations

• One or more equations did not get rendered due to their size.

Satisfiability witnesses for generating set axioms

theorem LPS.lpsGenSetPGL_satisfiable : ∃ (q : ℕ) (p : ℕ) (_ : Fact (Nat.Prime q)) (_ : Fact (Nat.Prime p)), p ≠ q ∧ p % 2 = 1 ∧ q % 2 = 1

Witness: lpsGenSetPGL is satisfiable.

theorem LPS.lpsGenSetPSL_satisfiable : ∃ (q : ℕ) (p : ℕ) (_ : Fact (Nat.Prime q)) (_ : Fact (Nat.Prime p)), p ≠ q ∧ p % 2 = 1 ∧ q % 2 = 1

Witness: lpsGenSetPSL is satisfiable.

axiom LPS.lpsGenSetPGL_card (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : (lpsGenSetPGL q p hpq hoddp hoddq hq_gt x y hxy).carrier.card = p + 1

The map from Sp to PGL(2,q) is injective (distinct tuples in Sp give distinct projective classes), and |Sp| = p+1 by Jacobi's four-square theorem. The injectivity requires that q > 2√p ensures no two distinct tuples can differ by a scalar multiple mod q. This deep number-theoretic result is not provable from Mathlib.

theorem LPS.lpsGenSetPGL_card_satisfiable : ∃ (q : ℕ) (p : ℕ) (_ : Fact (Nat.Prime q)) (_ : Fact (Nat.Prime p)), p ≠ q ∧ p % 2 = 1 ∧ q % 2 = 1

Witness: lpsGenSetPGL_card is satisfiable.

axiom LPS.lpsGenSetPSL_card (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (hleg : legendreSym q ↑p = 1) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : (lpsGenSetPSL q p hpq hoddp hoddq hq_gt hleg x y hxy).carrier.card = p + 1

Same as lpsGenSetPGL_card but for the PSL case. The injectivity of the map from Sp to PSL(2,q) via the scaled matrices requires the same deep number-theoretic arguments about quaternion arithmetic modulo q.

theorem LPS.lpsGenSetPSL_card_satisfiable : ∃ (q : ℕ) (p : ℕ) (_ : Fact (Nat.Prime q)) (_ : Fact (Nat.Prime p)), p ≠ q ∧ p % 2 = 1 ∧ q % 2 = 1

Witness: lpsGenSetPSL_card is satisfiable.

Generation property

The original statement asserts that S_{p,q} is a generating set of G, i.e., the subgroup generated by S_{p,q} equals all of G. This follows from the strong approximation theorem for quaternion algebras (Lubotzky–Phillips–Sarnak), which is far beyond current Mathlib infrastructure.

axiom LPS.lpsGenSetPGL_generates (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : Subgroup.closure ↑(lpsGenSetPGL q p hpq hoddp hoddq hq_gt x y hxy).carrier = ⊤

S_{p,q} generates all of PGL(2,q): the subgroup closure of the carrier equals the whole group. This is a deep result following from the strong approximation theorem for quaternion algebras (Lubotzky–Phillips–Sarnak).

theorem LPS.lpsGenSetPGL_generates_satisfiable : ∃ (q : ℕ) (p : ℕ) (_ : Fact (Nat.Prime q)) (_ : Fact (Nat.Prime p)), p ≠ q ∧ p % 2 = 1 ∧ q % 2 = 1

Witness: lpsGenSetPGL_generates premises are satisfiable.

axiom LPS.lpsGenSetPSL_generates (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (hleg : legendreSym q ↑p = 1) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : Subgroup.closure ↑(lpsGenSetPSL q p hpq hoddp hoddq hq_gt hleg x y hxy).carrier = ⊤

S_{p,q} generates all of PSL(2,q): the subgroup closure of the carrier equals the whole group. This is a deep result following from the strong approximation theorem for quaternion algebras (Lubotzky–Phillips–Sarnak).

theorem LPS.lpsGenSetPSL_generates_satisfiable : ∃ (q : ℕ) (p : ℕ) (_ : Fact (Nat.Prime q)) (_ : Fact (Nat.Prime p)), p ≠ q ∧ p % 2 = 1 ∧ q % 2 = 1

Witness: lpsGenSetPSL_generates premises are satisfiable.

The LPS Cayley graphs

def LPS.lpsGraphPGL (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : SimpleGraph (PGL2 q)

The LPS graph on PGL(2,q): the Cayley graph Cay(PGL(2,q), S_{p,q}). When (p/q) = -1 (Legendre symbol ≠ 1), the group is PGL(2,q).

Equations

• LPS.lpsGraphPGL q p hpq hoddp hoddq hq_gt x y hxy = CayleyGraph.cayleyGraph (LPS.lpsGenSetPGL q p hpq hoddp hoddq hq_gt x y hxy)

def LPS.lpsGraphPSL (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (hleg : legendreSym q ↑p = 1) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : SimpleGraph (PSL2 q)

The LPS graph on PSL(2,q): the Cayley graph Cay(PSL(2,q), S_{p,q}). When (p/q) = 1 (Legendre symbol = 1), the group is PSL(2,q).

Equations

• LPS.lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x y hxy = CayleyGraph.cayleyGraph (LPS.lpsGenSetPSL q p hpq hoddp hoddq hq_gt hleg x y hxy)

DecidableRel instances

instance LPS.lpsGraphPGL_decidableAdj (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : DecidableRel (lpsGraphPGL q p hpq hoddp hoddq hq_gt x y hxy).Adj

Equations

• LPS.lpsGraphPGL_decidableAdj q p hpq hoddp hoddq hq_gt x y hxy = CayleyGraph.cayleyGraph_decidableAdj (LPS.lpsGenSetPGL q p hpq hoddp hoddq hq_gt x y hxy)

instance LPS.lpsGraphPSL_decidableAdj (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (hleg : legendreSym q ↑p = 1) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : DecidableRel (lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x y hxy).Adj

Equations

• LPS.lpsGraphPSL_decidableAdj q p hpq hoddp hoddq hq_gt hleg x y hxy = CayleyGraph.cayleyGraph_decidableAdj (LPS.lpsGenSetPSL q p hpq hoddp hoddq hq_gt hleg x y hxy)

Regularity

theorem LPS.lpsGraphPGL_isRegularOfDegree (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : (lpsGraphPGL q p hpq hoddp hoddq hq_gt x y hxy).IsRegularOfDegree (p + 1)

The LPS graph on PGL is (p+1)-regular.

theorem LPS.lpsGraphPSL_isRegularOfDegree (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (hleg : legendreSym q ↑p = 1) (x y : ZMod q) (hxy : x ^ 2 + y ^ 2 + 1 = 0) : (lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x y hxy).IsRegularOfDegree (p + 1)

The LPS graph on PSL is (p+1)-regular.

Independence of the choice of (x, y)

axiom LPS.lpsGraphPGL_independent_of_xy (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (x₁ y₁ : ZMod q) (hxy₁ : x₁ ^ 2 + y₁ ^ 2 + 1 = 0) (x₂ y₂ : ZMod q) (hxy₂ : x₂ ^ 2 + y₂ ^ 2 + 1 = 0) : Nonempty (lpsGraphPGL q p hpq hoddp hoddq hq_gt x₁ y₁ hxy₁ ≃g lpsGraphPGL q p hpq hoddp hoddq hq_gt x₂ y₂ hxy₂)

For any two pairs (x₁,y₁), (x₂,y₂) with xᵢ²+yᵢ²+1=0, there exists g ∈ GL(2,𝔽_q) conjugating one quaternion embedding to the other, inducing a graph isomorphism via h ↦ ghg⁻¹. The proof requires constructing an explicit element of the orthogonal group of the norm form x²+y²+1 over 𝔽_q, which requires algebraic infrastructure not available in Mathlib.

theorem LPS.lpsGraphPGL_independent_of_xy_satisfiable : ∃ (q : ℕ) (p : ℕ) (_ : Fact (Nat.Prime q)) (_ : Fact (Nat.Prime p)), p ≠ q ∧ p % 2 = 1 ∧ q % 2 = 1

Witness: lpsGraphPGL_independent_of_xy is satisfiable.

axiom LPS.lpsGraphPSL_independent_of_xy (q : ℕ) [Fact (Nat.Prime q)] (p : ℕ) [Fact (Nat.Prime p)] (hpq : p ≠ q) (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) (hq_gt : ↑q > 2 * √↑p) (hleg : legendreSym q ↑p = 1) (x₁ y₁ : ZMod q) (hxy₁ : x₁ ^ 2 + y₁ ^ 2 + 1 = 0) (x₂ y₂ : ZMod q) (hxy₂ : x₂ ^ 2 + y₂ ^ 2 + 1 = 0) : Nonempty (lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x₁ y₁ hxy₁ ≃g lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x₂ y₂ hxy₂)

Same as lpsGraphPGL_independent_of_xy but for the PSL case. The conjugation by g ∈ GL(2,𝔽_q) preserves SL(2,𝔽_q) up to scaling, hence descends to PSL(2,q). Requires the same orthogonal group infrastructure.

theorem LPS.lpsGraphPSL_independent_of_xy_satisfiable : ∃ (q : ℕ) (p : ℕ) (_ : Fact (Nat.Prime q)) (_ : Fact (Nat.Prime p)), p ≠ q ∧ p % 2 = 1 ∧ q % 2 = 1

Witness: lpsGraphPSL_independent_of_xy is satisfiable.