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 file develops the canonical partition tree and extracts a live node of length at least
(Order.succ κ).ord. The end-homogenization engine in
EndHomogeneousErdosRado.lean consumes that node.
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: 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. - Consumer interface:
exists_live_node_ge.
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 κ.
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
2 ^ κ ≠ 0 (needed for power_le_power_left monotonicity).
succ κ ≤ 2 ^ κ — Cantor plus successor minimality; holds for every κ.
ℵ_0 ≤ succ (2 ^ κ) 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).
Counting-core product. succ κ * 2 ^ κ = 2 ^ κ for infinite κ
(the generalization of ℵ_1 * ℶ_1 = ℶ_1).
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.
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
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
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.)
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.
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 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.