Erdős Problem 70

Reference: erdosproblems.com/70

The 3-uniform (triple) partition relation $\mathfrak{c} \to (\beta, n)^3_2$ on the ordinal of the real numbers — the triple analogue of OrdinalCardinalRamsey used in Problems 590–592.

def Erdos70.OrdinalCardinalRamsey3 (α β : Ordinal.{u}) (c : Cardinal.{u}) : Prop

OrdinalCardinalRamsey3 α β c asserts the 3-uniform ordinal Ramsey property $\alpha \to (\beta, c)^3_2$.

It states that for any 2-coloring of all 3-element subsets of (the ordinal type) $\alpha$, one of the following must hold:

• There is a red-monochromatic subset of order type $\beta$: every 3-element sub-subset is colored red. (Formally: a set $s \subseteq \alpha$ with $\operatorname{typeLT} s = \beta$ such that any three distinct elements of $s$ are colored red.)
• There is a blue-monochromatic subset of cardinality $c$: a set $s \subseteq \alpha$ with $\#s = c$ such that every three distinct elements of $s$ are colored blue.

The coloring is given as a predicate isRed : α.ToType → α.ToType → α.ToType → Prop on ordered triples of distinct elements; to faithfully encode a coloring of unordered 3-element subsets we additionally require isRed to be invariant under permutation of its three (distinct) arguments.

Equations

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

theorem Erdos70.erdos_70 : sorry ↔ ∀ (β : Ordinal.{0}) (n : ℕ), β.card ≤ Cardinal.aleph0 → 2 ≤ n → OrdinalCardinalRamsey3 Cardinal.continuum.ord β ↑n

Erdős Problem 70: Let $\mathfrak{c}$ be the cardinality of the continuum, let $\beta$ be a countable ordinal, and let $2 \le n < \omega$. Is it true that $\mathfrak{c} \to (\beta, n)^3_2$?

Note: The cases $n \le 3$ are trivially true (see omega_three), so the genuine content of the conjecture begins at $n = 4$.

theorem Erdos70.erdos_70.variants.erdos_rado (n : ℕ) (hn : 2 ≤ n) : OrdinalCardinalRamsey3 Cardinal.continuum.ord (Ordinal.omega0 + ↑n) 4

Erdős–Rado partial result: $\mathfrak{c} \to (\omega + n, 4)^3_2$ for any $2 \le n < \omega$. Positive partial answer to Problem 70 with $\beta = \omega + n$ and the blue side fixed at $4$.

theorem Erdos70.erdos_70.variants.omega_times_two_four : sorry ↔ OrdinalCardinalRamsey3 Cardinal.continuum.ord (Ordinal.omega0 * 2) 4

First open case beyond Erdős–Rado: $\mathfrak{c} \to (\omega \cdot 2, 4)^3_2$.

Erdős and Rado proved $\mathfrak{c} \to (\omega + n, 4)^3_2$ for every finite $n \ge 2$ (see erdos_rado), which covers all red ordinals below $\omega \cdot 2 = \omega + \omega$. This variant asks whether the result extends to $\beta = \omega \cdot 2$, the simplest countable ordinal not covered by their theorem.

theorem Erdos70.erdos_70.variants.omega_three : True ↔ OrdinalCardinalRamsey3 Cardinal.continuum.ord Ordinal.omega0 3

Trivial boundary case: $\mathfrak{c} \to (\omega, 3)^3_2$.

This is trivially true because in a 3-uniform hypergraph, a "blue clique of size 3" consists of a single 3-element subset ($\binom{3}{3} = 1$), so the blue alternative merely asks for one blue triple to exist. The proof splits into two cases:

• If any blue triple exists, it is itself a blue-monochromatic set of cardinality 3.
• If no blue triple exists, all triples are red, and since $\omega \le \mathfrak{c}$, any subset of order type $\omega$ is red-monochromatic.

The problem becomes non-trivial only for $n \ge 4$; see omega_times_two_four for the simplest genuinely open case.

theorem Erdos70.erdos_70.variants.omega_one : sorry ↔ ∀ (n : ℕ), 2 ≤ n → OrdinalCardinalRamsey3 Cardinal.continuum.ord (Cardinal.aleph 1).ord ↑n

The relation at $\omega_1$: $\mathfrak{c} \to (\omega_1, n)^3_2$ for finite $n \ge 2$, where $\omega_1 = \aleph_1$ is the first uncountable ordinal.

Note that $\omega_1$ is not a countable ordinal, so this is not directly an instance of the main Erdős problem (which asks for countable $\beta$). Under CH, $\omega_1 = \mathfrak{c}.\mathrm{ord}$, making this a self-referential question about $\mathfrak{c}.\mathrm{ord} \to (\mathfrak{c}.\mathrm{ord}, n)^3_2$.

theorem Erdos70.erdos_70.variants.ordinalCardinalRamsey3_mono {α β β' : Ordinal.{u}} {c c' : Cardinal.{u}} (h : OrdinalCardinalRamsey3 α β c) (hβ : β' ≤ β) (hc : c' ≤ c) : OrdinalCardinalRamsey3 α β' c'

Monotonicity of OrdinalCardinalRamsey3: If OrdinalCardinalRamsey3 α β c holds and $\beta' \le \beta$, $c' \le c$, then OrdinalCardinalRamsey3 α β' c' also holds.

This allows us to deduce weaker partition results from stronger ones.