Main theorem

The complete reader-facing interface: the four non-Mathlib definitions needed to read the result, followed by one theorem.

theorem SaxlCounterexamples.MainTheorems.mainTheorem (B degreeBound : ℕ) (hB : 2 ≤ B) : ∃ (P : FinitePermutationGroup), degreeBound ≤ Nat.card P.Point ∧ MulAction.IsPreprimitive P.G P.Point ∧ P.baseSize = B ∧ ∃ (x : P.Point) (y : P.Point), ¬P.saxlGraph.Adj x y ∧ P.saxlGraph.commonNeighbors x y = ∅

For every base size B ≥ 2 and every prescribed bound there is a primitive permutation group of degree at least that bound and base size B whose generalised Saxl graph has two nonadjacent vertices with no common neighbour.