Countable-family diagonal infinite Ramsey on ℕ

This file derives the countable-family ("eventually homogeneous for every coloring") form of infinite Ramsey from the single-coloring lemma infinite_ramsey_nat_arity, by diagonalizing a descending chain of order-embeddings — one homogenization step per coloring.

This is the pure combinatorial residual consumed by MorleyHanfExtractionTail (the cheap route of the tail-weakened Morley–Hanf extraction; see InfinitaryLogic/Conditional/MorleyHanfTransfer.lean).

theorem infinite_ramsey_nat_family (c : ℕ → (n : ℕ) × (Fin n ↪o ℕ → Bool)) : ∃ (g : ℕ ↪o ℕ), ∀ (i : ℕ), ∃ (N : ℕ), ∀ (u v : Fin (c i).fst ↪o ℕ), (∀ (k : Fin (c i).fst), N ≤ u k) → (∀ (k : Fin (c i).fst), N ≤ v k) → (c i).snd (RelEmbedding.trans u g) = (c i).snd (RelEmbedding.trans v g)

Countable-family diagonal infinite Ramsey on ℕ.

Given countably many finite-arity Bool colorings c : ℕ → Σ n, (Fin n ↪o ℕ) → Bool, there is a single order embedding g : ℕ ↪o ℕ and, for each coloring c i, a cutoff N beyond which c i is constant on all n-tuples u.trans g whose underlying indices are all ≥ N.

Diagonalization of infinite_ramsey_nat_arity: build a descending chain of embeddings p 0 ⊇ p 1 ⊇ … (in the sense Set.range (p (k+1)) ⊆ Set.range (p k)), where p (k+1) homogenizes coloring c k; then read off a strictly increasing diagonal g with g j ∈ Set.range (p j). Every order-embedding ℕ ↪o ℕ has unbounded range, so the diagonal is well-defined and strictly increasing, and a deep tuple u (indices ≥ i+1) has u.trans g landing in Set.range (p (i+1)), where c i is constant.