Counterexamples at every base size

This module instantiates the abstract obstruction construction with the affine Frobenius groups and their deleted binary permutation modules.

noncomputable def SaxlCounterexamples.EveryBase.hqSeed (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) : EveryBaseSeed

The concrete binary seed attached to GF(3^d).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SaxlCounterexamples.EveryBase.hqColourTower (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) : RegularTupleColourTower (hqSeed d hd hd3)

The canonical regular-tuple colour tower for the concrete seed.

Equations

• SaxlCounterexamples.EveryBase.hqColourTower d hd hd3 = SaxlCounterexamples.EveryBase.quotientRegularTupleColourTower (SaxlCounterexamples.EveryBase.hqSeed d hd hd3)

noncomputable def SaxlCounterexamples.EveryBase.hqColours (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : BaseArrayColours (hqSeed d hd hd3) tail

The canonical tuple and vector colours at the requested tail length.

Equations

• SaxlCounterexamples.EveryBase.hqColours d hd hd3 tail = SaxlCounterexamples.EveryBase.quotientBaseArrayColours (SaxlCounterexamples.EveryBase.hqSeed d hd hd3) tail

noncomputable def SaxlCounterexamples.EveryBase.hqFirstColour (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : (hqColours d hd hd3 tail).C

A chosen colour at the requested tail length.

Equations

• SaxlCounterexamples.EveryBase.hqFirstColour d hd hd3 tail = Classical.choice ⋯

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.HqColourType (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : Type

The tuple-colour type for the concrete construction.

Equations

• SaxlCounterexamples.EveryBase.HqColourType d hd hd3 tail = (SaxlCounterexamples.EveryBase.hqColours d hd hd3 tail).C

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.HqLinearGroup (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : Type

The linear permutation-wreath group in the construction.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.HqProductModule (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : Type

The product module on which the linear group acts.

Equations

• SaxlCounterexamples.EveryBase.HqProductModule d hd hd3 tail = (SaxlCounterexamples.EveryBase.HqColourType d hd hd3 tail → ↥(SaxlCounterexamples.EveryBase.Vq d))

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.GBd (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : Type

The affine permutation group used for base size tail + 2.

Equations

• SaxlCounterexamples.EveryBase.GBd d hd hd3 tail = Saxl.AffineGroup (SaxlCounterexamples.EveryBase.HqLinearGroup d hd hd3 tail) (SaxlCounterexamples.EveryBase.HqProductModule d hd hd3 tail)

noncomputable def SaxlCounterexamples.EveryBase.hqBadVector (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : HqProductModule d hd hd3 tail

The explicit vector outside the doubled generalized neighborhood.

Equations

• One or more equations did not get rendered due to their size.

theorem SaxlCounterexamples.EveryBase.hq_zero_not_generalizedAdjacent_badVector (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) : ¬Saxl.GeneralizedAdjacent (GBd d hd hd3 0) (HqProductModule d hd hd3 0) 0 0 (hqBadVector d hd hd3 0)

At base size two, the displayed vertices are nonadjacent.

theorem SaxlCounterexamples.EveryBase.hq_exactBase_and_noCommonNeighbour (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : Saxl.ExactBaseSize (Saxl.AffineGroup (LinearTop (hqSeed d hd hd3) (hqColours d hd hd3 tail)) (ProductModule (hqSeed d hd hd3) (hqColours d hd hd3 tail))) (ProductModule (hqSeed d hd hd3) (hqColours d hd hd3 tail)) (tail + 2) ∧ ¬Saxl.HasCommonNeighbour (ProductModule (hqSeed d hd hd3) (hqColours d hd hd3 tail)) (Saxl.GeneralizedAdjacent (Saxl.AffineGroup (LinearTop (hqSeed d hd hd3) (hqColours d hd hd3 tail)) (ProductModule (hqSeed d hd hd3) (hqColours d hd hd3 tail))) (ProductModule (hqSeed d hd hd3) (hqColours d hd hd3 tail)) tail) 0 (badVector (hqSeed d hd hd3) (hqColours d hd hd3 tail) (hqFirstColour d hd hd3 tail))

theorem SaxlCounterexamples.EveryBase.hq_linearTop_irreducible (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : (Representation.ofDistribMulAction F2 (Saxl.PermWreath (Hq d) (Equiv.Perm (hqColours d hd hd3 tail).C) (hqColours d hd hd3 tail).C) ((hqColours d hd hd3 tail).C → ↥(Vq d))).IsIrreducible

theorem SaxlCounterexamples.EveryBase.hq_primitive (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : MulAction.IsPreprimitive (GBd d hd hd3 tail) (HqProductModule d hd hd3 tail)

theorem SaxlCounterexamples.EveryBase.hq_coreFamily (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : Saxl.ExactBaseSize (GBd d hd hd3 tail) (HqProductModule d hd hd3 tail) (tail + 2) ∧ MulAction.IsPreprimitive (GBd d hd hd3 tail) (HqProductModule d hd hd3 tail) ∧ ¬Saxl.HasCommonNeighbour (HqProductModule d hd hd3 tail) (Saxl.GeneralizedAdjacent (GBd d hd hd3 tail) (HqProductModule d hd hd3 tail) tail) 0 (hqBadVector d hd hd3 tail)

theorem SaxlCounterexamples.EveryBase.vq_card_le_productModule_card (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (tail : ℕ) : Nat.card ↥(Vq d) ≤ Nat.card (HqProductModule d hd hd3 tail)