# The Hales-Jewett theorem #

We prove the Hales-Jewett theorem and deduce Van der Waerden's theorem as a corollary.

The Hales-Jewett theorem is a result in Ramsey theory dealing with combinatorial lines. Given an 'alphabet' α : Type* and a b : α, an example of a combinatorial line in α^5 is { (a, x, x, b, x) | x : α }. See Combinatorics.Line for a precise general definition. The Hales-Jewett theorem states that for any fixed finite types α and κ, there exists a (potentially huge) finite type ι such that whenever ι → α is κ-colored (i.e. for any coloring C : (ι → α) → κ), there exists a monochromatic line. We prove the Hales-Jewett theorem using the idea of color focusing and a product argument. See the proof of Combinatorics.Line.exists_mono_in_high_dimension' for details.

The version of Van der Waerden's theorem in this file states that whenever a commutative monoid M is finitely colored and S is a finite subset, there exists a monochromatic homothetic copy of S. This follows from the Hales-Jewett theorem by considering the map (ι → S) → M sending v to ∑ i : ι, v i, which sends a combinatorial line to a homothetic copy of S.

## Main results #

• Combinatorics.Line.exists_mono_in_high_dimension: the Hales-Jewett theorem.
• Combinatorics.exists_mono_homothetic_copy: a generalization of Van der Waerden's theorem.

## Implementation details #

For convenience, we work directly with finite types instead of natural numbers. That is, we write α, ι, κ for (finite) types where one might traditionally use natural numbers n, H, c. This allows us to work directly with α, Option α, (ι → α) → κ, and ι ⊕ ι' instead of Fin n, Fin (n+1), Fin (c^(n^H)), and Fin (H + H').

## Todo #

• Prove a finitary version of Van der Waerden's theorem (either by compactness or by modifying the current proof).

• One could reformulate the proof of Hales-Jewett to give explicit upper bounds on the number of coordinates needed.

## Tags #

combinatorial line, Ramsey theory, arithmetic progression

### References #

• https://en.wikipedia.org/wiki/Hales%E2%80%93Jewett_theorem
structure Combinatorics.Line (α : Type u_1) (ι : Type u_2) :
Type (max u_1 u_2)

The type of combinatorial lines. A line l : Line α ι in the hypercube ι → α defines a function α → ι → α from α to the hypercube, such that for each coordinate i : ι, the function fun x ↦ l x i is either id or constant. We require lines to be nontrivial in the sense that fun x ↦ l x i is id for at least one i.

Formally, a line is represented by a word l.idxFun : ι → Option α which says whether fun x ↦ l x i is id (corresponding to l.idxFun i = none) or constantly y (corresponding to l.idxFun i = some y).

When α has size 1 there can be many elements of Line α ι defining the same function.

• idxFun : ι

The word representing a combinatorial line. l.idxfun i = none means that l x i = x for all x and l.idxfun i = some y means that l x i = y.

• proper : ∃ (i : ι), self.idxFun i = none

We require combinatorial lines to be nontrivial in the sense that fun x ↦ l x i is id for at least one coordinate i.

Instances For
instance Combinatorics.Line.instCoeFunLineForAll (α : Type u_1) (ι : Type u_2) :
CoeFun () fun (x : ) => αια
Equations
• = { coe := fun (l : ) (x : α) (i : ι) => Option.getD (l.idxFun i) x }
def Combinatorics.Line.IsMono {α : Type u_1} {ι : Type u_2} {κ : Sort u_3} (C : (ια)κ) (l : ) :

A line is monochromatic if all its points are the same color.

Equations
• = ∃ (c : κ), ∀ (x : α), C ((fun (x : α) (i : ι) => Option.getD (l.idxFun i) x) x) = c
Instances For
def Combinatorics.Line.diagonal (α : Type u_1) (ι : Type u_2) [] :

The diagonal line. It is the identity at every coordinate.

Equations
• = { idxFun := fun (x : ι) => none, proper := (_ : ∃ (i : ι), (fun (x : ι) => none) i = none) }
Instances For
instance Combinatorics.Line.instInhabitedLine (α : Type u_1) (ι : Type u_2) [] :
Equations
• = { default := }
structure Combinatorics.Line.AlmostMono {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι)κ) :
Type (max (max u_1 u_2) u_3)

The type of lines that are only one color except possibly at their endpoints.

• line :

The underlying line of an almost monochromatic line, where the coordinate dimension α is extended by an additional symbol none, thought to be marking the endpoint of the line.

• color : κ

The main color of an almost monochromatic line.

• has_color : ∀ (x : α), C ((fun (x : ) (i : ι) => Option.getD (self.line.idxFun i) x) (some x)) = self.color

The proposition that the underlying line of an almost monochromatic line assumes its main color except possibly at the endpoints.

Instances For
instance Combinatorics.Line.instInhabitedAlmostMonoForAllOptionDefault {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [] [] :
Inhabited (Combinatorics.Line.AlmostMono fun (x : ι) => default)
Equations
• Combinatorics.Line.instInhabitedAlmostMonoForAllOptionDefault = { default := { line := default, color := default, has_color := (_ : αdefault = default) } }
structure Combinatorics.Line.ColorFocused {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι)κ) :
Type (max (max u_1 u_2) u_3)

