End-homogeneous Erdős–Rado: the arity-general EHMR engine (ER hard chunk 2a)

The end-homogenization Erdős–Rado theorem at every finite arity: for an infinite cardinal lam, a color type C with #C ≤ lam, and a coloring G : (Fin (n + 2) ↪o I) → C of (n+2)-tuples in a well-ordered source I of size ≥ succ (2 ^ lam), there is a (succ lam).ord-indexed suborder on which G is end-homogeneous: the color of s ⌢ x depends only on the prefix (n+1)-tuple s, not on the final point x above it (exists_endHomogeneous_of_large).

This is a port-with-modification of the proven pair engine Combinatorics/PairErdosRadoGeneral.lean (namespace PairERGen, whose generic toolbox and cardinal helpers are reused here, not re-proven). The single structural change: an EHMR tree node at level β records the new point's color against every prefix (n+1)-tuple (NodeAt C n β = (Fin (n+1) ↪o β.ToType) → C) instead of against every prefix point (EHMRNodeAt C β = β.ToType → C). The endgame is shorter than the pair file's: end-homogeneity is read directly off the branch (Branch.coloring = EHMR fact (8)); no majority/pigeonhole layers are needed.

Why pair colors cannot do this job. One could try to prove the induction step by pair-coloring {x, y} with "the induced tuple-color functions of x and y agree" — but that comparison ranges over all lower (n+1)-tuples, a varying domain of size up to the full source, so the color type explodes past every fixed bound. The EHMR tree never makes that global comparison: a node only records colors against the ≤ lam-sized branch prefix below it, and that restriction is the proof — level counting stays at 2 ^ lam, so the succ (2 ^ lam)-sized source forces a branch of length (succ lam).ord.

The pair file is the n = 0 shadow of this engine: the regression theorem pairER_from_endHomogeneous re-derives the exact conclusion of PairERGen.pairErdosRado_general_of_large from exists_endHomogeneous_of_large at n = 0 plus a point pigeonhole, protecting the statement against drift.

Consumer (ER hard chunk 2b, the finite-arity induction step): from an end-homogeneous suborder, the induced arity-(n+1) coloring c' s := G (s ⌢ any-point-above) is well-defined (end-homogeneity + the no-max lemma supply and identify the above-points), and feeding c' to the arity-(n+1) inductive hypothesis homogenizes G outright.

Structure

