Finite-arity Erdős–Rado: the induction scaffold

The finite-arity induction toward the bounded finite-arity Erdős–Rado theorem: the cardinal ladder finiteERBound (with its arithmetic validated against the beth scale), the validated API (FiniteArityHomogeneousUpTo, FiniteArityErdosRadoBounded), the easy arities 0, 1, 2 (finiteArityHomogeneousUpTo_zero/_one/_two), the last consuming the proven generalized pair theorem pairErdosRado_general_of_large, the hard n → n+1 induction step finiteArityHomogeneousUpTo_step (end-homogenization via exists_endHomogeneous_of_large + the induced top-arity color fed to the IH), and the assembled bounded theorem finiteArityErdosRadoBounded with its ℶ₁ instance.

The previously envisaged continuation FiniteArityErdosRadoBounded ℶ₁ → FiniteArityErdosRadoOmega1 ℶ₁ → morley_hanf is DEAD at the first arrow (statement audit 2026-07-07): the all-arity FiniteArityErdosRadoOmega1 is refutable in ZFC — it is the Erdős-cardinal partition relation ℶ_ω₁ → (ω₁)^{<ω}, whose order-type-ω weakening already requires the inaccessible κ(ω) ≤ ℶ_ω₁ (see the fences on FiniteArityErdosRadoOmega1 and PureColoringHypothesis). The obstruction the earlier docstring flagged (per-N outputs cannot be iterated; an ω-schedule of passes needs an infinite descending sequence of ladder levels) is that refutation's shadow. The bounded theorem here is instead the per-stage approximation supply of the classical Morley/Hanf template route (Marker §5.2): instantiating the color/output parameter at κ := ℶ_α gives ℶ_α⁺-sized homogeneous-up-to-N suborders for the consistency-property certification, with the indiscernible sequence materializing in the constructed model, not in the source.

The ladder

Level N of finiteERBound κ is enough source to homogenize all arities ≤ N with output κ⁺. The recursion level (n+2) = succ (2 ^ level (n+1)) is sized so that generalized pair ER at color bound finiteERBound κ (n+1), applied to a source of size finiteERBound κ (n+2), outputs a suborder of size succ (finiteERBound κ (n+1)) — ample source for stage n+1. At κ = ℶ₁ every level sits below ℶ_{ω₁} (finiteERBound_le_beth_omega1): each ladder step succ ∘ (2 ^ ·) is absorbed by two beth steps (finiteERBound_beth_one_le).

The cardinal ladder

Ladder lemmas

The API

Small utilities: arity-0/1/2 order embeddings and no-max output

instance instSubsingletonOrderEmbeddingFinOfNatNat_leanPool {I : Type u_1} [LinearOrder I] : Subsingleton (Fin 0 ↪o I)

Tuple factoring and decomposition

theorem exists_orderEmbedding_factor {J : Type u_1} {I : Type u_2} [LinearOrder J] [LinearOrder I] {m : ℕ} (f : J ↪o I) (t : Fin m ↪o I) (ht : ∀ (k : Fin m), t k ∈ Set.range ⇑f) : ∃ (s : Fin m ↪o J), RelEmbedding.trans s f = t

Factor a finite tuple through an order embedding: a tuple whose values lie in the range of f : J ↪o I is the f-image of a (unique) tuple in J. The order structure transports back through f.lt_iff_lt, so the preimage tuple is again an order embedding.

The easy arities: 0, 1, 2

The induction step

The bounded finite-arity theorem

theorem finiteArityHomogeneousUpTo_beth_stage (α : Ordinal.{0}) (N : ℕ) {I : Type} [LinearOrder I] [WellFoundedLT I] (hI : Cardinal.beth (α + ↑(2 * N + 2)) ≤ Cardinal.mk I) (C : ℕ → Type) (hC : ∀ (n : ℕ), Cardinal.mk (C n) ≤ Cardinal.beth α) (c : (n : ℕ) → Fin n ↪o I → C n) : ∃ (e : (Order.succ (Cardinal.beth α)).ord.ToType ↪o I), ∀ n ≤ N, ∀ (t t' : Fin n ↪o I), (∀ (k : Fin n), t k ∈ Set.range ⇑e) → (∀ (k : Fin n), t' k ∈ Set.range ⇑e) → c n t = c n t'

The Marker-stage Erdős–Rado supply: from a source of size ≥ ℶ_{α + 2N + 2} and any ℕ-indexed coloring family with color types of size ≤ ℶ_α, one (ℶ_α)⁺-suborder homogeneous for all arities ≤ N simultaneously.

This is the TRUE replacement for the false all-arity jump (FiniteArityErdosRadoOmega1 — refutable in ZFC, see its docstring and PureColoringHypothesis): per-α, per-finite-N approximations, NOT one ω₁-suborder homogeneous for all arities at once. It is exactly the per-stage lemma the classical Morley/Hanf consistency-property schedule consumes [Marker, Lectures on Infinitary Model Theory, §5.2]: for each finite formula/arity budget N and cofinally many α < ω₁, a ℶ_{ω₁}-sized source dominates the demanded ℶ_{α + 2N + 2} (the beth index stays below ω₁), yielding ℶ_α-large approximations of the EM template; the indiscernible sequence itself materializes only in the model built by Model Existence, never in the source.