Erdős Problem 1128

Reference: erdosproblems.com/1128

def Erdos1128.IsMonochromaticBox {A : Type u_1} {B : Type u_2} {C : Type u_3} (f : A → B → C → Fin 2) (A₁ : Set A) (B₁ : Set B) (C₁ : Set C) : Prop

A subset $A_1 \times B_1 \times C_1$ of $A \times B \times C$ is monochromatic under a 2-colouring $f : A \to B \to C \to \operatorname{Fin} 2$ if $f$ is constant on $A_1 \times B_1 \times C_1$.

Equations

• Erdos1128.IsMonochromaticBox f A₁ B₁ C₁ = ∃ (c : Fin 2), ∀ a ∈ A₁, ∀ b ∈ B₁, ∀ c' ∈ C₁, f a b c' = c

theorem Erdos1128.erdos_1128.prikryMills : ∃ (X : Type) (_ : Cardinal.mk X = Cardinal.aleph 1) (f : X → X → X → Fin 2), ∀ (A₁ B₁ C₁ : Set X), Cardinal.mk ↑A₁ = Cardinal.aleph 0 → Cardinal.mk ↑B₁ = Cardinal.aleph 0 → Cardinal.mk ↑C₁ = Cardinal.aleph 0 → ¬IsMonochromaticBox f A₁ B₁ C₁

Prikry–Mills counterexample (key lemma):

There exists a 2-colouring $f$ of a set of cardinality $\aleph_1$ cubed such that no countable box $A_1 \times B_1 \times C_1$ is monochromatic.

This is the unpublished result of Prikry and Mills (1978). The proof proceeds by transfinite induction along $\omega_1$, which has uncountable cofinality, ensuring every countable box is non-monochromatic.

theorem Erdos1128.erdos_1128 : False ↔ ∀ (A B C : Type), Cardinal.mk A = Cardinal.aleph 1 → Cardinal.mk B = Cardinal.aleph 1 → Cardinal.mk C = Cardinal.aleph 1 → ∀ (f : A → B → C → Fin 2), ∃ (A₁ : Set A) (B₁ : Set B) (C₁ : Set C), Cardinal.mk ↑A₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑B₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑C₁ = Cardinal.aleph 0 ∧ IsMonochromaticBox f A₁ B₁ C₁

Erdős Problem 1128 (disproved by Prikry–Mills, 1978):

Erdős asked whether every 2-colouring of $A \times B \times C$, where $|A| = |B| = |C| = \aleph_1$, must contain a monochromatic countable box $A_1 \times B_1 \times C_1$ with $|A_1| = |B_1| = |C_1| = \aleph_0$.

The answer is No: Prikry and Mills constructed a 2-colouring of $\omega_1^3$ with no monochromatic countable box.

Note: The positive statement asserts that every 2-colouring of every $\aleph_1^3$ contains a monochromatic countably infinite box. Since the answer is False, this positive statement fails.

theorem Erdos1128.erdos_1128.variants.prikryMills_explicit : ∃ (f : { o : Ordinal.{u_1} // o < Ordinal.omega 1 } → { o : Ordinal.{u_2} // o < Ordinal.omega 1 } → { o : Ordinal.{u_3} // o < Ordinal.omega 1 } → Fin 2), ∀ (A₁ : Set { o : Ordinal.{u_1} // o < Ordinal.omega 1 }) (B₁ : Set { o : Ordinal.{u_2} // o < Ordinal.omega 1 }) (C₁ : Set { o : Ordinal.{u_3} // o < Ordinal.omega 1 }), Cardinal.mk ↑A₁ = Cardinal.aleph 0 → Cardinal.mk ↑B₁ = Cardinal.aleph 0 → Cardinal.mk ↑C₁ = Cardinal.aleph 0 → ¬IsMonochromaticBox f A₁ B₁ C₁

Explicit form of Prikry–Mills:

There exists a 2-colouring of $\omega_1 \times \omega_1 \times \omega_1$ such that for every countably infinite $A_1, B_1, C_1 \subseteq \omega_1$, the box $A_1 \times B_1 \times C_1$ is not monochromatic.

This is the content of the Prikry–Mills theorem (1978, unpublished), stated using Lean's ordinal type {o : Ordinal // o < ω_ 1} as the representation of $\omega_1$.

theorem Erdos1128.erdos_1128.variants.two_dimensional_false : ¬∀ (f : Erdos1128.Omega1✝ → Erdos1128.Omega1✝ → Fin 2), ∃ (A₁ : Set Erdos1128.Omega1✝¹) (B₁ : Set Erdos1128.Omega1✝²), ¬A₁.Countable ∧ ¬B₁.Countable ∧ ∃ (c : Fin 2), ∀ a ∈ A₁, ∀ b ∈ B₁, f a b = c

The claim that every 2-colouring of $\omega_1 \times \omega_1$ has an uncountable monochromatic product rectangle is false in ZFC.

Counterexample: The ordering colouring $f(\alpha, \beta) = 0$ iff $\alpha < \beta$ has no uncountable monochromatic product rectangle $A_1 \times B_1$.

Proof: If $A_1 \times B_1$ were monochromatic with colour 0, then every element of $A_1$ would be strictly less than every element of $B_1$, making $A_1$ bounded above in $\omega_1$; but any bounded subset of $\omega_1$ is countable (since initial segments are countable), contradicting $A_1$ being uncountable. The colour-1 case is symmetric with the roles of $A_1$ and $B_1$ swapped.

Note: The correct classical result for 2-colourings of pairs (not products) is the Erdős–Rado theorem $\omega_1 \to (\omega_1)^2_2$, which concerns unordered pairs.