The polygonal Jordan curve theorem

Theorem 2.3: the complement of a simple closed polygon has exactly two regions, one bounded and one unbounded, and each has the polygon as its frontier. Moreover the crossing parity of §2 is 1 on the bounded region and 0 on the unbounded one.

The three inputs, and where each is spent

• Lemma 1.8, the collar (Schoenflies.StripData, StripData.local_two_sided, StripData.carrier_subset_closure_sideL). It supplies the two tracks N_L, N_R: connected, disjoint, off the curve, together filling N ∖ C, and each with the whole curve in its closure.
• Lemma 1.3, the nearest-point segment (Plane.notMem_of_mem_segment_of_isMinOn). It gets an arbitrary point of the complement onto a track: walk from it to a nearest point of the curve; the walk misses the curve, and its final stretch is inside the collar.
• Lemma 2.2, crossing parity (ClosedPolygon.parity_eq_of_mem_connectedComponentIn_carrier, ClosedPolygon.parity_flip_carrier). It keeps the two tracks apart: they cannot be joined inside the complement, because a point just before and a point just after an edge differ in parity and parity is constant on a connected subset of the complement.

Blueprint

• Schoenflies.ClosedPolygon.exists_opposite_parity_sides, …parity_ne_of_mem_sides, …connectedComponentIn_ne_of_mem_sides — the two tracks of the collar carry different parities, hence lie in different components. The "at least two" half.
• Schoenflies.ClosedPolygon.exists_mem_sides_connectedComponentIn, …connectedComponentIn_eq_of_notMem — every point of the complement lies in the component of a point of a track. The "at most two" half.
• Schoenflies.ClosedPolygon.isSeparating_carrier — Theorem 2.3, in the form Definition 2.4 asks for: IsSeparating P.carrier. With it come inside P.carrier and outside P.carrier as the blueprint's Int(C) and Ext(C), and the whole IsSeparating API of Schoenflies/CrosscutCells.lean.
• Schoenflies.ClosedPolygon.connectedComponentIn_eq_inside_or_outside — "exactly two regions", explicitly: the component of any point off the polygon is one of the two named regions.
• Schoenflies.ClosedPolygon.parity_eq_one_of_mem_inside, …parity_eq_zero_of_mem_outside — the last sentence of Theorem 2.3, π_C = 1 inside and π_C = 0 outside, for every admissible ray direction, not just for one chosen at the start.
• Schoenflies.ClosedPolygon.polygonal_jordan — the same theorem with IsSeparating unfolded, for a reader who wants the statement without the definition.
• Schoenflies.isSeparating_unitTriangle — non-vacuity: the whole chain applies to the one polygon the development constructs.

Two facts restated

isBounded_closedSquare and not_isBounded_beyondSquare below are stated private. They are not new: they exist as Graph.isBounded_closedSquare and Graph.not_isBounded_beyondSquare in Schoenflies/Graph/OuterFace.lean. Neither has any graph content — they are plane facts about Schoenflies.Plane.closedSquare whose home is Schoenflies/Bounded.lean — and importing the whole plane-graph layer into the polygonal Jordan curve theorem, which every later graph argument depends on, would invert the layering. They are private so that the duplicate names cannot collide when the integrator hoists the originals.

Two plane facts about squares

See the module docstring: these belong in Schoenflies/Bounded.lean and are restated here only to keep the graph layer out of the import graph of Theorem 2.3.

Small arithmetic and topology helpers

theorem Schoenflies.ClosedPolygon.isClosed_carrier {m : ℕ} (P : ClosedPolygon m) : IsClosed P.carrier

theorem Schoenflies.ClosedPolygon.isOpen_compl_carrier {m : ℕ} (P : ClosedPolygon m) : IsOpen P.carrierᶜ

theorem Schoenflies.ClosedPolygon.carrier_nonempty {m : ℕ} (P : ClosedPolygon m) : P.carrier.Nonempty

