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

noncomputable def finiteERBound (κ : Cardinal.{0}) : ℕ → Cardinal.{0}

Source-size ladder; level N is enough source to homogenize all arities ≤ N with output κ⁺. Level 0/1 = κ⁺ (nothing to do / point pigeonhole); level n+2 = succ (2 ^ level (n+1)), 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.

Equations

• finiteERBound κ 0 = Order.succ κ
• finiteERBound κ 1 = Order.succ κ
• finiteERBound κ n.succ.succ = Order.succ (2 ^ finiteERBound κ (n + 1))

Ladder lemmas

theorem finiteERBound_zero (κ : Cardinal.{0}) : finiteERBound κ 0 = Order.succ κ

Ladder level 0 is κ⁺.

theorem finiteERBound_one (κ : Cardinal.{0}) : finiteERBound κ 1 = Order.succ κ

Ladder level 1 is κ⁺.

theorem finiteERBound_succ_succ (κ : Cardinal.{0}) (n : ℕ) : finiteERBound κ (n + 2) = Order.succ (2 ^ finiteERBound κ (n + 1))

The ladder recursion, as an equality: level n+2 is exactly the generalized-pair-ER source bound for color bound finiteERBound κ (n+1).

theorem succ_le_finiteERBound (κ : Cardinal.{0}) (n : ℕ) : Order.succ κ ≤ finiteERBound κ n

Every ladder level dominates κ⁺.

theorem finiteERBound_mono (κ : Cardinal.{0}) : Monotone (finiteERBound κ)

The ladder is monotone in the arity.

theorem pair_source_le_finiteERBound (κ : Cardinal.{0}) (n : ℕ) : Order.succ (2 ^ κ) ≤ finiteERBound κ (n + 2)

Every ladder level of index ≥ 2 dominates the generalized pair-ER source bound succ (2 ^ κ) — this is what lets the arity-2 theorem consume any level ≥ 2.

theorem aleph0_le_beth_one : Cardinal.aleph0 ≤ Cardinal.beth 1

ℵ₀ ≤ ℶ₁ — the infinite-cardinal hypothesis for the ladder at the Morley–Hanf color bound.

theorem finiteERBound_beth_one_le (n : ℕ) : finiteERBound (Cardinal.beth 1) n ≤ Cardinal.beth ↑(2 * n + 2)

At κ = ℶ₁, ladder level n is bounded by ℶ_{2n+2}: each ladder step succ ∘ (2 ^ ·) costs strictly more than one beth step (the inner succ), but two beth steps absorb it.

theorem finiteERBound_lt_beth_omega1 (n : ℕ) : finiteERBound (Cardinal.beth 1) n < Cardinal.beth (Ordinal.omega 1)

At κ = ℶ₁, every ladder level is strictly below ℶ_{ω₁} — the source size the Morley–Hanf chain supplies dominates every finite stage.

theorem finiteERBound_le_beth_omega1 (n : ℕ) : finiteERBound (Cardinal.beth 1) n ≤ Cardinal.beth (Ordinal.omega 1)

At κ = ℶ₁, every ladder level is at most ℶ_{ω₁} (the form consumed when feeding a ℶ_{ω₁}-sized source into a finite ladder stage).

theorem finiteERBound_beth_le (α : Ordinal.{0}) (N : ℕ) : finiteERBound (Cardinal.beth α) N ≤ Cardinal.beth (α + ↑(2 * N + 2))

The general beth-scheduled ladder bound: at κ = ℶ_α, ladder level N is bounded by ℶ_{α + 2N + 2} — each ladder step succ ∘ (2 ^ ·) is absorbed by two beth steps, uniformly in the base index α (the α = 1 bound above is the sharper special case; this one is loose on purpose — the goal is a reusable scheduled estimate, not sharpness). This is the arithmetic behind the Marker-style consistency-property schedule: per-arity Erdős–Rado approximations at every base ℶ_α, α < ω₁, all fed from a ℶ_{ω₁}-sized source.

The API

def FiniteArityHomogeneousUpTo (κ : Cardinal.{0}) (N : ℕ) : Prop

Homogeneity up to arity N: the exact statement the finite-arity induction will prove. Any well-ordered source of size ≥ finiteERBound κ N and any ℕ-indexed family of colorings with color types of size ≤ κ admit a single κ⁺-suborder homogeneous for all arities ≤ N simultaneously. The family is ℕ-indexed from the start, per the design note that the all-arity theorem must recurse internally over arity, not iterate over the external sequence.

Equations

• One or more equations did not get rendered due to their size.

def FiniteArityErdosRadoBounded (κ : Cardinal.{0}) : Prop

The bounded finite-arity residual: homogeneity up to every finite arity, each stage fed by its own ladder level. This is the target of the finite-arity induction; the arrow FiniteArityErdosRadoBounded ℶ₁ → FiniteArityErdosRadoOmega1 ℶ₁ (one ω₁-suborder for all arities at once from a ℶ_{ω₁}-sized source) is a separate, careful step — the per-N outputs cannot be iterated.

Equations

• FiniteArityErdosRadoBounded κ = ∀ (N : ℕ), FiniteArityHomogeneousUpTo κ N

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

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

def singletonOE {I : Type u_1} [LinearOrder I] (x : I) : Fin 1 ↪o I

The one-point order embedding Fin 1 ↪o I at x (strict monotonicity is vacuous on the subsingleton Fin 1).

Equations

• singletonOE x = OrderEmbedding.ofStrictMono (fun (x_1 : Fin 1) => x) ⋯

theorem orderEmbedding_fin_one_eq {I : Type u_1} [LinearOrder I] (t : Fin 1 ↪o I) : t = singletonOE (t 0)

