/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/importFormalConjecturesUtil
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.
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.
defOrdinalCardinalRamsey3(αβ:Ordinal.{u})(c:Cardinal.{u}):Prop:=-- For any partition of 3-element subsets into red and blue:∀(isRed:α.ToType→α.ToType→α.ToType→Prop),-- The colouring is well-defined on *unordered* triples of distinct elements:(∀xyz,x≠y→y≠z→x≠z→(isRedxyz↔isRedyxz)∧(isRedxyz↔isRedxzy))→-- either there is a red-monochromatic subset of order type β(∃s:Setα.ToType,typeLTs=β∧s.TriplewiseisRed)∨-- or there is a blue-monochromatic subset of cardinality c(∃s:Setα.ToType,#s=c∧s.Triplewise(funxyz↦¬isRedxyz))
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$.
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$.
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.
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.
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$.
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.
inlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3αβchβ:typeLTβ'.ToType≤βhc:c'≤cisRed:α.ToType→α.ToType→α.ToType→ProphSym:∀(xyz:α.ToType),x≠y→y≠z→x≠z→(isRedxyz↔isRedyxz)∧(isRedxyz↔isRedxzy)s:Setα.ToTypehs_type:typeLT↑s=βhs_clique:s.TriplewiseisRed⊢ (∃s,typeLT↑s=β'∧s.TriplewiseisRed)∨∃s,#↑s=c'∧s.Triplewisefunxyz↦¬isRedxyzobtain⟨g⟩:=Ordinal.type_le_iff'.mp(hs_type▸hβ)inlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3αβchβ:typeLTβ'.ToType≤βhc:c'≤cisRed:α.ToType→α.ToType→α.ToType→ProphSym:∀(xyz:α.ToType),x≠y→y≠z→x≠z→(isRedxyz↔isRedyxz)∧(isRedxyz↔isRedxzy)s:Setα.ToTypehs_type:typeLT↑s=βhs_clique:s.TriplewiseisRedg:(funx1x2↦x1<x2)↪rfunx1x2↦x1<x2⊢ (∃s,typeLT↑s=β'∧s.TriplewiseisRed)∨∃s,#↑s=c'∧s.Triplewisefunxyz↦¬isRedxyzlett:Setα.ToType:=Set.range(Subtype.val∘g)inlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3αβchβ:typeLTβ'.ToType≤βhc:c'≤cisRed:α.ToType→α.ToType→α.ToType→ProphSym:∀(xyz:α.ToType),x≠y→y≠z→x≠z→(isRedxyz↔isRedyxz)∧(isRedxyz↔isRedxzy)s:Setα.ToTypehs_type:typeLT↑s=βhs_clique:s.TriplewiseisRedg:(funx1x2↦x1<x2)↪rfunx1x2↦x1<x2t:Setα.ToType:=Set.range(Subtype.val∘⇑g)⊢ (∃s,typeLT↑s=β'∧s.TriplewiseisRed)∨∃s,#↑s=c'∧s.Triplewisefunxyz↦¬isRedxyzrefineOr.inl⟨t,?_,hs_clique.mono(byα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3αβchβ:typeLTβ'.ToType≤βhc:c'≤cisRed:α.ToType→α.ToType→α.ToType→ProphSym:∀(xyz:α.ToType),x≠y→y≠z→x≠z→(isRedxyz↔isRedyxz)∧(isRedxyz↔isRedxzy)s:Setα.ToTypehs_type:typeLT↑s=βhs_clique:s.TriplewiseisRedg:(funx1x2↦x1<x2)↪rfunx1x2↦x1<x2t:Setα.ToType:=Set.range(Subtype.val∘⇑g)⊢ t⊆srintrox⟨a,rfl⟩α:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3αβchβ:typeLTβ'.ToType≤βhc:c'≤cisRed:α.ToType→α.ToType→α.ToType→ProphSym:∀(xyz:α.ToType),x≠y→y≠z→x≠z→(isRedxyz↔isRedyxz)∧(isRedxyz↔isRedxzy)s:Setα.ToTypehs_type:typeLT↑s=βhs_clique:s.TriplewiseisRedg:(funx1x2↦x1<x2)↪rfunx1x2↦x1<x2t:Setα.ToType:=Set.range(Subtype.val∘⇑g)a:β'.ToType⊢ (Subtype.val∘⇑g)a∈s;exact(ga).2All goals completed! 🐙)⟩-- Show typeLT t = β'letemb:(·<·:β'.ToType→β'.ToType→Prop)↪r(·<·:↑t→↑t→Prop):={toFun:=funa=>⟨(ga).val,a,rfl⟩inj':=funabheq=>g.injective(Subtype.ext(congr_arg(funx:↑t=>x.val)heq))map_rel_iff':=g.map_rel_iff}inlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3αβchβ:typeLTβ'.ToType≤βhc:c'≤cisRed:α.ToType→α.ToType→α.ToType→ProphSym:∀(xyz:α.ToType),x≠y→y≠z→x≠z→(isRedxyz↔isRedyxz)∧(isRedxyz↔isRedxzy)s:Setα.ToTypehs_type:typeLT↑s=βhs_clique:s.TriplewiseisRedg:(funx1x2↦x1<x2)↪rfunx1x2↦x1<x2t:Setα.ToType:=Set.range(Subtype.val∘⇑g)emb:(funx1x2↦x1<x2)↪rfunx1x2↦x1<x2:={toFun:=funa↦⟨↑(ga),⋯⟩,inj':=⋯,map_rel_iff':=⋯}⊢ typeLT↑t=β'havehsurj:Function.Surjectiveemb:=fun⟨_,hy⟩=>⟨hy.choose,Subtype.exthy.choose_spec⟩inlα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3αβchβ:typeLTβ'.ToType≤βhc:c'≤cisRed:α.ToType→α.ToType→α.ToType→ProphSym:∀(xyz:α.ToType),x≠y→y≠z→x≠z→(isRedxyz↔isRedyxz)∧(isRedxyz↔isRedxzy)s:Setα.ToTypehs_type:typeLT↑s=βhs_clique:s.TriplewiseisRedg:(funx1x2↦x1<x2)↪rfunx1x2↦x1<x2t:Setα.ToType:=Set.range(Subtype.val∘⇑g)emb:(funx1x2↦x1<x2)↪rfunx1x2↦x1<x2:={toFun:=funa↦⟨↑(ga),⋯⟩,inj':=⋯,map_rel_iff':=⋯}hsurj:Function.Surjective⇑emb⊢ typeLT↑t=β'exact(Ordinal.type_eq.mpr⟨RelIso.ofSurjectiveembhsurj|>.symm⟩).trans(Ordinal.type_toTypeβ')All goals completed! 🐙·inrα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3αβchβ:β'≤βhc:c'≤cisRed:α.ToType→α.ToType→α.ToType→ProphSym:∀(xyz:α.ToType),x≠y→y≠z→x≠z→(isRedxyz↔isRedyxz)∧(isRedxyz↔isRedxzy)s:Setα.ToTypehs_card:#↑s=chs_clique:s.Triplewisefunxyz↦¬isRedxyz⊢ (∃s,typeLT↑s=β'∧s.TriplewiseisRed)∨∃s,#↑s=c'∧s.Triplewisefunxyz↦¬isRedxyz-- Blue case: s has cardinality c; find a sub-set of cardinality c' ≤ cobtain⟨t,ht_sub,ht_card⟩:=(Cardinal.le_mk_iff_exists_subset).mp(hs_card▸hc)inrα:Ordinal.{u}β:Ordinal.{u}β':Ordinal.{u}c:Cardinal.{u}c':Cardinal.{u}h:OrdinalCardinalRamsey3αβchβ:β'≤βhc:c'≤cisRed:α.ToType→α.ToType→α.ToType→ProphSym:∀(xyz:α.ToType),x≠y→y≠z→x≠z→(isRedxyz↔isRedyxz)∧(isRedxyz↔isRedxzy)s:Setα.ToTypehs_card:#↑s=chs_clique:s.Triplewisefunxyz↦¬isRedxyzt:Setα.ToTypeht_sub:t⊆sht_card:#↑t=c'⊢ (∃s,typeLT↑s=β'∧s.TriplewiseisRed)∨∃s,#↑s=c'∧s.Triplewisefunxyz↦¬isRedxyzexactOr.inr⟨t,ht_card,hs_clique.monoht_sub⟩All goals completed! 🐙enderdos_70.variantsendErdos70