Schoenflies theorem

schoenflies — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **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. -/
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

Informal solution sketch

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 ℝ².

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.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: schoenflies
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.