The finite-color interval lemma used for termination

The operation colors in the proof of the Flag Decomposition Lemma need not decrease. The combinatorial input instead finds an interval with many occurrences of its least color. The required number of occurrences may depend arbitrarily on the first index of the interval.

def EGZ.HasColorInterval (χ h : ℕ → ℕ) (a b l : ℕ) : Prop

An interval on which l is a lower bound for the colors and occurs at least h a times. Indices and colors start at zero.

Equations

• EGZ.HasColorInterval χ h a b l = (a ≤ b ∧ (∀ i ∈ Finset.Icc a b, l ≤ χ i) ∧ h a ≤ {i ∈ Finset.Icc a b | χ i = l}.card)

theorem EGZ.HasColorInterval.congr {χ ψ h : ℕ → ℕ} {a b l : ℕ} (hχ : HasColorInterval χ h a b l) (heq : ∀ i ∈ Finset.Icc a b, χ i = ψ i) : HasColorInterval ψ h a b l

theorem EGZ.exists_color_interval (k : ℕ) (h χ : ℕ → ℕ) (hχ : ∀ (i : ℕ), χ i < k) : ∃ (a : ℕ) (b : ℕ), ∃ l < k, HasColorInterval χ h a b l

Infinite version of the interval lemma: take the least color whose fiber is infinite, then start beyond every occurrence of a smaller color.

def EGZ.extendColoring {n k : ℕ} (χ : Fin n → Fin k) (i : ℕ) : ℕ

Extend a coloring of a finite initial segment by zero. Only values in the original segment will occur in the conclusions below.

Equations

• EGZ.extendColoring χ i = if hi : i < n then ↑(χ ⟨i, hi⟩) else 0

theorem EGZ.exists_finite_color_interval_bound (k : ℕ) (h : ℕ → ℕ) : ∃ (N : ℕ), ∀ (χ : Fin N → Fin k), ∃ (a : ℕ) (b : ℕ) (l : ℕ), b < N ∧ HasColorInterval (extendColoring χ) h a b l

The finite-color interval claim in the proof of the Flag Decomposition Lemma. The bound is uniform over all colorings and h need not be monotone. Kőnig's lemma turns arbitrarily long bad colorings into an infinite bad coloring, contradicting exists_color_interval.

theorem EGZ.exists_color_interval_bound (k : ℕ) (h : ℕ → ℕ) : ∃ (N : ℕ), ∀ (χ : ℕ → ℕ), (∀ i < N, χ i < k) → ∃ (a : ℕ) (b : ℕ) (l : ℕ), b < N ∧ l < k ∧ HasColorInterval χ h a b l

A formulation for operation sequences: among the first N operations, there is an interval whose smallest color occurs as often as prescribed by the interval's starting index. Only these first N colors are constrained.