The Jordan curve theorem

The complement of a Jordan curve has exactly two regions, one bounded and one unbounded, and both have the curve as their boundary. That is Schoenflies.IsSeparating C — the very predicate Schoenflies/CrosscutCells.lean introduces and Schoenflies.ClosedPolygon.polygonal_jordan establishes for a polygon — so every consumer of the polygonal case applies verbatim to the general one, inside C and outside C included.

Everything here takes one hypothesis, carried explicitly through every statement that needs it:

harc : ∀ A : Set Plane, IsArc A → IsConnected Aᶜ

which is thm:arc-complement, the complement of a simple arc is connected. Nothing else is assumed; in particular no part of thm:jordan itself is.

The two theorems

lem:accessible-dense (Schoenflies.accessible_dense) says the points of C reachable from a fixed x ∉ C by a polygonal arc meeting C only at its endpoint are dense in C. Its proof is the blueprint's: delete a small open subarc J₀, leaving a simple arc whose complement is connected by harc; join x there to a point of another component of Cᶜ; the joining chain must cross C, and it can only do so inside J₀.

thm:jordan (Schoenflies.IsJordanCurve.isSeparating) then needs "at most two components", which is Schoenflies.not_three_components, and the boundary clause, which is lem:accessible-dense again: an accessible point is a limit of the region it is accessible from, so C lies in the closure of each region and, being disjoint from both, in each frontier.

Three places where this departs from the blueprint's route

The first meeting is taken on a vertex list, not on a parametrisation. Schoenflies.exists_first_meeting recurses on the list: on the first segment the first hit is the infimum of the hitting parameters, and if the first segment misses the obstacle it is swallowed by the component of the start and the recursion moves on. It returns the initial chain, so both consumers — the accessibility of the meeting point, and the third branch of a tripod — read off the same lemma.

The tripod is built without a graph. The blueprint overlays the three access arcs (lem:polygonal-overlay), takes a minimal connected spanning subgraph, and extracts its unique degree-three vertex by lem:three-leaf-tree. Schoenflies.exists_tripod instead joins the first two terminals by a crosscut (lem:accessible-endpoints), runs a chain from the third terminal to that crosscut, and takes the first meeting: that meeting point is the branch vertex, and cutting the crosscut there (IsArcBetween.exists_split) gives the other two branches. Neither Schoenflies.polygonal_overlay nor Graph.IsTree.three_leaves is used.

The nine terminals are chosen in nine prescribed parameter windows. The blueprint chooses them distinct — proving that a dense set meets a nonempty relatively open subarc infinitely often — and then orders the three on each closed arc Q_j to find the middle one y_j. Schoenflies.exists_windows supplies nine pairwise separated windows inside (0,1), in three blocks of three; distinctness is then disjointness of the windows, the middle terminal of a block is always the one with row index 1, and no order on the curve is ever constructed. The blueprint's Q_j never appears: only the parameter blocks [t 0 j, t 2 j] do.

Blueprint

• Schoenflies.exists_first_meeting_segment, Schoenflies.exists_first_meeting, Schoenflies.exists_arc_to_first_meeting, Schoenflies.polyAccessible_first_meeting — the first-meeting machinery lem:accessible-dense and thm:jordan both run on. General enough to be hoisted if a second module needs it.
• Schoenflies.PolyAccessible.mem_closure — an accessible point of ∂Ω lies in closure Ω.
• Schoenflies.IsLoop.compl_openArc — lem:jordan-circle in the form used here: the curve minus an open subarc is the complementary closed arc.
• Schoenflies.exists_polyAccessible_openArc, Schoenflies.accessible_dense — lem:accessible-dense, in the parameter form the proof produces and in the closure form.
• Schoenflies.exists_tripod — the three internally disjoint branches of the blueprint's T_i, at the H5 step of thm:jordan.
• Schoenflies.exists_windows, Schoenflies.uIcc_inter_uIcc_mid — the choice of the nine terminals and the middle-point bookkeeping that replaces "order p_{1j}, p_{2j}, p_{3j} along Q_j".
• Schoenflies.not_three_components — the K(3,3) half of thm:jordan, through Graph.IsArcK33.elim (cor:k33-subdivision).
• Schoenflies.subset_closure_of_accessible_dense, Schoenflies.IsJordanCurve.isSeparating — thm:jordan.