theorem Schoenflies.ClosedPolygon.sideL_subset_compl {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : D.sideL ⊆ P.carrierᶜ

theorem Schoenflies.ClosedPolygon.sideR_subset_compl {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : D.sideR ⊆ P.carrierᶜ

theorem Schoenflies.ClosedPolygon.det_tang_ne_zero {m : ℕ} {P : ClosedPolygon m} {u : Plane} (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) (i : ZMod (m + 3)) : (P.tang i).det u ≠ 0

No edge is parallel to an admissible ray direction. "No edge is horizontal" says exactly that the two ends of an edge are at different heights, which is that the edge's tangent and the ray direction span the plane.

At least two regions: the two tracks are separated by one crossing

The blueprint: "Choose a sufficiently small disk B around an interior point of an edge, and reference points z_L ∈ B ∩ N_L, z_R ∈ B ∩ N_R in its two components. The two reference points have opposite parity."

The disk is the one of StripData.local_two_sided; the two reference points are the two points just before and just after the midpoint of the edge in the ray direction, which is what makes parity_flip_carrier applicable to them. That they land in the two different tracks is read off the sign of their transverse coordinate det (tang i) (· - vertex i), and the two signs are opposite and nonzero because det (tang i) u ≠ 0 — the edge is not parallel to the ray.

theorem Schoenflies.ClosedPolygon.exists_opposite_parity_sides {m : ℕ} (P : ClosedPolygon m) (D : StripData P) (i : ZMod (m + 3)) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) : ∃ zL ∈ D.sideL, ∃ zR ∈ D.sideR, parity u P.pieces zL ≠ parity u P.pieces zR

The two tracks of the collar carry different parities. The witnesses are a point just before and a point just after the midpoint of the edge i in the ray direction: they lie in the two different tracks, and the crossing count changes by one between them.

theorem Schoenflies.ClosedPolygon.parity_eq_of_mem_sideL {m : ℕ} (P : ClosedPolygon m) (D : StripData P) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x y : Plane} (hx : x ∈ D.sideL) (hy : y ∈ D.sideL) : parity u P.pieces x = parity u P.pieces y

The crossing parity is constant on the left track: it is connected and misses the polygon.

theorem Schoenflies.ClosedPolygon.parity_eq_of_mem_sideR {m : ℕ} (P : ClosedPolygon m) (D : StripData P) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x y : Plane} (hx : x ∈ D.sideR) (hy : y ∈ D.sideR) : parity u P.pieces x = parity u P.pieces y

The crossing parity is constant on the right track.

theorem Schoenflies.ClosedPolygon.parity_ne_of_mem_sides {m : ℕ} (P : ClosedPolygon m) (D : StripData P) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x y : Plane} (hx : x ∈ D.sideL) (hy : y ∈ D.sideR) : parity u P.pieces x ≠ parity u P.pieces y

The two tracks of the collar have opposite parity, whichever points of them are chosen. This is the "at least two regions" half of Theorem 2.3: no connected subset of the complement meets both tracks, since parity is constant on such a subset.

theorem Schoenflies.ClosedPolygon.connectedComponentIn_ne_of_mem_sides {m : ℕ} (P : ClosedPolygon m) (D : StripData P) {x y : Plane} (hx : x ∈ D.sideL) (hy : y ∈ D.sideR) : connectedComponentIn P.carrierᶜ x ≠ connectedComponentIn P.carrierᶜ y

The two tracks lie in different components of the complement.

At most two regions: walk to the nearest point of the polygon

The blueprint: "Let x ∉ C, and choose a nearest point a ∈ C. By Lemma 1.3, [x, a) avoids C. Its final portion lies in N_L or N_R, and that track is connected. Hence x lies in the component of either z_L or z_R."

theorem Schoenflies.ClosedPolygon.exists_mem_sides_connectedComponentIn {m : ℕ} (P : ClosedPolygon m) (D : StripData P) {x : Plane} (hx : x ∉ P.carrier) : ∃ y ∈ D.sideL ∪ D.sideR, connectedComponentIn P.carrierᶜ x = connectedComponentIn P.carrierᶜ y

At most two regions. Every point of the complement lies in the component of a point of one of the two tracks: walk towards a nearest point of the polygon — Lemma 1.3 says the walk misses the polygon — and stop just short of it, inside the collar.

theorem Schoenflies.ClosedPolygon.connectedComponentIn_eq_of_notMem {m : ℕ} (P : ClosedPolygon m) (D : StripData P) {zL zR : Plane} (hzL : zL ∈ D.sideL) (hzR : zR ∈ D.sideR) {x : Plane} (hx : x ∉ P.carrier) : connectedComponentIn P.carrierᶜ x = connectedComponentIn P.carrierᶜ zL ∨ connectedComponentIn P.carrierᶜ x = connectedComponentIn P.carrierᶜ zR

