feat: add Schoenflies theorem eval problem

LeanEval/Topology/Schoenflies.lean

@@ -0,0 +1,41 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Topology
+
+/-!
+# Schoenflies theorem (Arthur Moritz Schoenflies, 1906)
+
+§48 of Knill's *Some Fundamental Theorems in Mathematics*. The strong
+form: for every Jordan curve in the plane there is a self-homeomorphism
+of `ℝ²` carrying the curve to the standard unit circle.
+
+This is the faithful encoding of Knill's prose statement that "each
+complementary region is homeomorphic to the disk", which as
+literally written is false for the unbounded region (homeomorphic to
+`ℝ² ∖ closedBall 0 1`, fundamental group `ℤ`, vs. simply connected
+disk). The strong form here implies that the bounded complementary
+region is homeomorphic to the disk, recovering the correct half of
+Knill's claim.
+
+Mathlib has `Metric.sphere`, `EuclideanSpace`, and `Homeomorph`, but
+**no Schoenflies theorem** (`grep -ri 'schoenflies' Mathlib/`: no
+hits), no Jordan curve theorem, and no associated invariance-of-domain
+machinery in a form that would discharge it. Stateable with no new
+definitions.
+-/
+
+/-- **Schoenflies theorem (strong form).** For every Jordan curve in
+the plane there is a self-homeomorphism of `ℝ²` carrying the curve to
+the standard unit circle. -/
+@[eval_problem]
+theorem schoenflies
+    (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 → EuclideanSpace ℝ (Fin 2))
+    (_hcont : Continuous r) (_hinj : Function.Injective r) :
+    ∃ h : EuclideanSpace ℝ (Fin 2) ≃ₜ EuclideanSpace ℝ (Fin 2),
+      h '' Set.range r = Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by
+  sorry
+
+end Topology
+end LeanEval

manifests/problems/schoenflies.toml

@@ -0,0 +1,9 @@
+id = "schoenflies"
+title = "Schoenflies theorem"
+test = false
+module = "LeanEval.Topology.Schoenflies"
+holes = ["schoenflies"]
+submitter = "Kim Morrison"
+notes = "§48 of Knill's 'Some Fundamental Theorems in Mathematics'. Strong form: every Jordan curve in the plane is the image of the unit circle under some self-homeomorphism of ℝ². This is the faithful encoding of Knill's prose statement 'each complementary region is homeomorphic to the open disk' — which as literally written is false for the unbounded region (homeomorphic to ℝ² ∖ closedBall 0 1, fundamental group ℤ, not simply connected). The strong form implies the bounded region is homeomorphic to the open disk. Mathlib has Metric.sphere, EuclideanSpace, and Homeomorph, but no Schoenflies theorem (`grep -ri 'schoenflies' Mathlib/`: no hits), no Jordan curve theorem, no invariance-of-domain machinery in a form that would discharge it. Stateable with zero new definitions."
+source = "A. M. Schoenflies, *Beiträge zur Theorie der Punktmengen III*, Math. Annalen 62 (1906) (first proof, with gaps); rigorous proofs by L. Antoine (1921), L. E. J. Brouwer (1909–10). 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 = "Classical proof: (i) the Jordan curve theorem gives the inside and outside regions; (ii) Riemann mapping for the bounded inside extends to a homeomorphism of the closed disk by Carathéodory's theorem on prime ends; (iii) a parallel construction handles the outside; (iv) the two homeomorphisms patch along the curve to a homeomorphism of ℝ²."