Internal implementation of the main theorem

Construction parameters, bridge lemmas, and proof machinery used by the minimal public module Examples.MainTheorems.

theorem SaxlCounterexamples.MainTheorems.Internal.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.