Abstract data for counterexamples at every base size

This module contains the explicit binary permutation-module seed, arbitrary base-array criterion, a quotient-independent finite tuple-colour interface with canonical quotient realizations, symbolic colour growth, and the affine exact-base-size successor bridge used by the obstruction construction.

Faithfulness and irreducibility are intentionally absent from EveryBaseSeed: they are used only later to prove primitivity and are not needed for the obstruction.

Arbitrary-length base arrays

def SaxlCounterexamples.EveryBase.SameTupleOrbit (H : Type u_1) {V : Type u_2} [Group H] [MulAction H V] {n : ℕ} (x y : Fin n → V) : Prop

Two tuples lie in the same orbit under the diagonal action of H.

Equations

• SaxlCounterexamples.EveryBase.SameTupleOrbit H x y = ∃ (h : H), ∀ (j : Fin n), h • x j = y j

def SaxlCounterexamples.EveryBase.TupleRowsDistinguishing (H : Type u_1) (Q : Type u_2) {V : Type u_3} {ι : Type u_4} [Group H] [Group Q] [MulAction H V] [MulAction Q ι] {n : ℕ} (rows : ι → Fin n → V) : Prop

The tuple rows distinguish every nonidentity element of the top group.

Equations

• SaxlCounterexamples.EveryBase.TupleRowsDistinguishing H Q rows = ∀ (q : Q), (∀ (i : ι), SaxlCounterexamples.EveryBase.SameTupleOrbit H (rows (q⁻¹ • i)) (rows i)) → q = 1

theorem SaxlCounterexamples.EveryBase.permWreath_isBaseTuple_iff (H : Type u_1) (Q : Type u_2) (ι : Type u_3) (V : Type u_4) [Group H] [Group Q] [MulAction H V] [MulAction Q ι] {n : ℕ} (rows : Fin n → ι → V) : Saxl.IsBaseTuple (Saxl.PermWreath H Q ι) (ι → V) rows ↔ (∀ (i : ι), Saxl.IsBaseTuple H V fun (j : Fin n) => rows j i) ∧ TupleRowsDistinguishing H Q fun (i : ι) (j : Fin n) => rows j i

structure SaxlCounterexamples.EveryBase.TupleColourCode (H : Type u_1) (V : Type u_2) [Group H] [MulAction H V] (n : ℕ) (C : Type u_3) : Type (max u_2 u_3)

A complete finite coding of the H-orbits of base tuples.

• colour : (Fin n → V) → C

  The colour assigned to a tuple.

• colour_eq_iff_sameOrbit {x y : Fin n → V} : Saxl.IsBaseTuple H V x → Saxl.IsBaseTuple H V y → (self.colour x = self.colour y ↔ SameTupleOrbit H x y)
• hits (c : C) : ∃ (x : Fin n → V), Saxl.IsBaseTuple H V x ∧ self.colour x = c

theorem SaxlCounterexamples.EveryBase.permWreath_isBaseTuple_iff_colourWord (H : Type u_1) (Q : Type u_2) (ι : Type u_3) (V : Type u_4) (C : Type u_5) [Group H] [Group Q] [MulAction H V] [MulAction Q ι] {n : ℕ} (code : TupleColourCode H V n C) (rows : Fin n → ι → V) : Saxl.IsBaseTuple (Saxl.PermWreath H Q ι) (ι → V) rows ↔ (∀ (i : ι), Saxl.IsBaseTuple H V fun (j : Fin n) => rows j i) ∧ Saxl.WordDistinguishing Q fun (i : ι) => code.colour fun (j : Fin n) => rows j i

theorem SaxlCounterexamples.EveryBase.symmetricTop_isBaseTuple_iff_bijective (H : Type u_1) (V : Type u_2) (C : Type u_3) [Group H] [MulAction H V] [Finite C] {n : ℕ} (code : TupleColourCode H V n C) (rows : Fin n → C → V) : Saxl.IsBaseTuple (Saxl.PermWreath H (Equiv.Perm C) C) (C → V) rows ↔ (∀ (i : C), Saxl.IsBaseTuple H V fun (j : Fin n) => rows j i) ∧ Function.Bijective fun (i : C) => code.colour fun (j : Fin n) => rows j i