The first meeting of a polygonal chain with a closed set

A chain that starts off a closed obstacle S and eventually hits it has a first hit, and the piece of the chain before it never leaves the component of U its start lies in. This is the only reason lem:accessible-dense produces an accessible point rather than merely a point of the curve, and it is proved by structural recursion on the vertex list: on the first segment the first hit is the infimum of the hitting parameters, and if the first segment misses S the segment itself is swallowed by the component and the recursion moves on.

theorem Schoenflies.exists_first_meeting_segment {S U : Set Plane} {u v : Plane} (hS : IsClosed S) (hUS : Disjoint U S) (hu : u ∈ U) (hsub : segment ℝ u v ⊆ U ∪ S) (hmeet : (segment ℝ u v ∩ S).Nonempty) : ∃ p ∈ segment ℝ u v ∩ S, segment ℝ u p ⊆ segment ℝ u v ∧ segment ℝ u p \ {p} ⊆ connectedComponentIn U u

The first meeting on a single segment. The parameter interval of the hits is closed and bounded below, so it has a least element; before it the segment stays in U, hence in the component of U carrying the near endpoint.

theorem Schoenflies.exists_first_meeting {S U : Set Plane} (hS : IsClosed S) (hUS : Disjoint U S) (u : Plane) (vs : List Plane) : u ∈ U → poly (u :: vs) ⊆ U ∪ S → (poly (u :: vs) ∩ S).Nonempty → ∃ (ws : List Plane), ∃ p ∈ poly (u :: vs) ∩ S, poly (u :: ws) ⊆ poly (u :: vs) ∧ (u :: ws).getLast ⋯ = p ∧ poly (u :: ws) \ {p} ⊆ connectedComponentIn U u

The first meeting of a polygonal chain with a closed set. A chain that starts in U, runs inside U ∪ S and meets the closed set S has an initial piece — again a chain from the same start — that reaches S exactly at its far end and otherwise stays inside the component of U carrying the start.

The chain is returned as u :: ws, so that "same start" is definitional and no List.head obligation is ever produced.

theorem Schoenflies.exists_arc_to_first_meeting {S U : Set Plane} (hS : IsClosed S) (hUS : Disjoint U S) {u : Plane} {vs : List Plane} (hu : u ∈ U) (hsub : poly (u :: vs) ⊆ U ∪ S) (hmeet : (poly (u :: vs) ∩ S).Nonempty) : ∃ p ∈ poly (u :: vs) ∩ S, ∃ (P : Set Plane), IsPolygonal P ∧ IsArcBetween P p u ∧ P ⊆ poly (u :: vs) ∧ P \ {p} ⊆ connectedComponentIn U u

The first meeting, as a simple arc. The initial piece of the chain is re-extracted as a simple polygonal arc from the first meeting point back to the start; it meets S only at that point, and everything else on it stays in the component of U carrying the start.

This is the form both consumers want: lem:accessible-dense reads off the accessibility of p, and the tripod construction of thm:jordan needs the arc itself.

theorem Schoenflies.polyAccessible_first_meeting {S U : Set Plane} (hS : IsClosed S) (hUS : Disjoint U S) {u : Plane} {vs : List Plane} (hu : u ∈ U) (hsub : poly (u :: vs) ⊆ U ∪ S) (hmeet : (poly (u :: vs) ∩ S).Nonempty) : ∃ p ∈ poly (u :: vs) ∩ S, PolyAccessible (connectedComponentIn U u) p

The accessibility statement lem:accessible-dense produces: the first meeting point is polygonally accessible from the component of U the chain started in.

