Babai–Seress Conjectures on the Diameter of Finite Groups

References:

• Wikipedia, Diameter (group theory)
• H. A. Helfgott and Á. Seress, On the diameter of permutation groups
• L. Babai and Á. Seress, On the diameter of permutation groups, European Journal of Combinatorics 13 (1992), 231–243

This file contains two conjectures from the Babai–Seress paper:

• Conjecture 1.5: $\operatorname{diam}(A_n) < n^C$ for some absolute constant $C$, where $A_n$ is the alternating group on $n$ elements.

• Conjecture 1.7: $\operatorname{diam}(G) < (\log |G|)^C$ for some absolute constant $C$, where $G$ ranges over all non-abelian finite simple groups.

Conjecture 1.7 generalises Conjecture 1.5, since for $G = A_n$ we have $\log |A_n| \approx n \log n$, so a polylogarithmic bound in $|G|$ implies a polynomial bound in $n$.

def BabaiSeressConjectures.cayleyGraph {G : Type u_1} [Group G] (S : Set G) : SimpleGraph G

The (undirected) Cayley graph of a group $G$ with respect to a generating set $S$. Two elements $g, h \in G$ are adjacent iff $g \neq h$ and $g^{-1} h \in S$ or $h^{-1} g \in S$.

This is constructed using SimpleGraph.fromRel, which takes the relation $g \sim h \iff g^{-1} h \in S$ and automatically symmetrizes it (via disjunction with the reverse relation) and enforces irreflexivity (via $g \neq h$). In particular, this definition effectively uses the symmetrization $S \cup S^{-1}$, so it produces a standard undirected Cayley graph even when $S$ is not itself symmetric.

Equations

• BabaiSeressConjectures.cayleyGraph S = SimpleGraph.fromRel fun (g h : G) => g⁻¹ * h ∈ S

noncomputable def BabaiSeressConjectures.groupDiam (G : Type u_1) [Group G] [Fintype G] : ℕ

The diameter of a finite group $G$, defined as the maximum diameter of the Cayley graphs $\Gamma(G, A)$ over all generating sets $A$ of $G$.

Equations

• BabaiSeressConjectures.groupDiam G = sSup {d : ℕ | ∃ (S : Set G), Subgroup.closure S = ⊤ ∧ (BabaiSeressConjectures.cayleyGraph S).diam = d}

theorem BabaiSeressConjectures.groupDiam_fin_one : groupDiam ↥(alternatingGroup (Fin 0)) = 0

For the trivial group (with one element), the group diameter is zero, since every Cayley graph has only one vertex and hence diameter zero.

theorem BabaiSeressConjectures.groupDiam_alternating_three : groupDiam ↥(alternatingGroup (Fin 3)) = 1

The alternating group $A_3 \cong \mathbb{Z}/3\mathbb{Z}$ has group diameter $1$: every non-trivial generating set produces a complete Cayley graph $K_3$, since any single non-identity element and its inverse already reach the entire group.

theorem BabaiSeressConjectures.groupDiam_perm_two : groupDiam (Equiv.Perm (Fin 2)) = 1

The symmetric group $S_2 \cong \mathbb{Z}/2\mathbb{Z}$ has group diameter $1$: the unique generating set $\{(01)\}$ produces the complete graph $K_2$, since the single non-identity element and its inverse (which are equal) cover the only other vertex.

theorem BabaiSeressConjectures.babai_seress_conjecture_alternating : ∃ (C : ℕ), ∀ (n : ℕ), ↑(groupDiam ↥(alternatingGroup (Fin n))) ≤ ↑n ^ C

Babai–Seress Conjecture (Conjecture 1.5): There exists an absolute constant $C$ such that the diameter of the alternating group $A_n$ satisfies $$\operatorname{diam}(A_n) \leq n^C.$$

Reference: L. Babai and Á. Seress, On the diameter of permutation groups, European Journal of Combinatorics 13 (1992), Conjecture 1.5

theorem BabaiSeressConjectures.babai_seress_conjecture : ∃ (C : ℕ), ∀ (G : Type) [inst : Group G] [inst_1 : Fintype G] [IsSimpleGroup G], (∃ (a : G) (b : G), a * b ≠ b * a) → ↑(groupDiam G) ≤ Real.log ↑(Fintype.card G) ^ C

Babai–Seress Conjecture (Conjecture 1.7): There exists an absolute constant $C$ such that every finite simple non-abelian group $G$ satisfies $$\operatorname{diam}(G) \leq (\log |G|)^C.$$

Reference: L. Babai and Á. Seress, On the diameter of permutation groups, European Journal of Combinatorics 13 (1992), Conjecture 1.7