Explicit binary permutation-module seed interface

structure SaxlCounterexamples.EveryBase.AvoidingCycle (H : Type u_1) (Ω : Type u_2) [Group H] [MulAction H Ω] (h : H) (omega0 : Ω) : Type u_2

An odd invariant cycle avoiding a distinguished point.

• carrier : Finset Ω

  The finite carrier of the cycle.

• avoids : omega0 ∉ self.carrier
• odd_card : Odd self.carrier.card
• invariant (ω : Ω) : ω ∈ self.carrier ↔ h • ω ∈ self.carrier

structure SaxlCounterexamples.EveryBase.EveryBaseSeed : Type (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1))

Exactly the data used by the abstract obstruction. Faithfulness and irreducibility are deliberately absent because the cycle-sum proof does not use them.

• Ω : Type u_1

  The finite coordinate set.

• H : Type u_2

  The seed group.

• V : Type u_3

  The seed module.

• fintypeOmega : Fintype self.Ω
• fintypeV : Fintype self.V
• decidableEqOmega : DecidableEq self.Ω
• groupH : Group self.H
• addCommGroupV : AddCommGroup self.V
• moduleV : Module (ZMod 2) self.V
• actionHOmega : MulAction self.H self.Ω
• actionHV : DistribMulAction self.H self.V
• omega0 : self.Ω

  The distinguished coordinate.

• u : self.V

  The vector vanishing exactly at the distinguished coordinate.

• regular_exists : ∃ (v : self.V), Saxl.IsRegularVector self.H self.V v
• coord : self.V →+ self.Ω → ZMod 2

  The equivariant coordinate map into the binary permutation module.

• coord_smul (h : self.H) (v : self.V) (ω : self.Ω) : self.coord (h • v) ω = self.coord v (h⁻¹ • ω)
• u_coord (ω : self.Ω) : self.coord self.u ω = if ω = self.omega0 then 0 else 1
• avoidingCycle (h : self.H) : AvoidingCycle self.H self.Ω h self.omega0

  An avoiding cycle for every group element.

def SaxlCounterexamples.EveryBase.cycleSum (S : EveryBaseSeed) (L : Finset S.Ω) (v : S.V) : ZMod 2

Sum the binary coordinates of v over L.

Equations

• SaxlCounterexamples.EveryBase.cycleSum S L v = ∑ ω ∈ L, S.coord v ω

def SaxlCounterexamples.EveryBase.AvoidingCycle.reindexEquiv (S : EveryBaseSeed) (h : S.H) : ↥(S.avoidingCycle h).carrier ≃ ↥(S.avoidingCycle h).carrier

Reindex an avoiding cycle by the action of its group element.

Equations

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

theorem SaxlCounterexamples.EveryBase.cycleSum_smul (S : EveryBaseSeed) (h : S.H) (v : S.V) : cycleSum S (S.avoidingCycle h).carrier (h • v) = cycleSum S (S.avoidingCycle h).carrier v

theorem SaxlCounterexamples.EveryBase.cycleSum_add_smul (S : EveryBaseSeed) (h : S.H) (v : S.V) : cycleSum S (S.avoidingCycle h).carrier (v + h • v) = 0

theorem SaxlCounterexamples.EveryBase.cycleSum_u (S : EveryBaseSeed) (h : S.H) : cycleSum S (S.avoidingCycle h).carrier S.u = 1

theorem SaxlCounterexamples.EveryBase.u_ne_add_smul (S : EveryBaseSeed) (h : S.H) (v : S.V) : S.u ≠ v + h • v

Finite regular-tuple colours and orbit profiles

structure SaxlCounterexamples.EveryBase.VectorOrbitCode (H : Type u_1) (V : Type u_2) [Group H] [MulAction H V] (D : Type u_3) : Type (max u_2 u_3)

A complete code for the vector orbits of a group action.

