Infinite Ramsey on ℕ for finite-arity Bool colorings

This file isolates the pure combinatorial residual consumed by the tail-weakened Morley–Hanf extraction (MorleyHanfExtractionTail). The statement audit (2026-06-14) established that the tail residual asks only for a countable sequence that is tail-indiscernible for countably many finite-arity Bool colorings. That is an infinite Ramsey fact on ℕ — not an ℶ_{ω₁} Erdős–Rado / partition-calculus theorem. (The ℶ_{ω₁} beth schedule is a strictly stronger statement, needed only for full/uncountable indiscernibility; it is not consumed by this bridge. See InfinitaryLogic/Conditional/MorleyHanfTransfer.lean.)

Main statement

• infinite_ramsey_nat_arity — single-coloring n-ary infinite Ramsey on ℕ: a Bool coloring of strictly-increasing n-tuples of ℕ has an order-embedding f : ℕ ↪o ℕ whose image is monochromatic. This is the genuine new combinatorics (to be proved by induction on the arity n, generalizing infinite_ramsey_unary_nat/infinite_ramsey_pair_nat).

The countable-family diagonal form infinite_ramsey_nat_family lives in InfiniteRamseyFamily.lean and is derived from this single-coloring lemma. The model-side extraction (MorleyHanfExtractionTail) is proved against the family form, verifying that the cheap route discharges the conditional surface.

theorem infinite_ramsey_nat_arity (n : ℕ) (c : Fin n ↪o ℕ → Bool) : ∃ (f : ℕ ↪o ℕ), ∀ (u v : Fin n ↪o ℕ), c (RelEmbedding.trans u f) = c (RelEmbedding.trans v f)

Single-coloring finite-arity infinite Ramsey on ℕ.

For any Bool coloring c of strictly-increasing n-tuples of ℕ (presented as order embeddings Fin n ↪o ℕ), there is an order embedding f : ℕ ↪o ℕ such that c is constant on all n-tuples drawn from the range of f (every such tuple has the form u.trans f).

This is the genuine combinatorial residual of the cheap Morley–Hanf route: it generalizes the unary (infinite_ramsey_unary_nat) and pair (infinite_ramsey_pair_nat) cases in ErdosRado.lean to all finite arities, and is provable by induction on n. It does not require any beth/partition-calculus machinery.