feat: add Jordan–Brouwer separation eval problem

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

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