FormalConjectures/ErdosProblems/70.lean

GitHub source file

8 declarations, 5 contain sorry, 0 declared as axioms

1. def Erdos70.OrdinalCardinalRamsey3 OrdinalCardinalRamsey3 α β c asserts the 3-uniform ordinal Ramsey property $\alpha \to (\beta, c)^3_2$ line 65 source

   Source documentation

   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.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Ordinal, Cardinal

   Proof uses: Ordinal.ToType, Ne, And, Iff, Or, Exists, Set, Eq, Ordinal.type, LT.lt, Membership.mem, Set.Triplewise, Cardinal.mk, Not

   11 instances, coercions and auxiliary constants left out.

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

   Mentions: c

2. def Erdos70.RealCardinalRamsey3 RealCardinalRamsey3 β c asserts the 3-uniform partition relation line 91 source

   Source documentation

   RealCardinalRamsey3 β c asserts the 3-uniform partition relation $\mathfrak{c} \to (\beta, c)^3_2$, where $\mathfrak{c}$ is the order type of the real numbers with their usual order.

   It states that for any 2-coloring of all 3-element subsets of $\mathbb{R}$, one of the following must hold:

   • There is a red-monochromatic subset of order type $\beta$: the range of an order embedding β.ToType ↪o ℝ such that any three distinct elements of the range are colored red.
   • There is a blue-monochromatic subset of cardinality $c$: a set $s \subseteq \mathbb{R}$ with $\#s = c$ such that every three distinct elements of $s$ are colored blue.

   The coloring is encoded as in OrdinalCardinalRamsey3: a predicate on ordered triples of distinct reals that is invariant under permutation of its three arguments.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Ordinal, Cardinal

   Proof uses: Real, Ne, And, Iff, Or, Exists, OrderEmbedding, Ordinal.ToType, Set.Triplewise, Set.range, Set, Eq, Cardinal.mk, Not

   11 instances, coercions and auxiliary constants left out.

   def RealCardinalRamsey3 (β : Ordinal.{0}) (c : Cardinal.{0}) : Prop :=
   …

   Mentions: c

3. theorem Erdos70.erdos_70 Erdős Problem 70: Let $\mathfrak{c}$ be the order type of the real numbers, let $\beta$ be a countable ordinal, and let $2 \le n < \omega$ sorry line 113 source

   Source documentation

   Erdős Problem 70: Let $\mathfrak{c}$ be the order type of the real numbers, 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 (compare omega_three), so the genuine content of the conjecture begins at $n = 4$.

   depends on sorry what this means

   Statement uses: Iff, True, Ordinal, Nat, LE.le, Cardinal, Ordinal.card, Cardinal.aleph0, OfNat.ofNat, Erdos70.RealCardinalRamsey3

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_70 :
       answer(sorry) ↔
       ∀ᵉ (β : Ordinal.{0}) (n : ℕ) (_ : β.card ≤ ℵ₀) (_ : 2 ≤ n),
         RealCardinalRamsey3 β n := by
   …

   Mentions: Erdos70.RealCardinalRamsey3

4. theorem Erdos70.erdos_70.variants.erdos_rado Erdős–Rado partial result: $\mathfrak{c} \to (\omega + n, 4)^3_2$ for any $2 \le n < \omega$, where $\mathfrak{c}$ is the order type of the real numbers sorry line 130 source

   Source documentation

   Erdős–Rado partial result: $\mathfrak{c} \to (\omega + n, 4)^3_2$ for any $2 \le n < \omega$, where $\mathfrak{c}$ is the order type of the real numbers. Positive partial answer to Problem 70 with $\beta = \omega + n$ and the blue side fixed at $4$ [ErRa56, Theorem 31].

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, Erdos70.RealCardinalRamsey3, HAdd.hAdd, Ordinal, Ordinal.omega0, Cardinal

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   22 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_rado (n : ℕ) (hn : 2 ≤ n) :
       RealCardinalRamsey3 (ω + n) 4 := by
   …

   Mentions: Erdos70.RealCardinalRamsey3

5. theorem Erdos70.erdos_70.variants.omega_times_two_four First open case beyond Erdős–Rado: $\mathfrak{c} \to (\omega \cdot 2, 4)^3_2$, where $\mathfrak{c}$ is the order type of the real numbers sorry line 144 source

   Source documentation

   First open case beyond Erdős–Rado: $\mathfrak{c} \to (\omega \cdot 2, 4)^3_2$, where $\mathfrak{c}$ is the order type of the real numbers.

   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.

   depends on sorry what this means

   Statement uses: Iff, True, Erdos70.RealCardinalRamsey3, HMul.hMul, Ordinal, Ordinal.omega0, OfNat.ofNat, Nat, Cardinal

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   24 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem omega_times_two_four :
       answer(sorry) ↔ RealCardinalRamsey3 (ω * 2) 4 := by
   …

   Mentions: Erdos70.RealCardinalRamsey3

6. theorem Erdos70.erdos_70.variants.omega_three sorry line 164 source

   depends on sorry what this means

   Statement uses: Iff, True, Erdos70.OrdinalCardinalRamsey3, Cardinal.ord, Cardinal.continuum, Ordinal.omega0, OfNat.ofNat, Cardinal, Nat

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

7. theorem Erdos70.erdos_70.variants.omega_one 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 sorry line 178 source

   Source documentation

   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$.

   depends on sorry what this means

   Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Erdos70.OrdinalCardinalRamsey3, Cardinal.ord, Cardinal.continuum, OrderEmbedding, Ordinal, Cardinal, Cardinal.aleph

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   24 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem omega_one :
       answer(sorry) ↔
       ∀ᵉ (n : ℕ) (_ : 2 ≤ n),
         OrdinalCardinalRamsey3 (𝔠).ord (Cardinal.aleph 1).ord n := by
   …

   Mentions: Erdos70.OrdinalCardinalRamsey3

8. theorem Erdos70.erdos_70.variants.ordinalCardinalRamsey3_mono Monotonicity of OrdinalCardinalRamsey3: If OrdinalCardinalRamsey3 α β c holds and $\beta' \le \beta$, $c' \le c$, then OrdinalCardinalRamsey3 α β' c' also holds line 192 source

   Source documentation

   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.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Ordinal, Cardinal, Erdos70.OrdinalCardinalRamsey3, LE.le

   Proof uses: Ordinal.ToType, Ne, And, Iff, Exists, Set, Eq, Ordinal.type, LT.lt, Membership.mem, Set.Triplewise, Cardinal.mk, Not, Or, RelEmbedding, Nonempty, Iff.mp, inferInstance, IsWellOrder, Ordinal.type_le_iff' and 33 more

   30 instances, coercions and auxiliary constants left out.

   Tactic trace: 15 steps

   Open to load the checked before-and-after goal states.

   theorem ordinalCardinalRamsey3_mono {α β β' : Ordinal.{u}} {c c' : Cardinal.{u}}
       (h : OrdinalCardinalRamsey3 α β c) (hβ : β' ≤ β) (hc : c' ≤ c) :
       OrdinalCardinalRamsey3 α β' c' := by
   …

   Mentions: c, Erdos70.OrdinalCardinalRamsey3