Every Fin 1 ↪o I is the one-point embedding at its value.

theorem orderEmbedding_fin_two_eq_pairEmbed {I : Type u_1} [LinearOrder I] (t : Fin 2 ↪o I) {u v : I} (h : u < v) (h0 : t 0 = u) (h1 : t 1 = v) : t = FirstOrder.Combinatorics.PairERGen.pairEmbed h

Every Fin 2 ↪o I with prescribed endpoint values is the corresponding pairEmbed (stated flexibly so the <-proof can be supplied through the endpoints of any suborder).

theorem exists_gt_succOrdToType {κ : Cardinal.{0}} (hκ : Cardinal.aleph0 ≤ κ) (x : (Order.succ κ).ord.ToType) : ∃ (y : (Order.succ κ).ord.ToType), x < y

The output order (succ κ).ord.ToType has no maximum for infinite κ: (succ κ).ord is closed under ordinal successor (succ_lt_ord_of_lt), so every element has a strict upper bound. Supplies the second pair element the arity-1 endgame of the arity-2 theorem needs.

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.

theorem eq_appendLastOE {I : Type u_1} [LinearOrder I] {n : ℕ} (t : Fin (n + 2) ↪o I) : t = FirstOrder.Combinatorics.EndHomogER.appendLastOE (RelEmbedding.trans Fin.castSuccOrderEmb t) (t (Fin.last (n + 1))) ⋯

Every (n+2)-tuple is its castSucc-prefix extended by its last point — the decomposition through which end-homogeneity reaches an arbitrary top-arity tuple.

The easy arities: 0, 1, 2

theorem finiteArityHomogeneousUpTo_zero (κ : Cardinal.{0}) (_hκ : Cardinal.aleph0 ≤ κ) : FiniteArityHomogeneousUpTo κ 0

Arity ≤ 0. Homogeneity up to arity 0 from a κ⁺-sized source: there is nothing to homogenize (Fin 0 ↪o I is a subsingleton), so any κ⁺-suborder works.

theorem finiteArityHomogeneousUpTo_one (κ : Cardinal.{0}) (hκ : Cardinal.aleph0 ≤ κ) : FiniteArityHomogeneousUpTo κ 1

Arity ≤ 1. Homogeneity up to arity 1 from a κ⁺-sized source: point pigeonhole (exists_large_fiber_of_small_codomain) on the point coloring x ↦ c 1 (singletonOE x) yields a κ⁺-sized monochromatic fiber, which re-well-orders into a κ⁺-suborder.

theorem finiteArityHomogeneousUpTo_two (κ : Cardinal.{0}) (hκ : Cardinal.aleph0 ≤ κ) : FiniteArityHomogeneousUpTo κ 2

Arity ≤ 2. Homogeneity up to arity 2 from a finiteERBound κ 2-sized source: pack the pair color and the induced point color into C 2 × C 1 (still of size ≤ κ), apply the generalized pair theorem pairErdosRado_general_of_large, and read the two components back off the homogeneous suborder — arity 1 via the no-max lemma (exists_gt_succOrdToType supplies a second pair element above any given point).

The induction step

theorem finiteArityHomogeneousUpTo_step (κ : Cardinal.{0}) (hκ : Cardinal.aleph0 ≤ κ) (n : ℕ) (ih : FiniteArityHomogeneousUpTo κ (n + 1)) : FiniteArityHomogeneousUpTo κ (n + 2)

The induction step. Homogeneity up to arity n+1 implies homogeneity up to arity n+2, from the next ladder level: end-homogenize the top-arity coloring with the engine (exists_endHomogeneous_of_large at lam := finiteERBound κ (n+1) — the ladder recursion is sized exactly so the level-n+2 source meets the engine's succ (2 ^ lam) demand and the engine's lam⁺-sized output meets the level-n+1 demand), pull the coloring family back to the end-homogeneous suborder together with the induced top-arity color ind s := c (n+2) (s ⌢ chosen-point-above) — well-defined by end-homogeneity plus the no-max lemma exists_gt_succOrdToType — and feed everything to the inductive hypothesis. An arity-(n+2) tuple from the final suborder is then handled by decomposing it as prefix-plus-last (eq_appendLastOE), swapping the last point for the chosen point above its prefix (end-homogeneity), and reading off the induced color's constancy from the IH.

The bounded finite-arity theorem

theorem finiteArityHomogeneousUpTo_all (κ : Cardinal.{0}) (hκ : Cardinal.aleph0 ≤ κ) (N : ℕ) : FiniteArityHomogeneousUpTo κ N

Homogeneity up to every finite arity: ladder levels 0/1 are the proven base cases and each higher level is one application of the induction step. (The step at n = 0 subsumes the independently validated finiteArityHomogeneousUpTo_two, which is kept as a regression check on the statement.)

theorem finiteArityErdosRadoBounded (κ : Cardinal.{0}) (hκ : Cardinal.aleph0 ≤ κ) : FiniteArityErdosRadoBounded κ

The bounded finite-arity Erdős–Rado theorem: for every infinite color bound κ and every finite arity bound N, any well-ordered source of size ≥ finiteERBound κ N and any ℕ-indexed coloring family with color types of size ≤ κ admit a single κ⁺-suborder homogeneous for all arities ≤ N simultaneously.

theorem finiteArityErdosRadoBounded_beth_one : FiniteArityErdosRadoBounded (Cardinal.beth 1)

The bounded finite-arity Erdős–Rado theorem at the Morley–Hanf color bound ℶ₁, where every ladder level sits below ℶ_{ω₁} (finiteERBound_le_beth_omega1).

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.