• colour : V → D

  The colour assigned to a vector.

• colour_eq_iff_sameOrbit (x y : V) : self.colour x = self.colour y ↔ ∃ (h : H), h • x = y

structure SaxlCounterexamples.EveryBase.BaseArrayColours (S : EveryBaseSeed) (tail : ℕ) : Type (max (max (u_1 + 1) (u_2 + 1)) u_5)

A finite colour system for the tail + 1-tuples used in a generalized neighbourhood. firstColour is not extra mathematics: its compatibility field says exactly that it records the ordinary orbit of the first tuple entry. Keeping it explicit avoids quotient choice in executable files.

• C : Type u_1

  Colours for regular tuples of length tail + 1.

• D : Type u_2

  Colours for vector orbits.

• fintypeC : Fintype self.C
• decidableEqC : DecidableEq self.C
• tupleCode : TupleColourCode S.H S.V (tail + 1) self.C

  The regular-tuple orbit code.

• vectorCode : VectorOrbitCode S.H S.V self.D

  The vector-orbit code.

• firstColour : self.C → self.D

  Project a tuple colour to the colour of its first vector.

• firstColour_compat (x : Fin (tail + 1) → S.V) : Saxl.IsBaseTuple S.H S.V x → self.vectorCode.colour (x 0) = self.firstColour (self.tupleCode.colour x)

structure SaxlCounterexamples.EveryBase.RegularTupleColourTower (S : EveryBaseSeed) : Type (max (u_1 + 1) u_4)

Concrete finite types of all positive-length regular tuple orbits. Index t records colours of tuples of length t + 1. Positive indexing is essential: for a nontrivial group there are no regular zero-tuples, so a total colour map at length zero cannot exist.

• C : ℕ → Type u_1

  The colour type for each positive tuple length.

• fintypeC (n : ℕ) : Fintype (self.C n)

  Finiteness of every colour type.

• code (n : ℕ) : TupleColourCode S.H S.V (n + 1) (self.C n)

  The orbit code at each positive tuple length.

def SaxlCounterexamples.EveryBase.RegularTupleColourTower.card {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) : ℕ

The number of regular-tuple colours at level n.

Equations

• T.card n = Fintype.card (T.C n)

noncomputable def SaxlCounterexamples.EveryBase.RegularTupleColourTower.representative {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) (c : T.C n) : Fin (n + 1) → S.V

Choose a base-tuple representative of a colour.

Equations

• T.representative n c = Classical.choose ⋯

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.representative_isBase {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) (c : T.C n) : Saxl.IsBaseTuple S.H S.V (T.representative n c)

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.representative_colour {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) (c : T.C n) : (T.code n).colour (T.representative n c) = c

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.colour_nonempty {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) : Nonempty (T.C n)

noncomputable def SaxlCounterexamples.EveryBase.RegularTupleColourTower.appendColour {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) : T.C n × S.V → T.C (n + 1)

Append a vector to a representative and return the resulting colour.

Equations

• T.appendColour n cv = (T.code (n + 1)).colour (Fin.snoc (T.representative n cv.1) cv.2)

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.appendColour_injective {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) : Function.Injective (T.appendColour n)

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.card_mul_le_next {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) : T.card n * Fintype.card S.V ≤ T.card (n + 1)

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.card_lt_next {S : EveryBaseSeed} [Nontrivial S.V] (T : RegularTupleColourTower S) (n : ℕ) : T.card n < T.card (n + 1)

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.card_strictMono {S : EveryBaseSeed} [Nontrivial S.V] (T : RegularTupleColourTower S) : StrictMono T.card

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.card_lt_of_lt {S : EveryBaseSeed} [Nontrivial S.V] (T : RegularTupleColourTower S) {m n : ℕ} (hmn : m < n) : T.card m < T.card n

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.RegularTupleColourTower.LinearGroup {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) : Type (max (max u_2 u_4) u_4)

The permutation-wreath group associated to level n.

Equations

