Shelah's bound for the Hales--Jewett numbers

Shelah's proof of the Hales--Jewett theorem, by induction on the alphabet.

To pass from α to Option α, fix a letter a₀ of α. Combinatorics.Subspace.exists_insensitive gives a subspace on which the color of a word does not change when a none is replaced by some a₀. On this subspace the coloring is determined by the words over α, so a monochromatic line over α in its parameter cube is also monochromatic at none.

The subspace is built dimension by dimension. Each dimension is a line in a block of new coordinates, given by Combinatorics.Line.exists_map_eq_of_card_le, whose points at the two letters have the same color for every choice of the other coordinates.

Main definitions

• Combinatorics.Subspace.insensitiveBound: the dimension of the cube in Combinatorics.Subspace.exists_insensitive.
• Combinatorics.Line.shelahBound: Shelah's bound for the Hales--Jewett numbers.

Main results

• Combinatorics.Subspace.exists_insensitive: in a cube of dimension insensitiveBound, every coloring is insensitive to two given letters on a subspace.
• Combinatorics.Line.exists_mono_of_card_eq_shelahBound: the Hales--Jewett theorem in dimension shelahBound.
• Combinatorics.Line.exists_mono_of_shelahBound_le: the Hales--Jewett theorem in every dimension at least shelahBound, over a nonempty alphabet.

References

• S. Shelah, Primitive recursive bounds for van der Waerden numbers, J. Amer. Math. Soc. 1 (1988), 683--697.

def Combinatorics.Subspace.insensitiveBound (k : ℕ) : ℕ → ℕ → ℕ

A dimension in which every coloring with r colors of the words over k letters is insensitive to two given letters on an n-dimensional subspace. Each dimension of the subspace takes a block of as many coordinates as there are colorings of the words on the earlier blocks.

Equations

• Combinatorics.Subspace.insensitiveBound k 0 x✝ = 0
• Combinatorics.Subspace.insensitiveBound k n.succ x✝ = Combinatorics.Subspace.insensitiveBound k n (x✝ ^ k) + x✝ ^ k ^ Combinatorics.Subspace.insensitiveBound k n (x✝ ^ k)

theorem Combinatorics.Subspace.exists_insensitive (α : Type) [Finite α] (a b : α) (η : Type) [Finite η] (κ : Type) [Finite κ] : ∃ (ι : Type) (x : Fintype ι), Fintype.card ι = insensitiveBound (Nat.card α) (Nat.card η) (Nat.card κ) ∧ ∀ (C : (ι → α) → κ), ∃ (V : Subspace η α ι), ∀ (x y : η → α), (∀ (e : η), x e = y e ∨ x e = a ∧ y e = b) → C (↑V x) = C (↑V y)

In a cube of dimension insensitiveBound, every coloring is insensitive to the letters a and b on some η-dimensional subspace: replacing a by b in any coordinates of a point of the subspace does not change its color.

def Combinatorics.Line.shelahBound : ℕ → ℕ → ℕ

Shelah's bound for the Hales--Jewett number of k letters and r colors: the dimension of a cube in which every coloring is insensitive to two letters on a subspace whose dimension is the bound for k - 1 letters.

Equations

• Combinatorics.Line.shelahBound 0 x✝ = min x✝ 1
• Combinatorics.Line.shelahBound 1 x✝ = 1
• Combinatorics.Line.shelahBound k.succ.succ x✝ = Combinatorics.Subspace.insensitiveBound (k + 2) (Combinatorics.Line.shelahBound (k + 1) x✝) x✝

theorem Combinatorics.Line.exists_mono_of_card_eq_shelahBound {α : Type u_1} {κ : Type u_2} {ι : Type u_3} [Fintype α] [Fintype κ] [Fintype ι] (h : Fintype.card ι = shelahBound (Fintype.card α) (Fintype.card κ)) (C : (ι → α) → κ) : ∃ (l : Line α ι), IsMono C l

The Hales--Jewett theorem with Shelah's bound: every coloring of the words over α indexed by a type of cardinality shelahBound (card α) (card κ) has a monochromatic line.

theorem Combinatorics.Line.exists_mono_of_shelahBound_le {α : Type u_1} {κ : Type u_2} {ι : Type u_3} [Fintype α] [Fintype κ] [Fintype ι] [Nonempty α] (h : shelahBound (Fintype.card α) (Fintype.card κ) ≤ Fintype.card ι) (C : (ι → α) → κ) : ∃ (l : Line α ι), IsMono C l

The Hales--Jewett theorem with Shelah's bound: over a nonempty alphabet α, every coloring of the words indexed by a type of cardinality at least shelahBound (card α) (card κ) has a monochromatic line.