The type of collections of lines such that

• each line is only one color except possibly at its endpoint
• the lines all have the same endpoint
• the colors of the lines are distinct. Used in the proof exists_mono_in_high_dimension.
• lines :

The underlying multiset of almost monochromatic lines of a color-focused collection.

• focus : ι

The common endpoint of the lines in the color-focused collection.

• is_focused : pself.lines, (fun (x : ) (i : ι) => Option.getD (p.line.idxFun i) x) none = self.focus

The proposition that all lines in a color-focused collection have the same endpoint.

• distinct_colors : Multiset.Nodup (Multiset.map Combinatorics.Line.AlmostMono.color self.lines)

The proposition that all lines in a color-focused collection of lines have distinct colors.

Instances For
instance Combinatorics.Line.instInhabitedColorFocused {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι)κ) :
Equations
• One or more equations did not get rendered due to their size.
def Combinatorics.Line.map {α : Type u_1} {α' : Type u_2} {ι : Type u_3} (f : αα') (l : ) :

A function f : α → α' determines a function line α ι → line α' ι. For a coordinate i, l.map f is the identity at i if l is, and constantly f y if l is constantly y at i.

Equations
• = { idxFun := fun (i : ι) => Option.map f (l.idxFun i), proper := (_ : ∃ (i : ι), (fun (i : ι) => Option.map f (l.idxFun i)) i = none) }
Instances For
def Combinatorics.Line.vertical {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (v : ια) (l : ) :

A point in ι → α and a line in ι' → α determine a line in ι ⊕ ι' → α.

Equations
Instances For
def Combinatorics.Line.horizontal {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : ) (v : ι'α) :

A line in ι → α and a point in ι' → α determine a line in ι ⊕ ι' → α.

Equations
Instances For
def Combinatorics.Line.prod {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : ) (l' : ) :

One line in ι → α and one in ι' → α together determine a line in ι ⊕ ι' → α.

Equations
• = { idxFun := Sum.elim l.idxFun l'.idxFun, proper := (_ : ∃ (i : ι ι'), Sum.elim l.idxFun l'.idxFun i = none) }
Instances For
theorem Combinatorics.Line.apply {α : Type u_1} {ι : Type u_2} (l : ) (x : α) :
(fun (x : α) (i : ι) => Option.getD (l.idxFun i) x) x = fun (i : ι) => Option.getD (l.idxFun i) x
theorem Combinatorics.Line.apply_none {α : Type u_1} {ι : Type u_2} (l : ) (x : α) (i : ι) (h : l.idxFun i = none) :
(fun (x : α) (i : ι) => Option.getD (l.idxFun i) x) x i = x
theorem Combinatorics.Line.apply_of_ne_none {α : Type u_1} {ι : Type u_2} (l : ) (x : α) (i : ι) (h : l.idxFun i none) :
some ((fun (x : α) (i : ι) => Option.getD (l.idxFun i) x) x i) = l.idxFun i
@[simp]
theorem Combinatorics.Line.map_apply {α : Type u_1} {α' : Type u_2} {ι : Type u_3} (f : αα') (l : ) (x : α) :
(fun (x : α') (i : ι) => Option.getD (().idxFun i) x) (f x) = f (fun (x : α) (i : ι) => Option.getD (l.idxFun i) x) x
@[simp]
theorem Combinatorics.Line.vertical_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (v : ια) (l : ) (x : α) :
(fun (x : α) (i : ι ι') => Option.getD (.idxFun i) x) x = Sum.elim v ((fun (x : α) (i : ι') => Option.getD (l.idxFun i) x) x)
@[simp]
theorem Combinatorics.Line.horizontal_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : ) (v : ι'α) (x : α) :
(fun (x : α) (i : ι ι') => Option.getD (.idxFun i) x) x = Sum.elim ((fun (x : α) (i : ι) => Option.getD (l.idxFun i) x) x) v
@[simp]
theorem Combinatorics.Line.prod_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : ) (l' : ) (x : α) :
(fun (x : α) (i : ι ι') => Option.getD (().idxFun i) x) x = Sum.elim ((fun (x : α) (i : ι) => Option.getD (l.idxFun i) x) x) ((fun (x : α) (i : ι') => Option.getD (l'.idxFun i) x) x)
@[simp]
theorem Combinatorics.Line.diagonal_apply {α : Type u_1} {ι : Type u_2} [] (x : α) :
(fun (x : α) (i : ι) => Option.getD (.idxFun i) x) x = fun (x_1 : ι) => x
theorem Combinatorics.Line.exists_mono_in_high_dimension (α : Type u) [] (κ : Type v) [] :
∃ (ι : Type) (x : ), ∀ (C : (ια)κ), ∃ (l : ),

The Hales-Jewett theorem: for any finite types α and κ, there exists a finite type ι such that whenever the hypercube ι → α is κ-colored, there is a monochromatic combinatorial line.

theorem Combinatorics.exists_mono_homothetic_copy {M : Type u_1} {κ : Type u_2} [] (S : ) [] (C : Mκ) :
∃ a > 0, ∃ (b : M) (c : κ), sS, C (a s + b) = c

A generalization of Van der Waerden's theorem: if M is a finitely colored commutative monoid, and S is a finite subset, then there exists a monochromatic homothetic copy of S.