An accessible point is a limit of the region

The half of thm:jordan's boundary clause that lem:accessible-dense supplies: an accessible point of the curve is in the closure of the region it is accessible from. The access chain is connected and carries a point of the region, so the accessible point is not isolated on it.

theorem Schoenflies.PolyAccessible.mem_closure {Ω : Set Plane} {a : Plane} (h : PolyAccessible Ω a) (ha : a ∉ Ω) : a ∈ closure Ω

An accessible point off the region lies in its closure.

The curve with an open subarc deleted

lem:jordan-circle's "two points cut the curve into two arcs" in the form lem:accessible-dense consumes it: the complement in the curve of a relatively open subarc is one closed arc. The proof is the parameter bookkeeping of Schoenflies/TwoArcs.lean — no new topology.

theorem Schoenflies.IsLoop.compl_openArc {f : ℝ → Plane} (hf : IsLoop f) {a b : ℝ} (ha : a ∈ unitInterval) (hb : b ∈ unitInterval) (hab : a < b) : f '' unitInterval \ f '' Set.Ioo a b = f '' Set.Icc 0 a ∪ f '' Set.Icc b 1

The curve minus an open subarc is the complementary closed arc.

Density of accessible points, lem:accessible-dense

The blueprint's proof verbatim: shrink the given relatively open arc to one whose closure is inside it, delete it from the curve to leave a simple arc, join x to a point of another component in the (connected) complement of that arc by a polygonal chain, and take the first meeting of the chain with the curve.

The shrinking step is done on parameters. Instead of "an open arc J₀ with closure inside J" the statement below takes the open subarc f '' Ioo a b with 0 < a < b < 1, which is already strictly inside the parameter interval; every relatively open piece of the curve contains such a subarc (Schoenflies.basic_piece_inside_ball supplies one inside any ball), and that is all the blueprint's J₀ is for.

theorem Schoenflies.exists_polyAccessible_openArc (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) {f : ℝ → Plane} (hf : IsLoop f) {x : Plane} (hx : x ∉ f '' unitInterval) {a b : ℝ} (ha : 0 < a) (hab : a < b) (hb : b < 1) : ∃ p ∈ f '' Set.Ioo a b, PolyAccessible (connectedComponentIn (f '' unitInterval)ᶜ x) p

lem:accessible-dense, in the parameter form the proof produces. Every open subarc strictly inside the parameter interval carries a point accessible from the component of x.

harc is thm:arc-complement: the complement of a simple arc is connected.

theorem Schoenflies.accessible_dense {C : Set Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) {x : Plane} (hx : x ∉ C) : C ⊆ closure {p : Plane | p ∈ C ∧ PolyAccessible (connectedComponentIn Cᶜ x) p}

lem:accessible-dense (density of accessible points). The points of C reachable from x by a polygonal arc meeting C only at its endpoint are dense in C.

The tripod at a component

The blueprint builds the three internally disjoint branches from x_i to the three terminals by overlaying the three access arcs, taking a minimal connected spanning subgraph, and reading off its unique degree-three vertex (lem:three-leaf-tree). The construction below reaches the same object without a graph: join the first two terminals by a crosscut — a simple polygonal arc meeting the curve exactly at its two endpoints (lem:accessible-endpoints in crosscut form) — then run a chain from the third terminal into the region and on to a point of that crosscut, and take its first meeting with the crosscut. That meeting point is the branch vertex; cutting the crosscut there (IsArcBetween.exists_split) supplies the other two branches.

The output is the same three internally disjoint arcs, with the same two properties every later step uses: each meets the curve only at its terminal, and two of them meet only at the branch vertex.

