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).

theorem FirstOrder.Combinatorics.EndHomogER.appendLastOE_trans {I : Type u_1} [LinearOrder I] {n : ℕ} {J : Type u_2} [LinearOrder J] (s : Fin (n + 1) ↪o I) (x : I) (hx : ∀ (k : Fin (n + 1)), s k < x) (e : I ↪o J) : RelEmbedding.trans (appendLastOE s x hx) e = appendLastOE (RelEmbedding.trans s e) (e x) ⋯

appendLastOE commutes with postcomposition by an order embedding (Fin.snoc naturality).

def FirstOrder.Combinatorics.EndHomogER.oneTupleOE {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).

Equations

• FirstOrder.Combinatorics.EndHomogER.oneTupleOE x = OrderEmbedding.ofStrictMono (fun (x_1 : Fin 1) => x) ⋯

theorem FirstOrder.Combinatorics.EndHomogER.orderEmbedding_fin_one_eq' {I : Type u_1} [LinearOrder I] (t : Fin 1 ↪o I) : t = oneTupleOE (t 0)

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

theorem FirstOrder.Combinatorics.EndHomogER.appendLastOE_oneTupleOE {I : Type u_1} [LinearOrder I] {a b : I} (h : a < b) (hab : ∀ (k : Fin 1), (oneTupleOE a) k < b) : appendLastOE (oneTupleOE a) b hab = PairERGen.pairEmbed h

Arity-1 bridge: appending b above the one-point tuple at a is exactly the pair embedding of a < b.

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

theorem FirstOrder.Combinatorics.EndHomogER.mk_finTupleEmb_le {lam : Cardinal.{0}} (m : ℕ) {α : Type} [LinearOrder α] (hα : Cardinal.mk α ≤ lam) (hlam : Cardinal.aleph0 ≤ lam) : Cardinal.mk (Fin m ↪o α) ≤ lam

Finite tuple-embedding count: #(Fin m ↪o α) ≤ lam for #α ≤ lam and infinite lam (inject into Fin m → α and collapse the finite power).

theorem FirstOrder.Combinatorics.EndHomogER.mk_tupleNode_le {lam : Cardinal.{0}} {C : Type} (hC : Cardinal.mk C ≤ lam) (hlam : Cardinal.aleph0 ≤ lam) (n : ℕ) {β : Ordinal.{0}} (hβ : β < (Order.succ lam).ord) : Cardinal.mk (Fin (n + 1) ↪o β.ToType → C) ≤ 2 ^ lam

Tuple-node count bound. For β < (succ lam).ord and #C ≤ lam, the level of recorded-color tuple nodes has at most 2 ^ lam members: #((Fin (n+1) ↪o β.ToType) → C) ≤ (2 ^ lam) ^ lam = 2 ^ lam.

theorem FirstOrder.Combinatorics.EndHomogER.nonempty_color_tuple {lam : Cardinal.{0}} (hlam : Cardinal.aleph0 ≤ lam) {C : Type} {n : ℕ} (G : Fin (n + 2) ↪o PairERGen.Source lam → C) : Nonempty C

Any (n+2)-tuple coloring on Source lam witnesses Nonempty C: the source's order type is at least ω, so it contains an increasing (n+2)-tuple.

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.

theorem FirstOrder.Combinatorics.EndHomogER.level_card_le {lam : Cardinal.{0}} {C : Type} {n : ℕ} (hlam : Cardinal.aleph0 ≤ lam) (hC : Cardinal.mk C ≤ lam) {β : Ordinal.{0}} (hβ : β < (Order.succ lam).ord) : Cardinal.mk (NodeAt C n β) ≤ 2 ^ lam

Level cardinality: for β < (succ lam).ord and #C ≤ lam the level (all length-β tuple nodes) has cardinality ≤ 2 ^ lam.

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

The color of the tuple r ⌢ y when r is strictly monotone and bounded by y (junk otherwise). Factoring the tree's recorded colors through colorAbove makes every "the color depends only on the underlying points" step a congrArg.

Equations

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