• T.LinearGroup n = Saxl.PermWreath S.H (Equiv.Perm (T.C n)) (T.C n)

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.RegularTupleColourTower.LinearSpace {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) : Type (max u_4 u_3)

The product module associated to level n.

Equations

• T.LinearSpace n = (T.C n → S.V)

noncomputable def SaxlCounterexamples.EveryBase.RegularTupleColourTower.baseRows {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) : Fin (n + 1) → T.LinearSpace n

The canonical base rows formed from all chosen representatives.

Equations

• T.baseRows n j c = T.representative n c j

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.baseRows_isBase {S : EveryBaseSeed} (T : RegularTupleColourTower S) (n : ℕ) : Saxl.IsBaseTuple (T.LinearGroup n) (T.LinearSpace n) (T.baseRows n)

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.no_baseTuple_of_card_lt {S : EveryBaseSeed} (T : RegularTupleColourTower S) {m n : ℕ} (hcard : T.card m < T.card n) : ¬∃ (rows : Fin (m + 1) → T.LinearSpace n), Saxl.IsBaseTuple (T.LinearGroup n) (T.LinearSpace n) rows

Canonical finite quotient colours

These constructions show that the positive-length colour-tower interface is inhabited for every finite seed. Nonbase tuples receive the colour of a fixed constant regular tuple; on base tuples the colour is the actual diagonal orbit quotient.

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.RegularTuple (S : EveryBaseSeed) (n : ℕ) : Type u_3

A regular tuple of positive length n + 1.

Equations

