The abstract every-base-size construction

This module proves the base-array orbit-profile mechanism, the displayed sumset obstruction, and the abstract exact-base-size counterexample theorem. All seed and finite-colour hypotheses are exposed by the imported structures.

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.LinearTop {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) : Type (max (max u_2 u_4) u_4)

The permutation-wreath group associated to a seed and colour system.

Equations

• SaxlCounterexamples.EveryBase.LinearTop S K = Saxl.PermWreath S.H (Equiv.Perm K.C) K.C

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.ProductModule {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) : Type (max u_4 u_3)

The product of seed modules indexed by tuple colours.

Equations

• SaxlCounterexamples.EveryBase.ProductModule S K = (K.C → S.V)

def SaxlCounterexamples.EveryBase.neighbourSet {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) : Set (ProductModule S K)

The generalized affine neighborhood of zero.

Equations

• SaxlCounterexamples.EveryBase.neighbourSet S K = Saxl.generalizedAffineKernelSet (SaxlCounterexamples.EveryBase.LinearTop S K) (SaxlCounterexamples.EveryBase.ProductModule S K) tail

def SaxlCounterexamples.EveryBase.columnOf {tail : ℕ} {S : EveryBaseSeed} {tail✝ : ℕ} {K : BaseArrayColours S tail✝} (rows : Fin (tail + 1) → ProductModule S K) (c : K.C) : Fin (tail + 1) → S.V

Read one colour-indexed column from an array of product-module rows.

Equations

• SaxlCounterexamples.EveryBase.columnOf rows c j = rows j c

def SaxlCounterexamples.EveryBase.tupleColourWord {tail : ℕ} {S : EveryBaseSeed} (K : BaseArrayColours S tail) (rows : Fin (tail + 1) → ProductModule S K) : K.C → K.C

The word of tuple colours determined by an array of rows.

Equations

• SaxlCounterexamples.EveryBase.tupleColourWord K rows c = K.tupleCode.colour (SaxlCounterexamples.EveryBase.columnOf rows c)

theorem SaxlCounterexamples.EveryBase.neighbour_colourWord_bijective {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) {x : ProductModule S K} (hx : x ∈ neighbourSet S K) : ∃ (rows : Fin (tail + 1) → ProductModule S K), rows 0 = x ∧ Saxl.IsBaseTuple (LinearTop S K) (ProductModule S K) rows ∧ Function.Bijective (tupleColourWord K rows)

def SaxlCounterexamples.EveryBase.orbitProfile {tail : ℕ} {S : EveryBaseSeed} (K : BaseArrayColours S tail) (x : ProductModule S K) : Multiset K.D

The multiset of vector-orbit colours of a product-module element.

Equations

• SaxlCounterexamples.EveryBase.orbitProfile K x = Multiset.map (fun (c : K.C) => K.vectorCode.colour (x c)) Finset.univ.val

def SaxlCounterexamples.EveryBase.referenceProfile {tail : ℕ} {S : EveryBaseSeed} (K : BaseArrayColours S tail) : Multiset K.D

The reference multiset obtained from the first-colour projection.

Equations

• SaxlCounterexamples.EveryBase.referenceProfile K = Multiset.map K.firstColour Finset.univ.val

theorem SaxlCounterexamples.EveryBase.profile_eq_reference_of_neighbour {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) {x : ProductModule S K} (hx : x ∈ neighbourSet S K) : orbitProfile K x = referenceProfile K

theorem SaxlCounterexamples.EveryBase.value_eq_at_of_profile_eq_of_eq_off {C : Type u_1} {D : Type u_2} [Fintype C] (f g : C → D) (c0 : C) (hprofile : Multiset.map f Finset.univ.val = Multiset.map g Finset.univ.val) (hoff : ∀ (c : C), c ≠ c0 → f c = g c) : f c0 = g c0

theorem SaxlCounterexamples.EveryBase.neighbour_orbit_at_of_eq_off {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) {x y : ProductModule S K} (hx : x ∈ neighbourSet S K) (hy : y ∈ neighbourSet S K) (c0 : K.C) (hoff : ∀ (c : K.C), c ≠ c0 → x c = y c) : ∃ (h : S.H), h • x c0 = y c0

The displayed bad vector and the abstract obstruction

theorem SaxlCounterexamples.EveryBase.add_self_eq_zero_of_binaryModule (S : EveryBaseSeed) (v : S.V) : v + v = 0

theorem SaxlCounterexamples.EveryBase.eq_of_add_eq_zero_binaryModule (S : EveryBaseSeed) {x y : S.V} (h : x + y = 0) : x = y

def SaxlCounterexamples.EveryBase.badVector {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) (c0 : K.C) : ProductModule S K

The product vector supported at one colour with value S.u.

Equations

• SaxlCounterexamples.EveryBase.badVector S K c0 = Function.update (fun (x : K.C) => 0) c0 S.u

@[simp]

theorem SaxlCounterexamples.EveryBase.badVector_at {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) (c0 : K.C) : badVector S K c0 c0 = S.u

theorem SaxlCounterexamples.EveryBase.badVector_away {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) {c c0 : K.C} (hne : c ≠ c0) : badVector S K c0 c = 0

theorem SaxlCounterexamples.EveryBase.badVector_not_mem_neighbourSumset {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) (c0 : K.C) : badVector S K c0 ∉ neighbourSet S K + neighbourSet S K

Paper Lemma 6.3 at the abstract level. Its hypotheses consist only of finite tuple-orbit codes and the explicit binary cycle obstruction stored in EveryBaseSeed; neither irreducibility nor an external base-size theorem is assumed.

theorem SaxlCounterexamples.EveryBase.abstractCoreObstruction {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) (c0 : K.C) : ¬Saxl.HasCommonNeighbour (ProductModule S K) (Saxl.GeneralizedAdjacent (Saxl.AffineGroup (LinearTop S K) (ProductModule S K)) (ProductModule S K) tail) 0 (badVector S K c0)

The abstract no-common-neighbour conclusion, obtained from the proved generalized affine sumset criterion.

theorem SaxlCounterexamples.EveryBase.abstractCoreFamily {tail : ℕ} (S : EveryBaseSeed) (K : BaseArrayColours S tail) (c0 : K.C) (hlinear : ExactTupleBaseSize (LinearTop S K) (ProductModule S K) (tail + 1)) : Saxl.ExactBaseSize (Saxl.AffineGroup (LinearTop S K) (ProductModule S K)) (ProductModule S K) (tail + 2) ∧ ¬Saxl.HasCommonNeighbour (ProductModule S K) (Saxl.GeneralizedAdjacent (Saxl.AffineGroup (LinearTop S K) (ProductModule S K)) (ProductModule S K) tail) 0 (badVector S K c0)

Paper Theorem 6.4 at the abstract boundary. Exact linear tuple-base size is an explicit hypothesis, normally discharged from a RegularTupleColourTower by linear_exactTupleBaseSize; no literature base-size formula is hidden here.