Add Erdős Problem 1173 (set mappings on ω_{ω+1} under GCH)

FormalConjectures/ErdosProblems/1173.lean

@@ -0,0 +1,201 @@
+/-
+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.
+-/
+import FormalConjectures.Util.ProblemImports
+
+open Cardinal Ordinal
+
+open scoped Cardinal Ordinal
+
+/-!
+# Erdős Problem 1173
+
+**Verbatim statement (Erdős #1173, status O):**
+> Assume the generalised continuum hypothesis. Let\[f: \omega_{\omega+1}\to [\omega_{\omega+1}]^{\leq \aleph_\omega}\]be a set mapping such that\[\lvert f(\alpha)\cap f(\beta)\rvert <\aleph_\omega\]for all $\alpha\neq \beta$. Does there exist a free set of cardinality $\aleph_{\omega+1}$?
+
+**Source:** https://www.erdosproblems.com/1173
+
+**Notes:** OPEN
+
+
+*Reference:* [erdosproblems.com/1173](https://www.erdosproblems.com/1173)
+
+*References:*
+- [EH74] Erdős, Paul and Hajnal, András, Unsolved and solved problems in set theory.
+  Proceedings of the Tarski symposium (1974), 269–287.
+
+## Problem Statement
+
+Assume GCH. Let $f : \omega_{\omega+1} \to [\omega_{\omega+1}]^{\leq \aleph_\omega}$ be a
+**set mapping** — a function assigning to each element $\alpha \in \omega_{\omega+1}$ a subset
+$f(\alpha) \subseteq \omega_{\omega+1}$ of cardinality at most $\aleph_\omega$ — such that
+for all $\alpha \neq \beta$ in $\omega_{\omega+1}$, the intersection $f(\alpha) \cap f(\beta)$
+has cardinality strictly less than $\aleph_\omega$.
+
+Does there exist a **free set** of cardinality $\aleph_{\omega+1}$? That is, a set
+$Y \subseteq \omega_{\omega+1}$ with $|Y| = \aleph_{\omega+1}$ such that for all
+$\alpha \neq \beta$ in $Y$, $\beta \notin f(\alpha)$.
+
+A problem of Erdős and Hajnal [EH74].
+
+## Overview
+
+The key definitions are:
+- `IsSetMapping f`: the set mapping condition — each image has cardinality $\leq \aleph_\omega$
+  and the images are pairwise almost disjoint (intersections have cardinality $< \aleph_\omega$).
+- `IsFreeSet f Y`: the free set condition — $Y$ is free for $f$ if for all distinct
+  $\alpha, \beta \in Y$, $\beta \notin f(\alpha)$.
+- `GCH`: the Generalized Continuum Hypothesis, taken as an abstract hypothesis `Prop`.
+
+The domain is the initial ordinal $\omega_{\omega+1}$ (the $(\omega+1)$-th uncountable
+initial ordinal), realized as a type via `Ordinal.ToType`.
+The target cardinal $\aleph_\omega = $ `ℵ_ ω` and $\aleph_{\omega+1} = $ `ℵ_ (ω + 1)`.
+-/
+
+namespace Erdos1173
+
+/-- The **Generalized Continuum Hypothesis**: for every ordinal `o`, $2^{\aleph_o} = \aleph_{o+1}$.
+
+This is an axiom independent of ZFC; it is taken here as an abstract hypothesis `Prop` to be
+passed explicitly where needed. -/
+def GCH : Prop := ∀ o : Ordinal.{0}, (2 : Cardinal.{0}) ^ ℵ_ o = ℵ_ (Order.succ o)
+
+/-- The **set mapping condition** for a function
+$f : \omega_{\omega+1} \to \mathcal{P}(\omega_{\omega+1})$.
+
+We require:
+1. **Self-avoidance**: $\alpha \notin f(\alpha)$ for every $\alpha$.
+2. Each image $f(\alpha)$ has cardinality at most $\aleph_\omega$.
+3. For any two distinct elements $\alpha \neq \beta$, the intersection
+   $f(\alpha) \cap f(\beta)$ has cardinality strictly less than $\aleph_\omega$.
+
+The self-avoidance condition is the standard requirement on a set mapping in the
+Erdős–Hajnal sense (see the PR description for Problem 1173).
+
+Here the domain is the type `(ω_ (ω + 1)).ToType` corresponding to the initial ordinal
+$\omega_{\omega+1}$, and `Set (ω_ (ω + 1)).ToType` is the powerset. -/
+def IsSetMapping (f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType) : Prop :=
+  (∀ α : (ω_ (ω + 1)).ToType, α ∉ f α) ∧
+  (∀ α : (ω_ (ω + 1)).ToType, #(f α) ≤ ℵ_ ω) ∧
+  (∀ α β : (ω_ (ω + 1)).ToType, α ≠ β → #(f α ∩ f β : Set (ω_ (ω + 1)).ToType) < ℵ_ ω)
+
+/-- A set $Y \subseteq \omega_{\omega+1}$ is **free** for the set mapping $f$ if for all
+distinct $\alpha, \beta \in Y$, we have $\beta \notin f(\alpha)$.
+
+Equivalently: no element of $Y$ is "captured" by the image of any other element of $Y$ under $f$. -/
+def IsFreeSet (f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType)
+    (Y : Set (ω_ (ω + 1)).ToType) : Prop :=
+  ∀ α ∈ Y, ∀ β ∈ Y, α ≠ β → β ∉ f α
+
+/--
+**Erdős–Hajnal Problem 1173**: Assume GCH. Let $f : \omega_{\omega+1} \to [\omega_{\omega+1}]^{\leq
+\aleph_\omega}$ be a set mapping such that $|f(\alpha) \cap f(\beta)| < \aleph_\omega$ for all
+$\alpha \neq \beta$. Does there exist a free set of cardinality $\aleph_{\omega+1}$?
+
+More precisely: under GCH, for every function $f$ satisfying the set mapping condition
+`IsSetMapping f`, must there exist a free set $Y$ with $|Y| = \aleph_{\omega+1}$?
+
+*A problem of Erdős and Hajnal [EH74].*
+
+**Status:** OPEN.
+
+**Formalization notes:**
+- GCH is passed as an explicit hypothesis `hGCH : GCH`, following the convention for
+  set-theoretic problems whose status may depend on additional axioms.
+- The domain $\omega_{\omega+1}$ is encoded via `Ordinal.ToType`, so that `f` has type
+  `(ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType`.
+- `ω` in `ω_ (ω + 1)` is `Ordinal.omega0` (the first infinite ordinal), available via
+  `open scoped Ordinal`. Similarly `ℵ_ ω` and `ℵ_ (ω + 1)` use `open scoped Cardinal`.
+-/
+@[category research open, AMS 3]
+theorem erdos_1173 : answer(sorry) ↔
+    GCH →
+    ∀ f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType,
+      IsSetMapping f →
+      ∃ Y : Set (ω_ (ω + 1)).ToType, IsFreeSet f Y ∧ #Y = ℵ_ (ω + 1) := by
+  sorry
+
+/- ## Sanity checks and auxiliary lemmas -/
+
+/--
+**Cardinality check**: The initial ordinal $\omega_{\omega+1}$ has cardinality $\aleph_{\omega+1}$.
+
+This confirms that the domain type `(ω_ (ω + 1)).ToType` has the right cardinality. -/
+@[category test, AMS 3]
+theorem erdos_1173.sanity.card_domain :
+    #(ω_ (ω + 1)).ToType = ℵ_ (ω + 1) := by
+  rw [mk_toType, Ordinal.card_omega]
+
+/--
+**Cardinality ordering**: $\aleph_\omega < \aleph_{\omega+1}$.
+
+This ensures the free set size $\aleph_{\omega+1}$ is strictly larger than the bound
+$\aleph_\omega$ on image sizes, making the problem non-trivial. -/
+@[category test, AMS 3]
+theorem erdos_1173.sanity.aleph_omega_lt_succ : ℵ_ ω < ℵ_ (ω + 1) := by
+  exact Cardinal.aleph_lt_aleph.mpr (Order.lt_succ ω)
+
+/--
+**Well-definedness of `IsFreeSet`**: The empty set is always a free set for any mapping `f`.
+
+This is a trivial sanity check showing `IsFreeSet` is non-vacuously definable. -/
+@[category test, AMS 3]
+theorem erdos_1173.sanity.empty_is_free
+    (f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType) :
+    IsFreeSet f ∅ := by
+  intro _ hα
+  simp at hα
+
+/--
+**Well-definedness of `IsFreeSet`**: A singleton $\{\alpha\}$ is always a free set for any `f`.
+
+For a singleton, the condition `α ≠ β` with `α, β ∈ {α}` is never satisfied, so the predicate
+holds vacuously. -/
+@[category test, AMS 3]
+theorem erdos_1173.sanity.singleton_is_free
+    (f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType)
+    (α : (ω_ (ω + 1)).ToType) :
+    IsFreeSet f {α} := by
+  intro a ha b hb hab
+  simp only [Set.mem_singleton_iff] at ha hb
+  exact absurd (ha ▸ hb ▸ rfl) hab
+
+/--
+**Monotonicity of `IsFreeSet`**: If $Y$ is a free set and $Z \subseteq Y$, then $Z$ is also free.
+
+Free sets are downward-closed under inclusion. -/
+@[category textbook, AMS 3]
+theorem erdos_1173.variants.free_set_mono
+    (f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType)
+    {Y Z : Set (ω_ (ω + 1)).ToType}
+    (hYZ : Z ⊆ Y) (hY : IsFreeSet f Y) : IsFreeSet f Z := by
+  intro α hα β hβ hne
+  exact hY α (hYZ hα) β (hYZ hβ) hne
+
+/--
+**Relation to the set mapping bound**: Under `IsSetMapping f`, the image of each element
+has cardinality strictly less than $\aleph_{\omega+1}$.
+
+Since $|f(\alpha)| \leq \aleph_\omega < \aleph_{\omega+1}$, each image is strictly smaller
+than the full domain. -/
+@[category textbook, AMS 3]
+theorem erdos_1173.variants.image_lt_aleph_succ
+    (f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType)
+    (hf : IsSetMapping f)
+    (α : (ω_ (ω + 1)).ToType) :
+    #(f α) < ℵ_ (ω + 1) := by
+  exact (hf.2.1 α).trans_lt (Cardinal.aleph_lt_aleph.mpr (Order.lt_succ ω))
+
+end Erdos1173