From eb0afe07f7ae1eb8f08f61734aaab52e553e4c59 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 23 May 2026 20:18:01 +0000
Subject: [PATCH] =?UTF-8?q?feat:=20add=20Jordan=E2=80=93Brouwer=20separati?=
 =?UTF-8?q?on=20eval=20problem?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

§48 of Knill's "Some Fundamental Theorems in Mathematics" (Brouwer,
1912). High-dimensional generalization of the Jordan curve theorem:
for d ≥ 2, the complement in ℝᵈ of a topological (d-1)-sphere has
exactly two connected components. The hypothesis d ≥ 2 is essential
(in d = 1, the (d-1)-sphere is the two-point set {-1, 1} with three
complementary components). Mathlib has Metric.sphere, EuclideanSpace,
ConnectedComponents, Nat.card, but no Jordan–Brouwer separation
theorem, no Alexander duality, no invariance of domain in a form that
would discharge it. Stateable with zero new definitions.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---
 LeanEval/Topology/JordanBrouwer.lean   | 41 ++++++++++++++++++++++++++
 manifests/problems/jordan_brouwer.toml |  9 ++++++
 2 files changed, 50 insertions(+)
 create mode 100644 LeanEval/Topology/JordanBrouwer.lean
 create mode 100644 manifests/problems/jordan_brouwer.toml

diff --git a/LeanEval/Topology/JordanBrouwer.lean b/LeanEval/Topology/JordanBrouwer.lean
new file mode 100644
index 0000000..1231915
--- /dev/null
+++ b/LeanEval/Topology/JordanBrouwer.lean
@@ -0,0 +1,41 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Topology
+
+/-!
+# Jordan–Brouwer separation theorem (L. E. J. Brouwer, 1912)
+
+§48 of Knill's *Some Fundamental Theorems in Mathematics*. The
+high-dimensional generalization of the Jordan curve theorem: for
+`d ≥ 2`, the complement in `ℝᵈ` of any topological `(d−1)`-sphere —
+the image of any continuous injection from the unit `(d−1)`-sphere
+into `ℝᵈ` — has exactly two connected components.
+
+The hypothesis `2 ≤ d` is essential: in dimension `d = 1` the
+`(d−1)`-sphere is the two-point set `{−1, 1}`, whose complement in
+`ℝ` has *three* connected components (left of −1, between −1 and 1,
+right of 1).
+
+Mathlib has `Metric.sphere`, `EuclideanSpace`, `ConnectedComponents`,
+`Nat.card`, but **no Jordan–Brouwer separation theorem**, no Alexander
+duality, no invariance of domain in a form that would discharge it.
+Stateable with no new definitions.
+-/
+
+/-- **Jordan–Brouwer separation theorem.** For `d ≥ 2`, the
+complement in `ℝᵈ` of a topological `(d−1)`-sphere (the image of any
+continuous injection from the unit `(d−1)`-sphere into `ℝᵈ`) has
+exactly two connected components. -/
+@[eval_problem]
+theorem jordan_brouwer (d : ℕ) (_hd : 2 ≤ d)
+    (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1 → EuclideanSpace ℝ (Fin d))
+    (_hcont : Continuous r) (_hinj : Function.Injective r) :
+    Nat.card
+        (ConnectedComponents ((Set.range r)ᶜ : Set (EuclideanSpace ℝ (Fin d)))) =
+      2 := by
+  sorry
+
+end Topology
+end LeanEval
diff --git a/manifests/problems/jordan_brouwer.toml b/manifests/problems/jordan_brouwer.toml
new file mode 100644
index 0000000..fd602ae
--- /dev/null
+++ b/manifests/problems/jordan_brouwer.toml
@@ -0,0 +1,9 @@
+id = "jordan_brouwer"
+title = "Jordan–Brouwer separation theorem"
+test = false
+module = "LeanEval.Topology.JordanBrouwer"
+holes = ["jordan_brouwer"]
+submitter = "Kim Morrison"
+notes = "§48 of Knill's 'Some Fundamental Theorems in Mathematics'. The high-dimensional generalization of the Jordan curve theorem: for d ≥ 2, the complement in ℝᵈ of a topological (d-1)-sphere has exactly two connected components. The hypothesis 2 ≤ d is essential: in dimension d = 1 the (d-1)-sphere is the two-point set {-1, 1}, whose complement in ℝ has three connected components. Mathlib has Metric.sphere, EuclideanSpace, ConnectedComponents, Nat.card, but no Jordan–Brouwer separation theorem, no Alexander duality, no invariance of domain in a form that would discharge it. Stateable with zero new definitions."
+source = "L. E. J. Brouwer, *Beweis des Jordanschen Satzes für den n-dimensionalen Raum*, Math. Annalen 71 (1912) (first proof). Listed as §48 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). No formalization found in any major prover."
+informal_solution = "Modern proofs use singular homology via Alexander duality: H̃_0(ℝᵈ ∖ Σ) ≅ H̃^{d-1}(Σ), and an embedded (d-1)-sphere Σ has H̃^{d-1}(Σ) ≅ ℤ, giving exactly two components. Brouwer's original proof used direct simplicial-approximation arguments without modern homology."