• SaxlCounterexamples.EveryBase.RegularTuple S n = { x : Fin (n + 1) → S.V // Saxl.IsBaseTuple S.H S.V x }

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.regularTupleFintype (S : EveryBaseSeed) (n : ℕ) : Fintype (RegularTuple S n)

Equations

• SaxlCounterexamples.EveryBase.regularTupleFintype S n = id inferInstance

def SaxlCounterexamples.EveryBase.regularTupleSetoid (S : EveryBaseSeed) (n : ℕ) : Setoid (RegularTuple S n)

Orbit equivalence on regular tuples.

Equations

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

@[instance_reducible]

instance SaxlCounterexamples.EveryBase.regularTupleSetoidInstance (S : EveryBaseSeed) (n : ℕ) : Setoid (RegularTuple S n)

Equations

• SaxlCounterexamples.EveryBase.regularTupleSetoidInstance S n = SaxlCounterexamples.EveryBase.regularTupleSetoid S n

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.RegularTupleColour (S : EveryBaseSeed) (n : ℕ) : Type u_3

The quotient colour type of regular tuples under the diagonal action.

Equations

• SaxlCounterexamples.EveryBase.RegularTupleColour S n = Quotient (SaxlCounterexamples.EveryBase.regularTupleSetoid S n)

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.regularTupleRelDecidable (S : EveryBaseSeed) (n : ℕ) : DecidableRel fun (x1 x2 : RegularTuple S n) => x1 ≈ x2

Equations

• SaxlCounterexamples.EveryBase.regularTupleRelDecidable S n x✝¹ x✝ = Classical.propDecidable ((fun (x1 x2 : SaxlCounterexamples.EveryBase.RegularTuple S n) => x1 ≈ x2) x✝¹ x✝)

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.regularTupleColourFintype (S : EveryBaseSeed) (n : ℕ) : Fintype (RegularTupleColour S n)

Equations

• SaxlCounterexamples.EveryBase.regularTupleColourFintype S n = inferInstance

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.regularTupleColourDecidableEq (S : EveryBaseSeed) (n : ℕ) : DecidableEq (RegularTupleColour S n)

Equations

• SaxlCounterexamples.EveryBase.regularTupleColourDecidableEq S n = Classical.typeDecidableEq (SaxlCounterexamples.EveryBase.RegularTupleColour S n)

noncomputable def SaxlCounterexamples.EveryBase.defaultRegularTuple (S : EveryBaseSeed) (n : ℕ) : RegularTuple S n

A default constant regular tuple, used to colour nonbase tuples.

Equations

• SaxlCounterexamples.EveryBase.defaultRegularTuple S n = ⟨fun (x : Fin (n + 1)) => Classical.choose ⋯, ⋯⟩

noncomputable def SaxlCounterexamples.EveryBase.regularTupleColour (S : EveryBaseSeed) (n : ℕ) (x : Fin (n + 1) → S.V) : RegularTupleColour S n

Colour a tuple by its orbit, using the default colour when it is not a base.

Equations

• SaxlCounterexamples.EveryBase.regularTupleColour S n x = if hx : Saxl.IsBaseTuple S.H S.V x then ⟦⟨x, hx⟩⟧ else ⟦SaxlCounterexamples.EveryBase.defaultRegularTuple S n⟧

theorem SaxlCounterexamples.EveryBase.regularTupleColour_eq_iff_sameOrbit (S : EveryBaseSeed) (n : ℕ) {x y : Fin (n + 1) → S.V} (hx : Saxl.IsBaseTuple S.H S.V x) (hy : Saxl.IsBaseTuple S.H S.V y) : regularTupleColour S n x = regularTupleColour S n y ↔ SameTupleOrbit S.H x y

theorem SaxlCounterexamples.EveryBase.regularTupleColour_hits (S : EveryBaseSeed) (n : ℕ) (c : RegularTupleColour S n) : ∃ (x : Fin (n + 1) → S.V), Saxl.IsBaseTuple S.H S.V x ∧ regularTupleColour S n x = c

noncomputable def SaxlCounterexamples.EveryBase.regularTupleCode (S : EveryBaseSeed) (n : ℕ) : TupleColourCode S.H S.V (n + 1) (RegularTupleColour S n)

The canonical orbit code for regular tuples of length n + 1.

Equations

• SaxlCounterexamples.EveryBase.regularTupleCode S n = { colour := SaxlCounterexamples.EveryBase.regularTupleColour S n, colour_eq_iff_sameOrbit := ⋯, hits := ⋯ }

noncomputable def SaxlCounterexamples.EveryBase.quotientRegularTupleColourTower (S : EveryBaseSeed) : RegularTupleColourTower S

The canonical, genuinely inhabited positive regular-colour tower.

Equations

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

def SaxlCounterexamples.EveryBase.vectorOrbitSetoid (S : EveryBaseSeed) : Setoid S.V

Orbit equivalence on vectors in the seed module.

Equations

• SaxlCounterexamples.EveryBase.vectorOrbitSetoid S = { r := fun (x y : S.V) => ∃ (h : S.H), h • x = y, iseqv := ⋯ }

@[instance_reducible]

instance SaxlCounterexamples.EveryBase.vectorOrbitSetoidInstance (S : EveryBaseSeed) : Setoid S.V

Equations

• SaxlCounterexamples.EveryBase.vectorOrbitSetoidInstance S = SaxlCounterexamples.EveryBase.vectorOrbitSetoid S

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.VectorOrbitColour (S : EveryBaseSeed) : Type u_3

The quotient colour type of vector orbits.

Equations

• SaxlCounterexamples.EveryBase.VectorOrbitColour S = Quotient (SaxlCounterexamples.EveryBase.vectorOrbitSetoid S)

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.vectorOrbitRelDecidable (S : EveryBaseSeed) : DecidableRel fun (x1 x2 : S.V) => x1 ≈ x2

Equations

• SaxlCounterexamples.EveryBase.vectorOrbitRelDecidable S x✝¹ x✝ = Classical.propDecidable ((fun (x1 x2 : S.V) => x1 ≈ x2) x✝¹ x✝)

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.vectorOrbitColourFintype (S : EveryBaseSeed) : Fintype (VectorOrbitColour S)

Equations

• SaxlCounterexamples.EveryBase.vectorOrbitColourFintype S = inferInstance

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.vectorOrbitColourDecidableEq (S : EveryBaseSeed) : DecidableEq (VectorOrbitColour S)

Equations

• SaxlCounterexamples.EveryBase.vectorOrbitColourDecidableEq S = Classical.typeDecidableEq (SaxlCounterexamples.EveryBase.VectorOrbitColour S)

noncomputable def SaxlCounterexamples.EveryBase.quotientVectorOrbitCode (S : EveryBaseSeed) : VectorOrbitCode S.H S.V (VectorOrbitColour S)

The canonical quotient code for vector orbits.

Equations

• SaxlCounterexamples.EveryBase.quotientVectorOrbitCode S = { colour := Quotient.mk (SaxlCounterexamples.EveryBase.vectorOrbitSetoid S), colour_eq_iff_sameOrbit := ⋯ }

noncomputable def SaxlCounterexamples.EveryBase.firstVectorOrbitColour (S : EveryBaseSeed) (tail : ℕ) : RegularTupleColour S tail → VectorOrbitColour S

Project a regular-tuple colour to the orbit colour of its first vector.

Equations

• SaxlCounterexamples.EveryBase.firstVectorOrbitColour S tail = Quotient.lift (fun (x : SaxlCounterexamples.EveryBase.RegularTuple S tail) => ⟦↑x 0⟧) ⋯

theorem SaxlCounterexamples.EveryBase.firstVectorOrbitColour_regularTupleColour (S : EveryBaseSeed) (tail : ℕ) (x : Fin (tail + 1) → S.V) (hx : Saxl.IsBaseTuple S.H S.V x) : firstVectorOrbitColour S tail (regularTupleColour S tail x) = ⟦x 0⟧

noncomputable def SaxlCounterexamples.EveryBase.quotientBaseArrayColours (S : EveryBaseSeed) (tail : ℕ) : BaseArrayColours S tail

Canonical finite tuple/vector orbit colours used by the profile argument.

Equations

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

Exact tuple size and the affine successor bridge

def SaxlCounterexamples.EveryBase.ExactTupleBaseSize (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] (n : ℕ) : Prop

A technically convenient strengthening of Saxl.ExactBaseSize: smaller ordered tuples are excluded even before imposing injectivity.

Equations

• SaxlCounterexamples.EveryBase.ExactTupleBaseSize G X n = ((∃ (x : Fin n → X), Saxl.IsBaseTuple G X x) ∧ ∀ m < n, ¬∃ (x : Fin m → X), Saxl.IsBaseTuple G X x)

theorem SaxlCounterexamples.EveryBase.isBaseTuple_injective_of_no_predecessor {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {n : ℕ} (x : Fin (n + 1) → X) (hbase : Saxl.IsBaseTuple G X x) (hprev : ¬∃ (y : Fin n → X), Saxl.IsBaseTuple G X y) : Function.Injective x

theorem SaxlCounterexamples.EveryBase.exactBaseSize_of_exactTupleBaseSize {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {n : ℕ} (h : ExactTupleBaseSize G X n) : Saxl.ExactBaseSize G X n

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.linear_exactTupleBaseSize {S : EveryBaseSeed} [Nontrivial S.H] (T : RegularTupleColourTower S) (n : ℕ) (hcard : ∀ m < n, T.card m < T.card n) : ExactTupleBaseSize (T.LinearGroup n) (T.LinearSpace n) (n + 1)

theorem SaxlCounterexamples.EveryBase.RegularTupleColourTower.linear_exactTupleBaseSize_of_seed {S : EveryBaseSeed} [Nontrivial S.H] [Nontrivial S.V] (T : RegularTupleColourTower S) (n : ℕ) : ExactTupleBaseSize (T.LinearGroup n) (T.LinearSpace n) (n + 1)

theorem SaxlCounterexamples.EveryBase.affine_exactTupleBaseSize_succ (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] {n : ℕ} (hn : 0 < n) (h : ExactTupleBaseSize H V n) : ExactTupleBaseSize (Saxl.AffineGroup H V) V (n + 1)

theorem SaxlCounterexamples.EveryBase.affine_exactBaseSize_succ (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] {n : ℕ} (hn : 0 < n) (h : ExactTupleBaseSize H V n) : Saxl.ExactBaseSize (Saxl.AffineGroup H V) V (n + 1)