Common neighbour conjectures for Saxl graphs fail at every base size
Aluna Rizzoli, Adam R. Thomas
math.GR
Sep 1, 2026 · v1
math.CO
TL;DR
Theorem 1.2, counterexamples at every base size, is formally verified in Lean 4 with Mathlib, largely produced by Codex and reviewed by the authors.
Abstract
For a finite permutation group, a base is a set of points with trivial pointwise stabiliser, and the generalised Saxl graph records which pairs of points lie together in a base of minimum size. Burness and Giudici conjectured that any two vertices of the Saxl graph of a primitive group of base size two have a common neighbour, and Freedman, Huang, Lee and Rekvényi extended this conjecture to arbitrary base size. We disprove both. For each integer $B\ge2$ we construct infinitely many primitive groups of base size $B$ whose generalised Saxl graphs contain two nonadjacent vertices with no common neighbour. At base size two, where this is the usual Saxl graph, we obtain three further infinite families, one each of affine, product and twisted wreath type, so the conjecture fails in three of the five O'Nan–Scott types; in the affine and product type families the Saxl graphs have diameter exactly three. This answers Problem 21.29 in the Kourovka Notebook in the negative. In the positive direction, we prove the Burness–Giudici conjecture for every primitive affine group whose point stabiliser is almost quasisimple of sporadic type, completing work of Lee and Popiel. We conjecture that no base-two counterexample of almost simple or diagonal type exists.
Problem
Burness and Giudici conjectured that any two vertices of the Saxl graph of a primitive group of base size two have a common neighbour. Freedman, Huang, Lee and Rekvényi extended this conjecture to generalised Saxl graphs at arbitrary base size. The question is Problem 21.29 in the Kourovka Notebook.
Approach
Infinite families of counterexamples are built from affine groups, product-action wreath products, and twisted wreath products. Sumset criteria on the regular vectors handle the affine case. A uniform affine construction uses deleted permutation modules of Frobenius groups over F_{3^d} and works for every base size B≥2. The main theorem is formalised in Lean 4 with Mathlib, using a Codex-produced proof that the authors reviewed. The remaining results rely on GAP, Magma and C++ computations.
Results
Both conjectures are false at every base size, and at base size two they fail in the affine, product and twisted wreath O'Nan–Scott types, with diameter 3 in the affine and product families. The Burness–Giudici conjecture is proved for affine groups whose point stabiliser is almost quasisimple of sporadic type. The Lean proof uses no sorry placeholders or project-specific axioms.
| V | H | \ | V_reg\ | | \ | V \ 2V_reg\ | | diam Σ |
|---|
| F_3^9 | C_2^6:D_18 | 1152 | 96 | 3 |
| F_3^10 | C_2^5:S_5 | 3840 | 64 | 3 |
| F_3^12 | C_2^8:(12T35) | 18432 | 1600 | 3 |
| F_3^12 | C_2^8:(12T38) | 18432 | 1600 | 3 |
The four counterexamples found in the affine searches