Shelah's bound is below the fifth level of the Ackermann function

The recursion Combinatorics.Subspace.insensitiveBound replaces r colors by r ^ k colors, so after j steps the number of colors is r ^ k ^ j. Each step adds a term that is doubly exponential in the earlier ones, so insensitiveBound k n r is at most ack 4 at a linear function of n. Shelah's bound applies insensitiveBound once for each letter, so it is below ack 5 at a linear function of the number of letters and of colors.

Main results

• Combinatorics.Subspace.insensitiveBound_le_ack: insensitiveBound k n r ≤ ack 4 (5 * n + k + r + 2).
• Combinatorics.Line.shelahBound_lt_ack: shelahBound k r < ack 5 (2 * k + r).
• Combinatorics.Line.exists_mono_of_ack_le: the Hales--Jewett theorem in every dimension at least ack 5 (2 * k + r), for k letters and r colors.

theorem Combinatorics.Subspace.insensitiveBound_le_ack (k n r : ℕ) : insensitiveBound k n r ≤ ack 4 (5 * n + k + r + 2)

The dimension insensitiveBound k n r is at most the fourth level of the Ackermann function at a linear function of n.

theorem Combinatorics.Line.shelahBound_lt_ack (k r : ℕ) : shelahBound k r < ack 5 (2 * k + r)

Shelah's bound is below the fifth level of the Ackermann function.

theorem Combinatorics.Line.exists_mono_of_ack_le {α : Type u_1} {κ : Type u_2} {ι : Type u_3} [Fintype α] [Fintype κ] [Fintype ι] [Nonempty α] (h : ack 5 (2 * Fintype.card α + Fintype.card κ) ≤ Fintype.card ι) (C : (ι → α) → κ) : ∃ (l : Line α ι), IsMono C l

The Hales--Jewett theorem with the Ackermann function as the bound: over a nonempty alphabet α, every coloring of the words indexed by ι has a monochromatic line if card ι is at least ack 5 (2 * card α + card κ).