theorem FirstOrder.Combinatorics.EndHomogER.colorAbove_eq {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {y : PairERGen.Source lam} (remb : Fin (n + 1) ↪o PairERGen.Source lam) (hlt : ∀ (k : Fin (n + 1)), remb k < y) : colorAbove G y ⇑remb = G (appendLastOE remb y hlt)

On an actual bounded order embedding, colorAbove computes the appended color.

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

The successor set S(h) of a node with reps rep: points y strictly above every rep whose appended tuple colors all match the recorded ones.

Equations

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

@[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.

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

The reps along a node: the chosen rep of the restriction to each position.

Equations

• FirstOrder.Combinatorics.EndHomogER.nodeRep G h x = FirstOrder.Combinatorics.EndHomogER.nodeChosen G ((Ordinal.typein fun (x1 x2 : β.ToType) => x1 < x2).toRelEmbedding x) (h.restrict ⋯)

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 ∅

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

R(h) is a subsingleton (it is {s(h)} or ∅).

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

On a live node, the chosen rep lies in the successor set.

theorem FirstOrder.Combinatorics.EndHomogER.nodeChosen_eq_min {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {β : Ordinal.{0}} (h : NodeAt C n β) (hlive : nodeLive G h) : nodeChosen G β h = ⋯.min (nodeS G h) hlive

On a live node, nodeChosen is exactly the well-order minimum of the successor set.

theorem FirstOrder.Combinatorics.EndHomogER.nodeChosen_le_of_mem {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {β : Ordinal.{0}} (h : NodeAt C n β) {y : PairERGen.Source lam} (hy : y ∈ nodeS G h) : nodeChosen G β h ≤ y

The chosen min is ≤ every successor.

theorem FirstOrder.Combinatorics.EndHomogER.nodeChosen_congr {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {δ₁ δ₂ : Ordinal.{0}} (hδ : δ₁ = δ₂) {n₁ : NodeAt C n δ₁} {n₂ : NodeAt C n δ₂} (hn : n₁ ≍ n₂) : nodeChosen G δ₁ n₁ = nodeChosen G δ₂ n₂

nodeChosen transported along a level equality.

theorem FirstOrder.Combinatorics.EndHomogER.live_level_small {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β : β < (Order.succ lam).ord) : Cardinal.mk { h : NodeAt C n β // nodeLive G h } ≤ 2 ^ lam

Level smallness: for β < (succ lam).ord there are ≤ 2 ^ lam live length-β tuple nodes.

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.nodeRep_yNode {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) (y : PairERGen.Source lam) {β : Ordinal.{0}} [IsWellOrder β.ToType fun (x1 x2 : β.ToType) => x1 < x2] (x : β.ToType) : nodeRep G (yNode G y β) x = yRep G y ((Ordinal.typein fun (x1 x2 : β.ToType) => x1 < x2).toRelEmbedding x)

The reps of yNode G y β are exactly yRep G y (typein x).

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)

theorem FirstOrder.Combinatorics.EndHomogER.nodeRep_restrict {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {β : Ordinal.{0}} (h : NodeAt C n β) {δ : Ordinal.{0}} (hδ : δ ≤ β) (x : δ.ToType) : nodeRep G (h.restrict hδ) x = nodeRep G h ((PairERGen.initialSegOfLe hδ).toOrderEmbedding x)

The reps of a restriction agree with the parent's reps at the lifted positions.

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

A restriction of a live node is live (the same witness serves: the constraints of the restriction are a subset of the parent's, transported along nodeRep_restrict).

theorem FirstOrder.Combinatorics.EndHomogER.nodeRep_strictMono {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {β : Ordinal.{0}} {h : NodeAt C n β} (hlive : nodeLive G h) {x₁ x₂ : β.ToType} (hx : x₁ < x₂) : nodeRep G h x₁ < nodeRep G h x₂

End-homogeneity, strict monotonicity. On a live node the chosen reps strictly increase.

theorem FirstOrder.Combinatorics.EndHomogER.node_fact8 {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {β : Ordinal.{0}} {h : NodeAt C n β} (hlive : nodeLive G h) {τ : Fin (n + 1) ↪o β.ToType} {x₂ : β.ToType} (hx : ∀ (k : Fin (n + 1)), τ k < x₂) : (colorAbove G (nodeRep G h x₂) fun (k : Fin (n + 1)) => nodeRep G h (τ k)) = h τ

End-homogeneity, EHMR fact (8) in tuple form. On a live node, the recorded color at the prefix tuple τ is the actual appended color of {rep ∘ τ, rep x₂} for any position x₂ strictly above all of τ.

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) → (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).

noncomputable def FirstOrder.Combinatorics.EndHomogER.branchOfLive {lam : Cardinal.{0}} {C : Type} {n : ℕ} [Nonempty C] (G : Fin (n + 2) ↪o PairERGen.Source lam → C) {β : Ordinal.{0}} (h : NodeAt C n β) (hβ : (Order.succ lam).ord ≤ β) (hlive : nodeLive G h) : Branch G

A live node of length ≥ (succ lam).ord is a Branch: its reps (read off along the initial-segment embedding) strictly increase (nodeRep_strictMono) and satisfy fact (8) (node_fact8).

Equations

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

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.

theorem FirstOrder.Combinatorics.EndHomogER.tree_has_branch {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) : Nonempty (Branch G)

Branch-length. The canonical tuple partition tree for G has a branch of length (succ lam).ord.

The endgame: end-homogeneity read directly off the branch

theorem FirstOrder.Combinatorics.EndHomogER.exists_endHomogeneous (lam : Cardinal.{0}) (hlam : Cardinal.aleph0 ≤ lam) {C : Type} (hC : Cardinal.mk C ≤ lam) (n : ℕ) (G : Fin (n + 2) ↪o PairERGen.Source lam → C) : ∃ (f : (Order.succ lam).ord.ToType ↪o PairERGen.Source lam), ∀ (s : Fin (n + 1) ↪o PairERGen.Source lam) (x y : PairERGen.Source lam), (∀ (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)

[CONCRETE HEADLINE] End-homogenization over Source lam: there is a (succ lam).ord-indexed suborder on which the color of s ⌢ x depends only on the prefix tuple s — both branch-coherence instances at the position tuple of s give the recorded nodeFn value.

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.

Regression: the pair theorem's exact conclusion from the n = 0 engine

theorem FirstOrder.Combinatorics.EndHomogER.pairER_from_endHomogeneous (κ : Cardinal.{0}) (hκ : Cardinal.aleph0 ≤ κ) {C : Type} (hC : Cardinal.mk C ≤ κ) {I : Type} [LinearOrder I] [WellFoundedLT I] (hI : Order.succ (2 ^ κ) ≤ Cardinal.mk I) (cR : Fin 2 ↪o I → C) : ∃ (f : (Order.succ κ).ord.ToType ↪o I) (b : C), ∀ {x y : (Order.succ κ).ord.ToType} (hxy : x < y), cR (PairERGen.pairEmbed ⋯) = b

[REGRESSION] The exact conclusion of PairERGen.pairErdosRado_general_of_large, re-derived from exists_endHomogeneous_of_large at n = 0 plus the point pigeonhole: end-homogenize the pair coloring, pigeonhole the induced point color p ↦ cR {f₀ p, f₀ (canonical point above p)} (well-defined up to the choice of above-point by end-homogeneity), and re-well-order the large monochromatic fiber.