Theorem 11: LPS Graphs are Ramanujan

Main Results

• pgl2_card_ge_six: PGL(2, q) has at least 6 elements for odd prime q ≥ 5.
• psl2_card_ge_six: PSL(2, q) has at least 6 elements for odd prime q ≥ 5.
• lpsGraphPGL_card_ge_two: The LPS graph on PGL has at least 2 vertices.
• lpsGraphPSL_card_ge_two: The LPS graph on PSL has at least 2 vertices.
• lpsGraphPGL_lambda2_le: Under Ramanujan + spectral hypotheses, λ₂ ≤ 2√p.
• lpsGraphPSL_lambda2_le: Under Ramanujan + spectral hypotheses, λ₂ ≤ 2√p.

The connectedness and Ramanujan properties of LPS graphs follow from deep results in algebraic number theory (the Ramanujan–Petersson conjecture, proved via the Weil conjectures by Deligne). These are taken as hypotheses in the main theorems, since the required algebraic geometry is not available in Mathlib.

Cardinality bounds: PGL and PSL have at least 6 elements

theorem LPSRamanujan.pgl2_card_ge_six (q : ℕ) [Fact (Nat.Prime q)] (_hoddq : q % 2 = 1) (hq_ge : q ≥ 5) : 6 ≤ Fintype.card (LPS.PGL2 q)

The PGL(2, q) group has at least 6 elements when q ≥ 5.

theorem LPSRamanujan.psl2_card_ge_six (q : ℕ) [Fact (Nat.Prime q)] (_hoddq : q % 2 = 1) (hq_ge : q ≥ 5) : 6 ≤ Fintype.card (LPS.PSL2 q)

The PSL(2, q) group has at least 6 elements when q ≥ 5.

theorem LPSRamanujan.q_ge_five (q p : ℕ) [Fact (Nat.Prime p)] (hoddp : p % 2 = 1) (hoddq : q % 2 = 1) [Fact (Nat.Prime q)] (hq_gt : ↑q > 2 * √↑p) : q ≥ 5

An odd prime q with q > 2√p for odd prime p ≥ 3 satisfies q ≥ 5.

theorem LPSRamanujan.lpsGraphPGL_card_ge_two (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) : 2 ≤ Fintype.card (LPS.PGL2 q)

The LPS graph on PGL has at least 2 vertices.

theorem LPSRamanujan.lpsGraphPSL_card_ge_two (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) : 2 ≤ Fintype.card (LPS.PSL2 q)

The LPS graph on PSL has at least 2 vertices.

Connectedness, Ramanujan property, and spectral bounds

The following deep results are taken as hypotheses in downstream theorems:

• Connectedness of LPS graphs follows from the fact that S_{p,q} generates PGL/PSL.
• Ramanujan property follows from the Ramanujan–Petersson conjecture for GL(2)/ℚ, proved by Eichler–Igusa (weight 2) building on the Weil conjectures (Deligne, 1974).
• Spectral bound |λ₂| < s for connected s-regular graphs follows from the Perron–Frobenius theorem for non-negative matrices.

These results require algebraic geometry and spectral theory not available in Mathlib. They appear as explicit hypotheses hconn, hram, and hspec in the theorems below.

Corollary: λ₂ ≤ 2√p

theorem LPSRamanujan.lpsGraphPGL_lambda2_le (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) (hram : GraphExpansion.IsRamanujan (LPS.lpsGraphPGL q p hpq hoddp hoddq hq_gt x y hxy) (p + 1) ⋯) (hspec : |GraphExpansion.secondLargestEigenvalue (LPS.lpsGraphPGL q p hpq hoddp hoddq hq_gt x y hxy) ⋯| < ↑p + 1) : GraphExpansion.secondLargestEigenvalue (LPS.lpsGraphPGL q p hpq hoddp hoddq hq_gt x y hxy) ⋯ ≤ 2 * √↑p

The second-largest eigenvalue of the LPS graph on PGL satisfies λ₂ ≤ 2√p. The Ramanujan property and the spectral bound |λ₂| < s for connected regular graphs are deep results taken as hypotheses.

theorem LPSRamanujan.lpsGraphPSL_lambda2_le (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) (hram : GraphExpansion.IsRamanujan (LPS.lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x y hxy) (p + 1) ⋯) (hspec : |GraphExpansion.secondLargestEigenvalue (LPS.lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x y hxy) ⋯| < ↑p + 1) : GraphExpansion.secondLargestEigenvalue (LPS.lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x y hxy) ⋯ ≤ 2 * √↑p

The second-largest eigenvalue of the LPS graph on PSL satisfies λ₂ ≤ 2√p. The Ramanujan property and the spectral bound are taken as hypotheses.

Combined result

theorem LPSRamanujan.lpsRamanujan_PGL (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) (hconn : (LPS.lpsGraphPGL q p hpq hoddp hoddq hq_gt x y hxy).Connected) (hram : GraphExpansion.IsRamanujan (LPS.lpsGraphPGL q p hpq hoddp hoddq hq_gt x y hxy) (p + 1) ⋯) : let G := LPS.lpsGraphPGL q p hpq hoddp hoddq hq_gt x y hxy; G.Connected ∧ G.IsRegularOfDegree (p + 1) ∧ 2 ≤ Fintype.card (LPS.PGL2 q) ∧ GraphExpansion.IsRamanujan G (p + 1) ⋯

LPS Ramanujan Theorem (PGL, combined). The LPS graph X_{p,q} on PGL(2,q) is (p+1)-regular and has ≥ 2 vertices (proved). Under the hypotheses that the graph is connected and Ramanujan (deep results from Lubotzky–Phillips–Sarnak requiring algebraic geometry not in Mathlib), the full combined result holds.

theorem LPSRamanujan.lpsRamanujan_PSL (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) (hconn : (LPS.lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x y hxy).Connected) (hram : GraphExpansion.IsRamanujan (LPS.lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x y hxy) (p + 1) ⋯) : let G := LPS.lpsGraphPSL q p hpq hoddp hoddq hq_gt hleg x y hxy; G.Connected ∧ G.IsRegularOfDegree (p + 1) ∧ 2 ≤ Fintype.card (LPS.PSL2 q) ∧ GraphExpansion.IsRamanujan G (p + 1) ⋯

LPS Ramanujan Theorem (PSL, combined). The LPS graph X_{p,q} on PSL(2,q) is (p+1)-regular and has ≥ 2 vertices (proved). Under the hypotheses that the graph is connected and Ramanujan (deep results), the full combined result holds.