Pair Erdős–Rado, parameterized by the color bound κ #
The color-parameterized pair Erdős–Rado theorem: for any infinite cardinal κ and any
color type C with #C ≤ κ, every pair coloring cR : (Fin 2 ↪o Source κ) → C of the
source order Source κ = (Order.succ (2 ^ κ)).ord.ToType (the initial well-order of the
successor of 2 ^ κ) admits a (Order.succ κ).ord-indexed strict-mono suborder on which
cR is constant. In partition-calculus notation: (2 ^ κ)⁺ → (κ⁺)²_κ.
This is a fresh-namespace (PairERGen) port of the proven Bool/ℵ₀ theorem
FirstOrder.Combinatorics.erdos_rado_pair_omega1 from Combinatorics/ErdosRado.lean,
with the renaming table Bool → C, ℶ_1 → 2 ^ κ, ℵ_1 → Order.succ κ,
ω_1 → (Order.succ κ).ord. The legacy theorem's shape is recovered as the κ = ℵ₀
specialization erdos_rado_pair_omega1_from_general. The consumers are the
end-homogenization engine (EndHomogeneousErdosRado.lean) and the finite-arity induction
(FiniteArityErdosRadoInduction.lean, culminating in the bounded
finiteArityErdosRadoBounded), which need the color bound at κ = ℶ_1 (colors = functions
on continuum-indexed positions); the all-arity FiniteArityErdosRadoOmega1 is false-shaped
(statement audit 2026-07-07 — see its docstring).
Structure #
CardinalHelpers: all cardinal arithmetic isolated — source cardinality, the level-count bound#(β.ToType → C) ≤ 2 ^ κforβ < (succ κ).ord, the counting-core productsucc κ * 2 ^ κ = 2 ^ κ, and the subset order-iso lemma.- EHMR canonical partition tree (sections mirroring the source A–H): nodes are
recorded-color sequences
β.ToType → C, reps are chosen minima of successor sets, the coveragey-path shows every source element is some node's chosen rep, counting forces a live node of length≥ (succ κ).ord, and the resulting branch assembles into aCoherentMajorityBranchfeeding the chain + pigeonhole endgame. - Headline:
pairErdosRado_general; regression:erdos_rado_pair_omega1_from_general; abstract-source wrapper:pairErdosRado_general_of_large.
Pair embedding: from an ordered pair a < b in a linearly-ordered
type, produce the canonical Fin 2 ↪o α.
Equations
Instances For
Path-counting pigeonhole. A function out of a set of cardinality ≥ succ μ into a
codomain of cardinality ≤ μ (with μ ≥ ℵ_0) has some fiber of cardinality ≥ succ μ.
Routes through Cardinal.infinite_pigeonhole_card with parameter θ := succ μ. The
regularity of succ μ (successor cardinals are regular) supplies the cofinality
hypothesis.
Project-local replacement for the deprecated Ordinal.initialSegToType (deprecated in
favor of Ordinal.type_le_iff, from which this is extracted): the initial segment
embedding of α.ToType into β.ToType from α ≤ β.
Instances For
A well-ordered source of cardinality at least c admits an order-embedding from the
initial-ordinal well-order of cardinality c. Used by the abstract-source wrapper
pairErdosRado_general_of_large to pull the coloring back to Source κ.
Any subset of c.ord.ToType of cardinality at least c is order-isomorphic to
c.ord.ToType (the generalization of the legacy ℵ_1-subset-of-ω_1 lemma).
Proof outline: the subset's order type β satisfies β ≤ c.ord (suborder) and
β.card ≥ c; since c.ord is the least ordinal of cardinality c, any β < c.ord
would force β.card < c (Cardinal.lt_ord), a contradiction. So β = c.ord, giving a
RelIso transported to an OrderIso.
Composition of initialSegOfLe via InitialSeg.eq uniqueness on well-orders.
Two initial segments from α.ToType to γ.ToType (both well-ordered) agree
pointwise. (Shared with EndHomogER, which previously carried a private copy.)
Cardinal helpers: all the κ-arithmetic the EHMR port consumes #
Pair-ER source at color bound κ. The initial ordinal of the regular successor
cardinal succ (2 ^ κ), viewed as a linearly-ordered Type. All pair-Erdős–Rado
recursion happens inside Source κ; the specialization κ = ℵ₀ recovers the legacy
PairERSource (since 2 ^ ℵ₀ = ℶ_1).
Equations
Instances For
Cardinality of the source: #(Source κ) = succ (2 ^ κ).
2 ^ κ ≠ 0 (needed for power_le_power_left monotonicity).
succ κ ≤ 2 ^ κ — Cantor plus successor minimality; holds for every κ.
ℵ_0 ≤ 2 ^ κ for infinite κ (via Cantor).
ℵ_0 ≤ succ (2 ^ κ) for infinite κ.
ℵ_0 ≤ succ κ for infinite κ.
Ordinals below (succ κ).ord have ToType of cardinality ≤ κ (the generalization
of "ordinals below ω_1 are countable").
(succ κ).ord is closed under ordinal successor for infinite κ (it is a limit
ordinal, being the initial ordinal of an uncountable-cofinality cardinal).
Node-count bound. For β < (succ κ).ord and #C ≤ κ, the level of
recorded-color sequences has at most 2 ^ κ nodes:
#(β.ToType → C) = #C ^ #β.ToType ≤ (2 ^ κ) ^ κ = 2 ^ (κ * κ) = 2 ^ κ.
Counting-core product. succ κ * 2 ^ κ = 2 ^ κ for infinite κ
(the generalization of ℵ_1 * ℶ_1 = ℶ_1).
Any coloring on Source κ witnesses Nonempty C: the source is nontrivial
(#(Source κ) = succ (2 ^ κ) ≥ 2), so it contains a strict pair, whose color inhabits
C. Supplies the junk value the coverage y-path needs.
Branch structures: validFiber, CoherentMajorityBranch, EHMRBranch #
Valid fiber (quantifier form). The set of elements y ∈ Source κ strictly above
every p β, whose pair color with each p β matches τ β. Kept in quantifier form so
that successor rewriting and restriction lemmas do not have to commute big intersections
through the recursion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
CoherentMajorityBranch cR: globally coherent prefix + branch data of length
(succ κ).ord — the object the pair Erdős–Rado endgame consumes. Produced from an
EHMRBranch by exists_coherentMajorityBranch_of_ehmrBranch.
- prefixAt (α : Ordinal.{0}) : α < (Order.succ κ).ord → α.ToType ↪o Source κ
Prefix at each level
α < (succ κ).ord. - branch (α : Ordinal.{0}) : α < (Order.succ κ).ord → α.ToType → C
Type function at each level
α < (succ κ).ord. - prefix_restrict {β α : Ordinal.{0}} (hβα : β ≤ α) (hβ : β < (Order.succ κ).ord) (hα : α < (Order.succ κ).ord) (x : β.ToType) : (self.prefixAt α hα) ((initialSegOfLe hβα).toOrderEmbedding x) = (self.prefixAt β hβ) x
Prefix coherence: prefix at α restricted to β-level via the initial-segment inclusion equals prefix at β.
- branch_restrict {β α : Ordinal.{0}} (hβα : β ≤ α) (hβ : β < (Order.succ κ).ord) (hα : α < (Order.succ κ).ord) (x : β.ToType) : self.branch α hα ((initialSegOfLe hβα).toOrderEmbedding x) = self.branch β hβ x
Branch coherence: branch at α restricted to β-level equals branch at β.
- top_in_validFiber (γ : Ordinal.{0}) (hγ : γ < (Order.succ κ).ord) (hsγ : Order.succ γ < (Order.succ κ).ord) : (self.prefixAt (Order.succ γ) hsγ) ⊤ ∈ validFiber cR (self.prefixAt γ hγ) (self.branch γ hγ)
Chain extension: the value at the top of
(succ γ).ToTypeis in thevalidFiberfor the lower-level chain at γ. This is the within-chain pair-color consistency that pair-homogeneity needs.
Instances For
EHMRBranch cR: a strictly increasing (succ κ).ord-indexed family of reps with
recorded colors — cR({rep β, rep γ}) = bit β for β < γ (EHMR fact (8) content).
Produced by the tree-counting theorem ehmr_tree_has_branch.
- rep (β : Ordinal.{0}) : β < (Order.succ κ).ord → Source κ
The rep at each position
β < (succ κ).ord. - bit (β : Ordinal.{0}) : β < (Order.succ κ).ord → C
The recorded color at each position
β < (succ κ).ord. - rep_strictMono {β γ : Ordinal.{0}} (hβ : β < (Order.succ κ).ord) (hγ : γ < (Order.succ κ).ord) : β < γ → self.rep β hβ < self.rep γ hγ
The reps strictly increase.
- coloring {β γ : Ordinal.{0}} (hβ : β < (Order.succ κ).ord) (hγ : γ < (Order.succ κ).ord) (hβγ : β < γ) : cR (pairEmbed ⋯) = self.bit β hβ
Instances For
EHMR canonical-tree skeleton #
Nodes are recorded-color sequences β.ToType → C (Type 0, so the counting stays in
Cardinal.{0}); reps s(h↾γ) = min S(h↾γ) are derived by well-founded recursion on
length; live = nonempty successor set.
A node at level β: the recorded colors at the positions β.ToType. The eventual
branch is a cofinal chain through these of length < (succ κ).ord.
Equations
- FirstOrder.Combinatorics.PairERGen.EHMRNodeAt C β = (β.ToType → C)
Instances For
Restrict a node to a shorter length δ ≤ β, via the initial-segment embedding.
Equations
- h.restrict hδβ x = h ((FirstOrder.Combinatorics.PairERGen.initialSegOfLe hδβ).toOrderEmbedding x)
Instances For
[EHMR §14, Lemma 14.2 + |E| counting — coverage/counting engine] If the
"used-up" sets R i cover Source κ and each is a subsingleton, then the node index
set has cardinality ≥ succ (2 ^ κ) = #(Source κ). This is the counting feeding the
branch-length theorem.
The successor set S(h): points above all the reps respecting the recorded
colors. (β.ToType-indexed validFiber shape, with a plain-function rep.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Chosen representative s(h) = min S(h) — the <-least element of the successor
set (via Source κ's well-order), 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 (empty-fiber) nodes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The reps along a node: the chosen rep of the restriction to each position.
Equations
- FirstOrder.Combinatorics.PairERGen.ehmrRep cR h x = FirstOrder.Combinatorics.PairERGen.ehmrChosen cR ((Ordinal.typein fun (x1 x2 : β.ToType) => x1 < x2).toRelEmbedding x) (h.restrict ⋯)
Instances For
S(h) as a set, via ehmrRep.
Equations
Instances For
A node is live iff its successor set is nonempty.
Equations
Instances For
The used/remainder set R(h): {s(h)} on live nodes, else ∅.
Equations
Instances For
R(h) is a subsingleton (it is {s(h)} or ∅).
On a live node, the chosen rep lies in the successor set.
On a live node, ehmrChosen is exactly the well-order minimum of the successor set
(the defining unfold).
The chosen min is ≤ every successor (the <-least element of S(h) in the
linear well-order).
Level cardinality: for β < (succ κ).ord the level (all length-β nodes) has
cardinality ≤ 2 ^ κ — β.ToType of size ≤ κ, C-valued with #C ≤ κ.
ehmrChosen transported along a level equality: equal levels plus
heterogeneously-equal nodes give equal chosen reps.
Level smallness: for β < (succ κ).ord there are ≤ 2 ^ κ live length-β nodes
(a fortiori ≤ 2 ^ κ nodes, by ehmr_level_card_le).
Coverage (EHMR Lemma 14.2) — the canonical y-path #
Rather than build the y-path by transfinite recursion with an explicit limit step, we
define the whole path at once: yNode cR y β is the length-β node recording, at each
position x, the pair-color of y against the chosen rep of the path so far — or junk
(an arbitrary color) once that rep is no longer < y. Restriction-coherence then
becomes a lemma, and the stopping argument is pure well-foundedness.
The chosen rep of the canonical y-path at level γ, defined by well-founded
recursion: it is the chosen min of the node whose recorded color at each position x is
cR({yRep(typein x), y}) (or junk once that rep is ≥ y). Because the recursion lands
in Source κ (non-dependent), restriction-coherence later needs only congrArg, not a
heterogeneous transport.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical y-path node of length β (a plain def over yRep): at position
x it records the pair-color of y against yRep (typein x) (junk once that rep is
≥ y).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining fixpoint equation: yRep is the chosen min of yNode.
Restriction-coherence: every restriction of a yNode is again the yNode of that
length. (Each color depends only on yRep (typein x), and typein is preserved by the
initial-segment embedding.)
The reps of yNode cR y β are exactly yRep cR y (typein x). (The IsWellOrder
binder lets typein appear in the signature; call sites discharge it with
isWellOrder_lt.)
Liveness criterion: if every earlier rep stays < y, then y is a successor of
yNode cR y β (so the node is live and y ∈ S).
As long as yNode cR y γ₂ is live (every earlier rep stays < y), the canonical
reps strictly increase: yRep γ₁ < yRep γ₂ for γ₁ < γ₂. (The rep at the position γ₁
of yNode γ₂ is yRep γ₁, and it lies strictly below the chosen min yRep γ₂.)
Stopping. The canonical y-path stops: there is a least level γ where the
chosen rep reaches y (y ≤ yRep γ), with all earlier reps strictly below y.
Existence is pure well-foundedness — if every yRep γ stayed < y then yRep would be
a strictly increasing Ordinal → Source κ, and composing with typein gives a strictly
increasing Ordinal → Ordinal exceeding the order type of Source κ, impossible.
Coverage (EHMR Lemma 14.2). Every source element is the chosen representative of
some node (y ∈ R(h)): take the least level γ where the canonical y-path reaches
y (exists_yRep_ge). There every earlier rep is < y, so the node is live
(yNode_mem_of) and its chosen min is ≤ y (ehmrChosen_le_of_mem); combined with
y ≤ yRep γ this forces y = s(yNode γ), i.e. y ∈ R(yNode γ).
End-homogeneity of live nodes (EHMR fact (8)) #
Restriction is transitive (initial segments compose).
EHMRNodeAt.restrict at heterogeneously-equal lengths.
The reps of a restriction agree with the parent's reps at the lifted positions.
A restriction of a live node is live (the same witness y serves, since the reps
and recorded colors only shrink).
cR ∘ pairEmbed depends only on the two endpoints, not on the <-proof: equal
endpoints give equal colors.
End-homogeneity, strict monotonicity. On a live node the chosen reps strictly
increase: the rep at x₁ is the rep of the restriction-to-x₂ at the position of x₁,
hence strictly below that restriction's chosen min = rep x₂.
End-homogeneity, EHMR fact (8). On a live node, the recorded color at x₁ is
the pair-color of the reps {rep x₁, rep x₂} for any x₁ < x₂.
Branch extraction from a high live node #
EHMR Theorem 13.1 realized concretely: the succ (2 ^ κ)-many live nodes (coverage)
cannot all sit at levels < (succ κ).ord (each such level has ≤ 2 ^ κ nodes, and
there are only succ κ of them), so some live node has length ≥ (succ κ).ord;
reading it off at the first (succ κ).ord positions yields an EHMRBranch.
The position enum β' of a length-β node, for β' < (succ κ).ord ≤ β.
Equations
- FirstOrder.Combinatorics.PairERGen.ehmrBranchPos hβ β' hβ' = (Ordinal.enum fun (x1 x2 : β.ToType) => x1 < x2) ⟨β', ⋯⟩
Instances For
Positions are strictly monotone in the level.
A live node of length ≥ (succ κ).ord is an EHMRBranch: its reps (read off at
the positions enum β') strictly increase (ehmrRep_strictMono) and satisfy fact (8)
(ehmr_fact8).
Equations
- One or more equations did not get rendered due to their size.
Instances For
[THE COUNTING CORE — EHMR Theorem 13.1] Some live node has length
≥ (succ κ).ord.
Suppose not: every live node has length < (succ κ).ord. Then the coverage map
(exists_node_choosing_source) injects Source κ into the Type-0 index
Σ b : (succ κ).ord.ToType, EHMRNodeAt C (typein b) via
ehmr_partitionTree_card_lower. But that index has size at most
succ κ * 2 ^ κ = 2 ^ κ (mk_node_le per fibre, succ_mul_two_power), so
succ (2 ^ κ) ≤ 2 ^ κ, contradiction.
[EHMR §13 Theorem 13.1 / §14 Theorem 14.3 — branch-length] The canonical
partition tree for cR has a branch of length (succ κ).ord: a live node of length
≥ (succ κ).ord (exists_live_node_ge) restricts to the sought EHMRBranch
(ehmrBranch_of_live).
Assembly: EHMR branch → CoherentMajorityBranch #
Assemble an EHMRBranch into a CoherentMajorityBranch. prefixAt α is the
embedding α.ToType ↪o Source κ sending position β < α to rep β; branch α reads
off bit; prefix_restrict/branch_restrict are immediate from the assembly;
top_in_validFiber is EHMR fact (8) (coloring).
Existence of a CoherentMajorityBranch — a coherent branch (prefix/branch
restriction coherence + top_in_validFiber) of length (succ κ).ord, the object the
pair Erdős–Rado endgame consumes. Derived directly from the EHMR canonical partition
tree.
Chain + pigeonhole endgame #
treeCommitOfBranch: canonical commit at position δ using B. Reads off
B.prefixAt (succ δ) ⊤ (the top of the succ δ chain).
Equations
- FirstOrder.Combinatorics.PairERGen.treeCommitOfBranch hκ B δ hδ = (B.prefixAt (Order.succ δ) ⋯) ⊤
Instances For
treeCommitColorOfBranch: canonical color at position δ using B. Reads off
B.branch (succ δ) ⊤.
Equations
- FirstOrder.Combinatorics.PairERGen.treeCommitColorOfBranch hκ B δ hδ = B.branch (Order.succ δ) ⋯ ⊤
Instances For
treeCommitOfBranch_strictMono: strict monotonicity of the branch-driven chain
values, inherited from B.prefixAt's order embedding structure + prefix_restrict to
identify levels.
treeCommitColorFnOfBranch: indexed color function on (succ κ).ord.ToType
using B.
Equations
- One or more equations did not get rendered due to their size.
Instances For
treeChainEmbeddingOfBranch: (succ κ).ord.ToType ↪o Source κ embedding
driven by B.
Equations
- One or more equations did not get rendered due to their size.
Instances For
treeChain_pair_homogeneous_ofBranch: pair-homogeneity along the branch-driven
chain. For δ < η < (succ κ).ord,
cR (pair (treeCommitOfBranch B δ) (treeCommitOfBranch B η)) = treeCommitColorOfBranch B δ.
Proof: by B.top_in_validFiber η, commit η = B.prefixAt (succ η) ⊤ is in
validFiber cR (B.prefixAt η hη) (B.branch η hη). Apply at position enum δ : η.ToType;
use B.prefix_restrict / B.branch_restrict to identify the constraint values with
commit δ and commit color δ.
[THE FINAL PIGEONHOLE] Color pigeonhole on treeCommitColorFnOfBranch B: some
color has a succ κ-sized preimage (domain of size succ κ, codomain of size
≤ κ).
[CONDITIONAL HEADLINE] Parameterized pair Erdős–Rado, assuming a
CoherentMajorityBranch: there is a color b and a (succ κ).ord-indexed strict-mono
sequence into Source κ whose every pair has cR-color b.
Proof: color pigeonhole (exists_large_treeCommitColorFn_fiber_ofBranch) gives a
succ κ-sized preimage of some b; ordIso_ordToType_of_card_ge gives an order iso
preimage ≃ (succ κ).ord.ToType. Compose with treeChainEmbeddingOfBranch B to get the
embedding; pair-homogeneity comes from treeChain_pair_homogeneous_ofBranch + constancy
of treeCommitColorFnOfBranch B on the preimage.
The headline, the regression specialization, and the abstract-source wrapper #
[HEADLINE — parameterized pair Erdős–Rado] For infinite κ and any color type
C with #C ≤ κ, every pair coloring of Source κ = (succ (2 ^ κ)).ord.ToType is
constant on a (succ κ).ord-indexed strict-mono suborder: (2 ^ κ)⁺ → (κ⁺)²_κ.
The κ = ℵ₀, C = Bool case is the legacy erdos_rado_pair_omega1.
[REGRESSION] The legacy Bool/ℵ₀ shape, recovered from the general theorem at
κ = ℵ₀ via succ ℵ₀ = ℵ_1 and (ℵ_1).ord = ω_1 (stated with this file's own
Source/pairEmbed; Source ℵ₀ = (succ (2 ^ ℵ₀)).ord.ToType matches the legacy
PairERSource = (succ ℶ_1).ord.ToType up to 2 ^ ℵ₀ = ℶ_1).
[ABSTRACT SOURCE] The parameterized pair Erdős–Rado over any well-ordered source
I of cardinality ≥ succ (2 ^ κ): embed Source κ into I
(exists_ordToType_embedding_of_card_ge), pull the coloring back, and transport the
homogeneous chain forward.