Every point of the complement lies in the component of one of two fixed reference points, one on each track. This is exists_mem_sides_connectedComponentIn with the track collapsed to a point, which is possible because each track is connected.

Packaging: from "exactly two components" to IsSeparating

Schoenflies/CrosscutCells.lean defines inside C and outside C as the union of the bounded and of the unbounded components of Cᶜ, without any separation hypothesis, and Definition 2.4 is the assertion that each of the two is a single region with boundary C. So the last step of Theorem 2.3 is to identify the two components found above with inside C and outside C, and that identification needs no case analysis on which of them is which: the one that swallows the outside of a containing square is the unbounded one by definition, and the other is caught inside the square.

theorem Schoenflies.ClosedPolygon.isSeparating_carrier {m : ℕ} (P : ClosedPolygon m) : IsSeparating P.carrier

The polygonal Jordan curve theorem (Theorem 2.3), in the form Definition 2.4 asks for. The complement of a simple closed polygon has exactly two regions, one bounded and one unbounded, and each has the polygon as its frontier.

The bounded region is Schoenflies.inside P.carrier and the unbounded one Schoenflies.outside P.carrier; everything the blueprint writes Int(C) and Ext(C) for, and the whole IsSeparating API of Schoenflies/CrosscutCells.lean, comes with this statement.

theorem Schoenflies.ClosedPolygon.connectedComponentIn_eq_inside_or_outside {m : ℕ} (P : ClosedPolygon m) {x : Plane} (hx : x ∉ P.carrier) : connectedComponentIn P.carrierᶜ x = inside P.carrier ∨ connectedComponentIn P.carrierᶜ x = outside P.carrier

Exactly two regions, explicitly: the component of any point off the polygon is one of the two named regions.

The parity values

The blueprint: "take a point q whose coordinate along the ray exceeds that of every point of the compact set C. No edge crosses the level line through q beyond q, so π_C(q) = 0; and q lies in the unbounded region." Here q is chosen to be beyond a containing square as well, so that it visibly lies in the unbounded region: the outside of that square is connected, misses the polygon, and is unbounded.

theorem Schoenflies.ClosedPolygon.parity_eq_zero_of_mem_outside {m : ℕ} (P : ClosedPolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x : Plane} (hx : x ∈ outside P.carrier) : parity u P.pieces x = 0

π_C = 0 on the unbounded region. Every admissible ray direction gives the same answer.

theorem Schoenflies.ClosedPolygon.parity_eq_one_of_mem_inside {m : ℕ} (P : ClosedPolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x : Plane} (hx : x ∈ inside P.carrier) : parity u P.pieces x = 1

π_C = 1 on the bounded region. The two tracks of the collar have opposite parity and lie in the two different regions, so the region that is not the unbounded one carries the parity that is not 0.

The theorem, unpacked

theorem Schoenflies.ClosedPolygon.polygonal_jordan {m : ℕ} (P : ClosedPolygon m) : IsJordanCurve P.carrier ∧ IsPolygonal P.carrier ∧ IsOpen (inside P.carrier) ∧ IsOpen (outside P.carrier) ∧ IsConnected (inside P.carrier) ∧ IsConnected (outside P.carrier) ∧ Disjoint (inside P.carrier) (outside P.carrier) ∧ inside P.carrier ∪ outside P.carrier = P.carrierᶜ ∧ Bornology.IsBounded (inside P.carrier) ∧ ¬Bornology.IsBounded (outside P.carrier) ∧ (∀ x ∉ P.carrier, connectedComponentIn P.carrierᶜ x = inside P.carrier ∨ connectedComponentIn P.carrierᶜ x = outside P.carrier) ∧ frontier (inside P.carrier) = P.carrier ∧ frontier (outside P.carrier) = P.carrier

The polygonal Jordan curve theorem (Theorem 2.3), spelled out. The complement of a simple closed polygon is the disjoint union of two nonempty connected open sets, one bounded and one unbounded, each a connected component of the complement and each with the polygon as its frontier.

theorem Schoenflies.isSeparating_unitTriangle : IsSeparating unitTriangle.carrier

Non-vacuity. The triangle with vertices (0,0), (1,0), (0,1) separates the plane.

Schoenflies.unitTriangle is the one ClosedPolygon the development exhibits, and this is the check that the whole chain applies to it: the collar constants exists_stripData, the collar itself, the crossing parity, and the separation above. Without it every statement in this file would formally be a statement about a structure with no known inhabitant.