• Tuple utilities: appendLastOE (append a strict upper bound to an (n+1)-tuple), its evaluation/congruence/composition lemmas, and the arity-1 bridges to pairEmbed.
• Cardinal helpers: mk_finTupleEmb_le (#(Fin m ↪o α) ≤ lam) and mk_tupleNode_le (the tuple-node level bound ≤ 2 ^ lam), plus nonempty_color_tuple.
• EHMR tree with tuple-typed nodes: NodeAt/NodeAt.restrict (restriction is tuple precomposition with the initial-segment embedding), the fiber/chosen-rep recursion, the coverage y-path, end-homogeneity of live nodes (node_fact8), and branch extraction (exists_live_node_ge, tree_has_branch).
• Headline: exists_endHomogeneous (concrete source), exists_endHomogeneous_of_large (abstract well-ordered source); regression: pairER_from_endHomogeneous.

Tuple utilities: appending a strict upper bound to an (n+1)-tuple

def FirstOrder.Combinatorics.EndHomogER.appendLastOE {I : Type u_1} [LinearOrder I] {n : ℕ} (s : Fin (n + 1) ↪o I) (x : I) (hx : ∀ (k : Fin (n + 1)), s k < x) : Fin (n + 2) ↪o I

Append a strict upper bound x to an (n+1)-tuple s, giving an (n+2)-tuple. The underlying function is Fin.snoc s x; the <-proof hx enters only the strict-monotonicity argument, so the embedding's data depends on s and x alone.

Equations

• FirstOrder.Combinatorics.EndHomogER.appendLastOE s x hx = OrderEmbedding.ofStrictMono (Fin.snoc (⇑s) x) ⋯

@[simp]

theorem FirstOrder.Combinatorics.EndHomogER.appendLastOE_coe {I : Type u_1} [LinearOrder I] {n : ℕ} (s : Fin (n + 1) ↪o I) (x : I) (hx : ∀ (k : Fin (n + 1)), s k < x) : ⇑(appendLastOE s x hx) = Fin.snoc (⇑s) x

The underlying function of appendLastOE is Fin.snoc s x.

theorem FirstOrder.Combinatorics.EndHomogER.appendLastOE_castSucc {I : Type u_1} [LinearOrder I] {n : ℕ} (s : Fin (n + 1) ↪o I) (x : I) (hx : ∀ (k : Fin (n + 1)), s k < x) (k : Fin (n + 1)) : (appendLastOE s x hx) k.castSucc = s k

appendLastOE at a prefix position gives the prefix value.

theorem FirstOrder.Combinatorics.EndHomogER.appendLastOE_last {I : Type u_1} [LinearOrder I] {n : ℕ} (s : Fin (n + 1) ↪o I) (x : I) (hx : ∀ (k : Fin (n + 1)), s k < x) : (appendLastOE s x hx) (Fin.last (n + 1)) = x

appendLastOE at the last position gives the appended point.

theorem FirstOrder.Combinatorics.EndHomogER.appendLastOE_congr {I : Type u_1} [LinearOrder I] {n : ℕ} {s s' : Fin (n + 1) ↪o I} {x x' : I} (hs : ∀ (k : Fin (n + 1)), s k = s' k) (hxx : x = x') (hx : ∀ (k : Fin (n + 1)), s k < x) (hx' : ∀ (k : Fin (n + 1)), s' k < x') : appendLastOE s x hx = appendLastOE s' x' hx'

appendLastOE depends only on the underlying points (in particular it is proof-irrelevant in the <-hypothesis).

Cardinal helpers: the tuple-domain bounds the tree port consumes

The tuple-node EHMR tree skeleton

Nodes at level β are recorded-color assignments to prefix (n+1)-tuples (Fin (n+1) ↪o β.ToType) → C; reps are chosen minima of successor sets by well-founded recursion on the length, exactly as in PairERGen — only the node domain changes.

@[reducible, inline]

abbrev FirstOrder.Combinatorics.EndHomogER.NodeAt (C : Type) (n : ℕ) (β : Ordinal.{0}) : Type

A node at level β: the recorded colors at the prefix-position (n+1)-tuples of β.ToType.

Equations

• FirstOrder.Combinatorics.EndHomogER.NodeAt C n β = (Fin (n + 1) ↪o β.ToType → C)

noncomputable def FirstOrder.Combinatorics.EndHomogER.NodeAt.restrict {C : Type} {n : ℕ} {β : Ordinal.{0}} (h : NodeAt C n β) {δ : Ordinal.{0}} (hδβ : δ ≤ β) : NodeAt C n δ

Restrict a node to a shorter length δ ≤ β: precompose every position tuple with the initial-segment embedding.

Equations

• h.restrict hδβ τ = h (RelEmbedding.trans τ (FirstOrder.Combinatorics.PairERGen.initialSegOfLe hδβ).toOrderEmbedding)

theorem FirstOrder.Combinatorics.EndHomogER.NodeAt.restrict_trans {C : Type} {n : ℕ} {β : Ordinal.{0}} (h : NodeAt C n β) {δ ε : Ordinal.{0}} (hδ : δ ≤ β) (hε : ε ≤ δ) : (h.restrict hδ).restrict hε = h.restrict ⋯

Restriction is transitive (initial segments compose).

theorem FirstOrder.Combinatorics.EndHomogER.NodeAt.restrict_heq {C : Type} {n : ℕ} {β : Ordinal.{0}} (h : NodeAt C n β) {δ₁ δ₂ : Ordinal.{0}} (hδ : δ₁ = δ₂) (h1 : δ₁ ≤ β) (h2 : δ₂ ≤ β) : h.restrict h1 ≍ h.restrict h2

NodeAt.restrict at heterogeneously-equal lengths.

@[irreducible]

noncomputable def FirstOrder.Combinatorics.EndHomogER.nodeChosen {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) (β : Ordinal.{0}) (h : NodeAt C n β) : PairERGen.Source lam

Chosen representative s(h) = min S(h) — the <-least element of the successor set, by well-founded recursion on the node length: the rep at position x : β.ToType is the chosen rep of the restriction to typein x. Junk default on dead nodes.

Equations

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

def FirstOrder.Combinatorics.EndHomogER.nodeS {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {β : Ordinal.{0}} (h : NodeAt C n β) : Set (PairERGen.Source lam)

S(h) as a set, via nodeRep.

Equations

• FirstOrder.Combinatorics.EndHomogER.nodeS G h = FirstOrder.Combinatorics.EndHomogER.nodeFiber✝ G (FirstOrder.Combinatorics.EndHomogER.nodeRep✝ G h) h

def FirstOrder.Combinatorics.EndHomogER.nodeLive {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {β : Ordinal.{0}} (h : NodeAt C n β) : Prop

A node is live iff its successor set is nonempty.

Equations

• FirstOrder.Combinatorics.EndHomogER.nodeLive G h = (FirstOrder.Combinatorics.EndHomogER.nodeS G h).Nonempty

noncomputable def FirstOrder.Combinatorics.EndHomogER.nodeR {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {β : Ordinal.{0}} (h : NodeAt C n β) : Set (PairERGen.Source lam)

The used/remainder set R(h): {s(h)} on live nodes, else ∅.

Equations

• FirstOrder.Combinatorics.EndHomogER.nodeR G h = if FirstOrder.Combinatorics.EndHomogER.nodeLive G h then {FirstOrder.Combinatorics.EndHomogER.nodeChosen G β h} else ∅

Coverage — the canonical y-path

As in PairERGen, the whole y-path is defined at once: yNode G y β is the length-β node recording, at each prefix tuple τ, the color of y appended above the chosen reps of the path so far (junk once a rep is no longer < y, or the reps fail monotonicity — both absorbed by colorAbove).

@[irreducible]

noncomputable def FirstOrder.Combinatorics.EndHomogER.yRep {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) (y : PairERGen.Source lam) (γ : Ordinal.{0}) : PairERGen.Source lam

The chosen rep of the canonical y-path at level γ, by well-founded recursion: the chosen min of the node recording colorAbove of y over the earlier path reps.

Equations

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

noncomputable def FirstOrder.Combinatorics.EndHomogER.yNode {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) (y : PairERGen.Source lam) (β : Ordinal.{0}) : NodeAt C n β

The canonical y-path node of length β (a plain def over yRep).

Equations

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

theorem FirstOrder.Combinatorics.EndHomogER.yRep_eq {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) (y : PairERGen.Source lam) (γ : Ordinal.{0}) : yRep G y γ = nodeChosen G γ (yNode G y γ)

The defining fixpoint equation: yRep is the chosen min of yNode.

theorem FirstOrder.Combinatorics.EndHomogER.yNode_restrict {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) (y : PairERGen.Source lam) {β δ : Ordinal.{0}} (hδ : δ ≤ β) : (yNode G y β).restrict hδ = yNode G y δ

Restriction-coherence: every restriction of a yNode is again the yNode of that length (typein is preserved by the initial-segment embedding).

theorem FirstOrder.Combinatorics.EndHomogER.yNode_mem_of {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) (y : PairERGen.Source lam) {β : Ordinal.{0}} (hbelow : ∀ δ < β, yRep G y δ < y) : y ∈ nodeS G (yNode G y β)

Liveness criterion: if every earlier rep stays < y, then y is a successor of yNode G y β (so the node is live and y ∈ S).

theorem FirstOrder.Combinatorics.EndHomogER.yRep_strictMono {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) (y : PairERGen.Source lam) {γ₁ γ₂ : Ordinal.{0}} (h12 : γ₁ < γ₂) (hlive : ∀ δ < γ₂, yRep G y δ < y) : yRep G y γ₁ < yRep G y γ₂

As long as every rep below γ₂ stays < y, the canonical reps strictly increase.

theorem FirstOrder.Combinatorics.EndHomogER.exists_yRep_ge {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) (y : PairERGen.Source lam) : ∃ (γ : Ordinal.{0}), y ≤ yRep G y γ ∧ ∀ δ < γ, yRep G y δ < y

Stopping. The canonical y-path stops: there is a least level γ where the chosen rep reaches y, with all earlier reps strictly below y (pure well-foundedness, as in PairERGen).

theorem FirstOrder.Combinatorics.EndHomogER.exists_node_choosing_source {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) (y : PairERGen.Source lam) : ∃ (β : Ordinal.{0}) (h : NodeAt C n β), y ∈ nodeR G h

Coverage. Every source element is the chosen representative of some node (y ∈ R(h)), at the least level where the canonical y-path reaches y.

End-homogeneity of live nodes (EHMR fact (8), tuple form)

Branch extraction from a high live node

The counting core: succ (2 ^ lam)-many live nodes (coverage) cannot all sit at levels < (succ lam).ord (each such level has ≤ 2 ^ lam tuple nodes and there are only succ lam levels), so some live node has length ≥ (succ lam).ord; reading it off along the initial segment yields a Branch.

structure FirstOrder.Combinatorics.EndHomogER.Branch {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) : Type

Branch G: a strictly increasing (succ lam).ord.ToType-indexed family of reps together with the recorded tuple colors — end-homogeneity holds along it: the appended color of {rep ∘ τ, rep q} is nodeFn τ for every position tuple τ and every level q strictly above all of τ. Produced by tree_has_branch.

• rep : (Order.succ lam).ord.ToType → PairERGen.Source lam

  The rep at each position of (succ lam).ord.ToType.

• rep_strictMono : StrictMono self.rep

  The reps strictly increase.

• nodeFn : Fin (n + 1) ↪o (Order.succ lam).ord.ToType → C

  The recorded color at each prefix position tuple.

• coloring (τ : Fin (n + 1) ↪o (Order.succ lam).ord.ToType) (q : (Order.succ lam).ord.ToType) : (∀ (k : Fin (n + 1)), τ k < q) → (FirstOrder.Combinatorics.EndHomogER.colorAbove✝ G (self.rep q) fun (k : Fin (n + 1)) => self.rep (τ k)) = self.nodeFn τ

  End-homogeneity along the branch (EHMR fact (8) read off the live node).

theorem FirstOrder.Combinatorics.EndHomogER.exists_live_node_ge {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (hlam : Cardinal.aleph0 ≤ lam) (hC : Cardinal.mk C ≤ lam) (G : Fin (n + 2) ↪o PairERGen.Source lam → C) : ∃ (β : Ordinal.{0}) (h : NodeAt C n β), (Order.succ lam).ord ≤ β ∧ nodeLive G h

[THE COUNTING CORE] Some live node has length ≥ (succ lam).ord. Otherwise the coverage map injects Source lam (size succ (2 ^ lam)) into the index Σ b : (succ lam).ord.ToType, {live nodes of length typein b} of size ≤ succ lam * 2 ^ lam = 2 ^ lam, contradiction.

The endgame: end-homogeneity read directly off the branch

theorem FirstOrder.Combinatorics.EndHomogER.exists_endHomogeneous_of_large (lam : Cardinal.{0}) (hlam : Cardinal.aleph0 ≤ lam) {C : Type} (hC : Cardinal.mk C ≤ lam) (n : ℕ) {I : Type} [LinearOrder I] [WellFoundedLT I] (hI : Order.succ (2 ^ lam) ≤ Cardinal.mk I) (G : Fin (n + 2) ↪o I → C) : ∃ (f : (Order.succ lam).ord.ToType ↪o I), ∀ (s : Fin (n + 1) ↪o I) (x y : I), (∀ (k : Fin (n + 1)), s k ∈ Set.range ⇑f) → x ∈ Set.range ⇑f → y ∈ Set.range ⇑f → ∀ (hx : ∀ (k : Fin (n + 1)), s k < x) (hy : ∀ (k : Fin (n + 1)), s k < y), G (appendLastOE s x hx) = G (appendLastOE s y hy)

[HEADLINE — end-homogeneous Erdős–Rado, abstract source] For infinite lam, a color type C with #C ≤ lam, and any well-ordered source I of cardinality ≥ succ (2 ^ lam): every (n+2)-tuple coloring admits a (succ lam).ord-indexed suborder on which the color of s ⌢ x is independent of the final point x above the prefix tuple s.