The Nash-Williams theorem

The Nash-Williams theorem: a 2-coloring (equivalently, a subset S) of a front F on M admits a monochromatic sub-front, i.e. an infinite X ⊆ M with F | X ⊆ S or F | X ∩ S = ∅. Here F | X is shrink F (M ∘ e) for the increasing enumeration M ∘ e of X.

This file stages the development:

• IsFront.nash_williams — the base 2-color/subset theorem, by recursion on the rank of the front.
• IsFront.nash_williams_fin — the finite-color version, by induction on colors and color-blurring.
• Front.ramsey_seq_of_nashWilliams — the finite-arity infinite Ramsey theorem, obtained by instantiating the finite-color version at the uniform front [M]^k (powK).

Supporting lemmas:

• Front.shrink_shrink — restricting twice collapses to a single restriction.
• Front.shrink_powK — the restriction of a uniform front is the uniform front on the subset.

Two proofs of infinite Ramsey

Front.ramsey_seq_of_nashWilliams re-derives infinite_ramsey_seq from the Nash-Williams theorem. It is deliberately kept alongside the direct iterated-pigeonhole proof in NashWilliams.Combinatorics.Ramsey.Infinite, and the two are independent: this file does not import that one. The only lemmas the two developments share are the generic helpers in NashWilliams.Data.

Stage 1: the base 2-color / subset theorem

theorem Front.IsFront.nash_williams {F : Set (List ℕ)} {M : ℕ → ℕ} (hF : IsFront F M) (S : Set (List ℕ)) : ∃ X ⊆ Set.range M, X.Infinite ∧ (shrinkOn F X ⊆ S ∨ Disjoint (shrinkOn F X) S)

The Nash-Williams theorem (subset form). For a front F on M and any subset S, there is an infinite subset X ⊆ range M on which the restricted front shrinkOn F X (the survey's F ↾ X) is entirely inside S or entirely outside S.

The carrier is stated as a set X; its strictly monotone enumeration N (with Set.range N = X, so that shrinkOn F X = shrink F N) is recovered through Set.Infinite.exists_strictMono_range.

Proved by transfinite recursion on hF.rank (the ray recursion).

Stage 2: the finite-color version

theorem Front.IsFront.nash_williams_fin {F : Set (List ℕ)} {M : ℕ → ℕ} (hF : IsFront F M) {κ : Type u_1} [Finite κ] (c : List ℕ → κ) : ∃ (e : ℕ → ℕ), StrictMono e ∧ ∃ (col : κ), ∀ s ∈ shrink F (M ∘ e), c s = col

Finite-color Nash-Williams. For a front F on M and a coloring c of finite lists by a finite palette κ, there is an infinite subset M ∘ e ⊆ M on which c is constant over the restricted front.

Obtained from IsFront.nash_williams by induction on the palette with color-blurring: split off one color as a subset S, apply the base theorem, and recurse into the smaller palette on the disjoint side (a front via shrink_isFront), composing restrictions with shrink_shrink.

Stage 3: the finite-arity infinite Ramsey theorem

theorem Front.ramsey_seq_of_nashWilliams {κ : Type u_1} [Finite κ] (k : ℕ) (c : Finset ℕ → κ) : ∃ (e : ℕ → ℕ), StrictMono e ∧ ∃ (col : κ), ∀ (t : Finset ℕ), ↑t ⊆ Set.range e → t.card = k → c t = col

Infinite Ramsey at arbitrary finite arity, via Nash-Williams. A finite coloring c of the size-k subsets of ℕ admits a strictly monotone e and a color col such that every size-k subset of range e has color col.

Obtained by applying IsFront.nash_williams_fin to the uniform front [ℕ]^k (powK id k) with the list-coloring s ↦ c s.toFinset, rewriting the restricted front via shrink_powK, and bridging the size-k Finsets with their sorted lists. This matches infinite_ramsey_seq and re-derives it from the Nash-Williams theorem.