The Jordan–Schönflies theorem

The quantitative stage recursion supplies the interior homeomorphism. Its fresh target nets give a dense source anchor set; radial mesh spokes supply the boundary germs, and finite-stage nonboundary edge paths supply matched crosscuts. These data prove HasLimitHomeomorphism, then SquareExtension, and finally the relative Jordan–Schönflies theorem.

Blueprint

The declarations below close thm:square-extension and thm:main; the intervening square reduction, closed-interior, pointed, and exterior extensions are supplied by Endgame.lean.

theorem Schoenflies.hasLimitHomeomorphism : HasLimitHomeomorphism

All four inputs to boundary continuity are supplied by the prescribed quantitative stage sequence.

theorem Schoenflies.squareExtension : SquareExtension

thm:square-extension. Every homeomorphism from a Jordan curve to the boundary of the model square extends over the corresponding closed domains.

theorem Schoenflies.jordan_schoenflies {C C' : Set Plane} {f g : Plane → Plane} (hC : IsJordanCurve C) (hC' : IsJordanCurve C') (hfg : IsHomeoOn f g C C') : ∃ (F : Plane → Plane) (G : Plane → Plane), IsHomeoOn F G Set.univ Set.univ ∧ Set.EqOn F f C

The relative Jordan–Schönflies theorem, in the unbundled IsHomeoOn form.

theorem Schoenflies.jordan_schoenflies_homeomorph {C C' : Set Plane} {f g : Plane → Plane} (hC : IsJordanCurve C) (hC' : IsJordanCurve C') (hfg : IsHomeoOn f g C C') : ∃ (F : Plane ≃ₜ Plane), Set.EqOn (⇑F) f C

The relative Jordan–Schönflies theorem, packaged as a plane self-homeomorphism.

theorem Schoenflies.jordan_schoenflies_of_homeomorph {C C' : Set Plane} (hC : IsJordanCurve C) (hC' : IsJordanCurve C') (e : ↑C ≃ₜ ↑C') : ∃ (F : Plane ≃ₜ Plane), ∀ (z : ↑C), F ↑z = ↑(e z)

The blueprint's bundled statement. Every homeomorphism between two Jordan curves extends to a self-homeomorphism of the plane.