theorem Schoenflies.exists_tripod {C Ω : Set Plane} (hΩopen : IsOpen Ω) (hΩconn : IsPreconnected Ω) (hdisj : Disjoint Ω C) {a b c : Plane} (haC : a ∈ C) (hbC : b ∈ C) (hcC : c ∈ C) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (ha : PolyAccessible Ω a) (hb : PolyAccessible Ω b) (hc : PolyAccessible Ω c) : ∃ x ∈ Ω, ∃ (Ta : Set Plane) (Tb : Set Plane) (Tc : Set Plane), IsArcBetween Ta x a ∧ IsArcBetween Tb x b ∧ IsArcBetween Tc x c ∧ Ta \ {a} ⊆ Ω ∧ Tb \ {b} ⊆ Ω ∧ Tc \ {c} ⊆ Ω ∧ Ta ∩ Tb ⊆ {x} ∧ Ta ∩ Tc ⊆ {x} ∧ Tb ∩ Tc ⊆ {x}

Three internally disjoint arcs from one point of a region to three accessible points of its complementary set. The blueprint's T_i with its three branches, for Ω the i-th component and the three points the terminals p_{ij}.

Nine parameter windows

The blueprint chooses the nine terminals p_{ij} distinct and then orders the three on each arc Q_j to find the middle one y_j. Choosing them in nine prescribed, pairwise separated parameter windows does both jobs at once: distinctness is disjointness of the windows, and the middle one is always the terminal of the middle index. No order on the curve is ever constructed.

The windows are ((6j + 2i + 2)/24, (6j + 2i + 3)/24), which for i, j < 3 are nine disjoint intervals inside (0, 1), ordered lexicographically by (j, i).

theorem Schoenflies.exists_windows : ∃ (w : Fin 3 → Fin 3 → ℝ), (∀ (i j : Fin 3), 0 < w i j) ∧ (∀ (i j : Fin 3), w i j + 1 / 24 < 1) ∧ ∀ (i j k l : Fin 3), j = l ∧ ↑i < ↑k ∨ ↑j < ↑l → w i j + 1 / 24 ≤ w k l

Nine parameter windows strictly inside (0, 1), in blocks of three: increasing the row index i within a block, or the block index j, moves past the end of the current window.

theorem Schoenflies.uIcc_inter_uIcc_mid {r s m : ℝ} (hr : r ≤ m) (hs : m ≤ s) : Set.uIcc r m ∩ Set.uIcc s m ⊆ {m}

Two closed intervals sharing the endpoint m, one on each side of it, meet only there.

At most two components

The heart of thm:jordan. Three components would give three tripods, whose nine branches, extended along the curve to the three middle terminals, are a plane K(3,3) subdivision — excluded by cor:k33-subdivision (Graph.IsArcK33.elim).

theorem Schoenflies.not_three_components {C : Set Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) {q : Fin 3 → Plane} (hqC : ∀ (i : Fin 3), q i ∉ C) (hqne : ∀ (i k : Fin 3), i ≠ k → connectedComponentIn Cᶜ (q i) ≠ connectedComponentIn Cᶜ (q k)) : False

Three points of the complement of a Jordan curve cannot lie in three distinct components.

The Jordan curve theorem

Stated as IsSeparating C, the predicate Schoenflies/CrosscutCells.lean introduces and Schoenflies.ClosedPolygon.polygonal_jordan establishes in the polygonal case. Unfolding it, that is exactly the blueprint's statement: inside C and outside C are each a single region, one bounded and one unbounded (IsSeparating.isBounded_inside, IsSeparating.not_isBounded_outside), and both have C as boundary. Every consumer written against the polygonal case therefore applies verbatim.

theorem Schoenflies.subset_closure_of_accessible_dense {C : Set Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) {x : Plane} (hx : x ∉ C) : C ⊆ closure (connectedComponentIn Cᶜ x)

A point of the curve is in the closure of any region it is accessible from — the reverse inclusion of the boundary clause, packaged for both regions at once.

theorem Schoenflies.IsJordanCurve.isSeparating {C : Set Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) : IsSeparating C

thm:jordan (the Jordan curve theorem). The complement of a Jordan curve has exactly two regions, one bounded and one unbounded, and both have the curve as their boundary.

harc is thm:arc-complement.