Theorem 2.8: two-sided polygonal crosscuts

A crosscut P of a simple closed polygon C cuts one of the two regions of ℝ² ∖ C into exactly two, bounded by the two curves Jᵢ = Aᵢ ∪ P; and ℝ² ∖ (C ∪ P) then has exactly three regions, with boundaries C, J₁, J₂.

One theorem, not two

The blueprint splits the statement into case (a), the crosscut inside C, and case (b), the crosscut outside. The two cases differ only in which region of ℝ² ∖ Jᵢ is the new cell: in case (a) it is Int(Jᵢ) for both i, while in case (b) it is Ext(J₁) for one index and Int(J₂) for the other, and which is which is not determined by the data. What is uniform is the description "the region of ℝ² ∖ Jᵢ on the far side from a point y of the region of ℝ² ∖ C that the crosscut does not enter". So the whole theorem is proved once, for

farRegion J y  =  the region of `ℝ² ∖ J` that does not contain `y`,

and the two cases of the blueprint are then read off by identifying farRegion with inside or with outside (IsSeparating.farRegion_eq_inside, …_eq_outside). A reference point y in the untouched region is the one extra datum this costs, and it is exactly the datum the blueprint hides in the phrase "let Ω be the region containing P ∖ {p, q}".

Exhaustion is pure parity, in both cases at once

Lemma 2.6 (Schoenflies.crosscut_cells) already exhibits the two cells as components of Ω ∖ P. All that Theorem 2.8 adds is that there are no others, and the blueprint reads this off Lemma 2.7. Here the reading is uniform. Write πJ for the crossing count of a curve J. For points x, y off J — Theorem 2.3 —

`x` and `y` lie in different regions of `ℝ² ∖ J`  ↔  `πJ(x) ≠ πJ(y)`,

which is ClosedPolygon.parity_ne_iff_mem_farRegion. Lemma 2.7 gives πJ₁ + πJ₂ = πC at every point, so subtracting the identity at y from the identity at x turns "x is separated from y by C" into "x is separated from y by exactly one of J₁, J₂" — IsPolygonalCrosscut.separates_xor, whose entire proof is sixteen cases of ZMod 2 arithmetic. No case distinction on inside/outside is made anywhere.

The hypotheses, bundled

IsPolygonalCrosscut C J₁ J₂ K a k y collects the seven hypotheses of the theorem: the two curves of the split carry the right edges (Schoenflies.SameEdges, from Lemma 2.7), the crosscut meets C only in points common to both arcs, and the reference point y lies off C in a region the crosscut does not enter. It is closed under swapping the two arcs (IsPolygonalCrosscut.symm), which is why every statement below is proved for index 1 only.

Realizing J₁ and J₂ as ClosedPolygons is the consumer's job, exactly as in Lemma 2.7 — see the note there about the corner field. Nothing in this file inspects corner.

Blueprint

• farRegion, IsSeparating.isRegionPair_farRegion, IsSeparating.farRegion_eq_inside, IsSeparating.farRegion_eq_outside — the blueprint's Ω, Ω†, Vᵢ and Wᵢ named as functions of a reference point instead of by an existential.
• ClosedPolygon.arc — the arcs A₁, A₂ of Theorem 2.8, as sets; …vertex_mem_arc, …vertex_add_mem_arc, …endpoints_subset_arc, …endpoints_subset_arc' — the two cut vertices lie on both arcs, which is what "the crosscut meets C only in its endpoints" has to say to be usable.
• ClosedPolygon.parity_ne_iff_mem_farRegion — Theorem 2.3 read as a separation criterion.
• IsPolygonalCrosscut — the hypotheses of Theorem 2.8; IsPolygonalCrosscut.of_endpoints is the constructor a consumer should use, and IsPolygonalCrosscut.symm swaps the two arcs.
• IsPolygonalCrosscut.separates_xor — Lemma 2.7's "consequently", in the uniform form.
• IsPolygonalCrosscut.region_eq, …cells_disjoint, …cells_ne, …cell_isComponent₁/₂, …frontier_cell₁/₂, …closure_cell_inter₁/₂ — the two cells of Ω ∖ P.
• IsPolygonalCrosscut.inside_diff_eq — Theorem 2.8(a).
• IsPolygonalCrosscut.outside_diff_eq, …inside_exactly_one — Theorem 2.8(b).
• IsPolygonalCrosscut.compl_eq, …isComponent, …near_isComponent, …cell_isComponent_compl₁/₂, …cell_ne_near₁/₂, …frontier_near — "in either case ℝ² ∖ (C ∪ P) has exactly three regions, with boundaries C, J₁, J₂".
• polygonal_crosscut — Theorem 2.8, bundled.

The region on the far side of a point

The blueprint names the four regions in play — Ω, Ω†, Wᵢ, Vᵢ — by their relation to one another: Ω† is the region of ℝ² ∖ C the crosscut does not enter, and Vᵢ is the region of ℝ² ∖ Jᵢ on the other side of Jᵢ from Ω†. Fixing a point y ∈ Ω† turns all four into functions of the data.

def Schoenflies.farRegion (C : Set Plane) (y : Plane) : Set Plane

The region of ℝ² ∖ C that does not contain y: everything off C except the component of y. For a separating curve this really is the other region (IsSeparating.isRegionPair_farRegion); no hypothesis is needed to define it.

Equations

• Schoenflies.farRegion C y = Cᶜ \ connectedComponentIn Cᶜ y

theorem Schoenflies.mem_farRegion_iff {C : Set Plane} {x y : Plane} : x ∈ farRegion C y ↔ x ∉ C ∧ x ∉ connectedComponentIn Cᶜ y

theorem Schoenflies.farRegion_subset_compl {C : Set Plane} {y : Plane} : farRegion C y ⊆ Cᶜ

theorem Schoenflies.notMem_farRegion_self {C : Set Plane} {y : Plane} (hy : y ∉ C) : y ∉ farRegion C y

theorem Schoenflies.mem_farRegion_iff_connectedComponentIn_ne {C : Set Plane} {x y : Plane} (hx : x ∉ C) : x ∈ farRegion C y ↔ connectedComponentIn Cᶜ x ≠ connectedComponentIn Cᶜ y

Off the curve, being in the far region is exactly being in another component.

theorem Schoenflies.diff_subset_farRegion {C P : Set Plane} {y : Plane} (hdis : Disjoint P (connectedComponentIn Cᶜ y)) : P \ C ⊆ farRegion C y

The crosscut misses the region of y, so all of it off the curve is in the far region.

theorem Schoenflies.compl_diff_inside (C : Set Plane) : Cᶜ \ inside C = outside C

theorem Schoenflies.compl_diff_outside (C : Set Plane) : Cᶜ \ outside C = inside C

theorem Schoenflies.IsSeparating.isRegionPair_farRegion {C : Set Plane} {y : Plane} (hC : IsSeparating C) (hy : y ∉ C) : IsRegionPair C (connectedComponentIn Cᶜ y) (farRegion C y)

The component of y and the far region are the two regions of ℝ² ∖ C.

theorem Schoenflies.IsSeparating.isRegionOf_farRegion {C : Set Plane} {y : Plane} (hC : IsSeparating C) (hy : y ∉ C) : IsRegionOf C (farRegion C y)

theorem Schoenflies.IsSeparating.farRegion_eq_inside {C : Set Plane} {y : Plane} (hC : IsSeparating C) (hy : y ∈ outside C) : farRegion C y = inside C

Seen from the unbounded region, the far region is the bounded one — the blueprint's case (a), where Vᵢ = Int(Jᵢ).

theorem Schoenflies.IsSeparating.farRegion_eq_outside {C : Set Plane} {y : Plane} (hC : IsSeparating C) (hy : y ∈ inside C) : farRegion C y = outside C

Seen from the bounded region, the far region is the unbounded one.

The three regions of ℝ² ∖ (C ∪ P), abstractly

Lemma 2.6 places the two cells inside Ω ∖ P; the last paragraph of the proof of Theorem 2.8 places all three regions inside ℝ² ∖ (C ∪ P), and the argument is the same each time: an open connected set whose frontier misses the ambient open set is a component of it (Lemma 1.7).

theorem Schoenflies.compl_union_eq_of_isRegionPair {C P Ω Ω' : Set Plane} (hΩ : IsRegionPair C Ω Ω') (hdis : Disjoint P Ω') : (C ∪ P)ᶜ = Ω \ P ∪ Ω'

ℝ² ∖ (C ∪ P) is Ω ∖ P together with the untouched region Ω'.

theorem Schoenflies.far_isComponent {C P Ω Ω' : Set Plane} {z : Plane} (hC : IsSeparating C) (hΩ : IsRegionPair C Ω Ω') (hdis : Disjoint P Ω') (hz : z ∈ Ω') : connectedComponentIn (C ∪ P)ᶜ z = Ω'

The untouched region is a component of ℝ² ∖ (C ∪ P): its frontier is C.

theorem Schoenflies.cell_isComponent_compl {C J P W V : Set Plane} {z : Plane} (hJ : IsSeparating J) (hWV : IsRegionPair J W V) (hJCP : J ⊆ C ∪ P) (hV : V ⊆ (C ∪ P)ᶜ) (hz : z ∈ V) : connectedComponentIn (C ∪ P)ᶜ z = V

A cell is a component of ℝ² ∖ (C ∪ P): its frontier is J ⊆ C ∪ P.

The arcs of a polygon, and parity as a separation criterion

theorem Schoenflies.zmod_add_sub_cancel {m k : ℕ} (hk : k ≤ m + 3) (a : ZMod (m + 3)) : a + ↑k + ↑(m + 3 - k) = a

Going k steps forward and then the remaining m + 3 - k returns to where one started: the second arc of a split ends at the first arc's starting vertex.

def Schoenflies.ClosedPolygon.arc {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) : Set Plane

The arc of C that leaves vertex a and runs forward through k edges, as a set: the blueprint's A₁ for k edges and A₂ for the remaining m + 3 - k.

Equations

• C.arc a k = Schoenflies.cover (C.arcPieces a k)

theorem Schoenflies.ClosedPolygon.arc_subset_carrier {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) : C.arc a k ⊆ C.carrier

theorem Schoenflies.ClosedPolygon.arc_union {m k : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (hk : k ≤ m + 3) : C.arc a k ∪ C.arc (a + ↑k) (m + 3 - k) = C.carrier

The two arcs cover the polygon.

theorem Schoenflies.ClosedPolygon.carrier_eq_arc_union {m : ℕ} {C : ClosedPolygon m} {a : ZMod (m + 3)} {k m' : ℕ} {J : ClosedPolygon m'} {K : List Piece} (h : SameEdges J.pieces (C.arcPieces a k ++ K)) : J.carrier = C.arc a k ∪ cover K

A curve of the split occupies its arc together with the crosscut.

theorem Schoenflies.ClosedPolygon.parity_ne_iff_mem_farRegion {m : ℕ} (C : ClosedPolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ C.pieces, hgt u Q.1 ≠ hgt u Q.2) {x y : Plane} (hx : x ∉ C.carrier) (hy : y ∉ C.carrier) : parity u C.pieces x ≠ parity u C.pieces y ↔ x ∈ farRegion C.carrier y

The crossing count separates points exactly as the polygon does (Theorem 2.3, read as a criterion). Two points off the polygon lie in different regions precisely when their crossing counts differ: equal components force equal counts by Lemma 2.2, and different components are the bounded and the unbounded one, whose counts are 1 and 0.

theorem Schoenflies.ClosedPolygon.vertex_mem_arc {m k : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (hk : 1 ≤ k) : C.vertex a ∈ C.arc a k

The first vertex of a nonempty arc lies on it.

theorem Schoenflies.ClosedPolygon.vertex_add_mem_arc {m k : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (hk : 1 ≤ k) : C.vertex (a + ↑k) ∈ C.arc a k

The last vertex of a nonempty arc lies on it.

theorem Schoenflies.ClosedPolygon.endpoints_subset_arc {m k : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (hk : 1 ≤ k) : {C.vertex a, C.vertex (a + ↑k)} ⊆ C.arc a k

The two cut vertices lie on both arcs. This is what turns the blueprint's "the crosscut meets C only in its two endpoints" into the hypotheses meets₁ and meets₂.

theorem Schoenflies.ClosedPolygon.endpoints_subset_arc' {m k : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (hk2 : k ≤ m + 2) : {C.vertex a, C.vertex (a + ↑k)} ⊆ C.arc (a + ↑k) (m + 3 - k)

The same for the complementary arc, whose two ends are the same two vertices in the other order.

The hypotheses of Theorem 2.8

structure Schoenflies.IsPolygonalCrosscut {m m₁ m₂ : ℕ} (C : ClosedPolygon m) (J₁ : ClosedPolygon m₁) (J₂ : ClosedPolygon m₂) (K : List Piece) (a : ZMod (m + 3)) (k : ℕ) (y : Plane) : Prop

The setting of Theorem 2.8. K is the edge list of a polygonal crosscut of the polygon C, cutting it at the vertices a and a + k; J₁ and J₂ are the two closed curves formed by the crosscut with each of the two arcs; and y is a point of the region of ℝ² ∖ C that the crosscut does not enter, which is what fixes which side of C the crosscut is on.

The blueprint's "P is a simple arc meeting C exactly in its two endpoints" appears here in two pieces: meets₁ and meets₂ say that whatever the crosscut has in common with C lies on both arcs, which for a genuine crosscut is the two cut vertices (ClosedPolygon.vertex_mem_arc, ClosedPolygon.vertex_add_mem_arc); and simplicity is carried by the assumption that J₁ and J₂ really are ClosedPolygons. Nothing else about K is assumed — not even that its pieces are nondegenerate, which follows from edges₁.

• le : k ≤ m + 3

  The first arc runs forward through at most a full turn.

• edges₁ : SameEdges J₁.pieces (C.arcPieces a k ++ K)

  J₁ carries the edges of the first arc together with those of the crosscut.

• edges₂ : SameEdges J₂.pieces (C.arcPieces (a + ↑k) (m + 3 - k) ++ K)

  J₂ carries the edges of the second arc together with those of the crosscut.

• meets₁ : cover K ∩ C.carrier ⊆ C.arc a k

  The crosscut meets the polygon only in points of the first arc …

• meets₂ : cover K ∩ C.carrier ⊆ C.arc (a + ↑k) (m + 3 - k)

  … and only in points of the second arc.

• notMem : y ∉ C.carrier

  The reference point lies off the polygon …

• avoids : Disjoint (cover K) (connectedComponentIn C.carrierᶜ y)

  … and the crosscut does not enter its region.

theorem Schoenflies.IsPolygonalCrosscut.of_endpoints {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (hk1 : 1 ≤ k) (hk2 : k ≤ m + 2) (edges₁ : SameEdges J₁.pieces (C.arcPieces a k ++ K)) (edges₂ : SameEdges J₂.pieces (C.arcPieces (a + ↑k) (m + 3 - k) ++ K)) (meets : cover K ∩ C.carrier ⊆ {C.vertex a, C.vertex (a + ↑k)}) (notMem : y ∉ C.carrier) (avoids : Disjoint (cover K) (connectedComponentIn C.carrierᶜ y)) : IsPolygonalCrosscut C J₁ J₂ K a k y

The front door. A crosscut is normally presented by saying that it meets C exactly in its two endpoints, and that those endpoints are the two cut vertices; meets₁ and meets₂ follow, because both cut vertices lie on both arcs. The bound k ≤ m + 2 says the second arc is nonempty, as 1 ≤ k says the first one is.

theorem Schoenflies.IsPolygonalCrosscut.symm {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : IsPolygonalCrosscut C J₂ J₁ K (a + ↑k) (m + 3 - k) y

The two arcs may be swapped. Every statement below is therefore proved for J₁ only.

The elementary consequences

theorem Schoenflies.IsPolygonalCrosscut.notMem_cover {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : y ∉ cover K

theorem Schoenflies.IsPolygonalCrosscut.carrier₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : J₁.carrier = C.arc a k ∪ cover K

theorem Schoenflies.IsPolygonalCrosscut.notMem_carrier₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : y ∉ J₁.carrier

theorem Schoenflies.IsPolygonalCrosscut.cover_subset_carrier₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : cover K ⊆ J₁.carrier

theorem Schoenflies.IsPolygonalCrosscut.carrier₁_subset {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : J₁.carrier ⊆ C.carrier ∪ cover K

theorem Schoenflies.IsPolygonalCrosscut.nondeg {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) (Q : Piece) : Q ∈ K → Q.Nondeg

The edges of the crosscut are nondegenerate, because they are edges of J₁.

theorem Schoenflies.IsPolygonalCrosscut.exists_direction {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : ∃ (u : Plane), u.IsDirection ∧ (∀ Q ∈ C.pieces, hgt u Q.1 ≠ hgt u Q.2) ∧ ∀ Q ∈ K, hgt u Q.1 ≠ hgt u Q.2

A ray direction transverse to every edge of C and of the crosscut at once.

The two cells

Lemma 2.6 applies with Ω = farRegion C.carrier y, Ω' = connectedComponentIn C.carrierᶜ y, Wᵢ = connectedComponentIn Jᵢ.carrierᶜ y and Vᵢ = farRegion Jᵢ.carrier y. The inclusion Ω' ⊆ Wᵢ — the blueprint's "being connected it lies in one region of ℝ² ∖ Jᵢ" — is near_subset₁, and needs no separation hypothesis at all.

theorem Schoenflies.IsPolygonalCrosscut.regionPairC {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : IsRegionPair C.carrier (farRegion C.carrier y) (connectedComponentIn C.carrierᶜ y)

theorem Schoenflies.IsPolygonalCrosscut.regionPair₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : IsRegionPair J₁.carrier (connectedComponentIn J₁.carrierᶜ y) (farRegion J₁.carrier y)

theorem Schoenflies.IsPolygonalCrosscut.near_subset₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : connectedComponentIn C.carrierᶜ y ⊆ connectedComponentIn J₁.carrierᶜ y

The untouched region of ℝ² ∖ C lies in one region of ℝ² ∖ J₁, namely the one of y.

theorem Schoenflies.IsPolygonalCrosscut.cell_subset₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : farRegion J₁.carrier y ⊆ farRegion C.carrier y \ cover K

Lemma 2.6(a), first half: the cell lies in Ω ∖ P.

theorem Schoenflies.IsPolygonalCrosscut.cell_subset₂ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : farRegion J₂.carrier y ⊆ farRegion C.carrier y \ cover K

theorem Schoenflies.IsPolygonalCrosscut.cell_isComponent₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) (z : Plane) : z ∈ farRegion J₁.carrier y → connectedComponentIn (farRegion C.carrier y \ cover K) z = farRegion J₁.carrier y

Lemma 2.6(a): the cell is a connected component of Ω ∖ P.

theorem Schoenflies.IsPolygonalCrosscut.cell_isComponent₂ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) (z : Plane) : z ∈ farRegion J₂.carrier y → connectedComponentIn (farRegion C.carrier y \ cover K) z = farRegion J₂.carrier y

theorem Schoenflies.IsPolygonalCrosscut.closure_cell_inter₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : closure (farRegion J₁.carrier y) ∩ C.carrier = C.arc a k

Lemma 2.6(c): the closure of the cell meets the polygon exactly in its arc.

theorem Schoenflies.IsPolygonalCrosscut.closure_cell_inter₂ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : closure (farRegion J₂.carrier y) ∩ C.carrier = C.arc (a + ↑k) (m + 3 - k)

theorem Schoenflies.IsPolygonalCrosscut.frontier_cell₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : frontier (farRegion J₁.carrier y) = J₁.carrier

The cell has J₁ as its frontier.

theorem Schoenflies.IsPolygonalCrosscut.frontier_cell₂ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : frontier (farRegion J₂.carrier y) = J₂.carrier

theorem Schoenflies.IsPolygonalCrosscut.cell_nonempty₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : (farRegion J₁.carrier y).Nonempty

Exhaustion: the crossing counts add up

This is the whole of Theorem 2.8 beyond Lemma 2.6, and it is one ZMod 2 computation.

theorem Schoenflies.IsPolygonalCrosscut.separates_xor {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) {x : Plane} (hxC : x ∉ C.carrier) (hxK : x ∉ cover K) : x ∈ farRegion C.carrier y ↔ (x ∈ farRegion J₁.carrier y ↔ x ∉ farRegion J₂.carrier y)

A point off C ∪ P is separated from y by C exactly when it is separated from y by exactly one of J₁, J₂. Lemma 2.7 gives πJ₁ + πJ₂ = πC at every point; evaluating it at x and at y and subtracting turns the three "different region" statements — which Theorem 2.3 reads off the three crossing counts — into the exclusive disjunction.

theorem Schoenflies.IsPolygonalCrosscut.region_eq {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : farRegion C.carrier y \ cover K = farRegion J₁.carrier y ∪ farRegion J₂.carrier y

Theorem 2.8, the two cells. The region the crosscut enters, with the crosscut removed, is the disjoint union of the two cells.

theorem Schoenflies.IsPolygonalCrosscut.cells_disjoint {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : Disjoint (farRegion J₁.carrier y) (farRegion J₂.carrier y)

theorem Schoenflies.IsPolygonalCrosscut.cells_ne {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : farRegion J₁.carrier y ≠ farRegion J₂.carrier y

theorem Schoenflies.IsPolygonalCrosscut.cell_ne_near₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : farRegion J₁.carrier y ≠ connectedComponentIn C.carrierᶜ y

A cell is not the untouched region: it lies on the other side of C.

theorem Schoenflies.IsPolygonalCrosscut.cell_ne_near₂ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : farRegion J₂.carrier y ≠ connectedComponentIn C.carrierᶜ y

The three regions of ℝ² ∖ (C ∪ P)

theorem Schoenflies.IsPolygonalCrosscut.cell_subset_compl₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : farRegion J₁.carrier y ⊆ (C.carrier ∪ cover K)ᶜ

theorem Schoenflies.IsPolygonalCrosscut.compl_eq {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : (C.carrier ∪ cover K)ᶜ = farRegion J₁.carrier y ∪ farRegion J₂.carrier y ∪ connectedComponentIn C.carrierᶜ y

The three regions together are the whole of ℝ² ∖ (C ∪ P).

theorem Schoenflies.IsPolygonalCrosscut.near_isComponent {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) {z : Plane} (hz : z ∈ connectedComponentIn C.carrierᶜ y) : connectedComponentIn (C.carrier ∪ cover K)ᶜ z = connectedComponentIn C.carrierᶜ y

The untouched region is a component of ℝ² ∖ (C ∪ P), with frontier C.

theorem Schoenflies.IsPolygonalCrosscut.frontier_near {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : frontier (connectedComponentIn C.carrierᶜ y) = C.carrier

theorem Schoenflies.IsPolygonalCrosscut.cell_isComponent_compl₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) {z : Plane} (hz : z ∈ farRegion J₁.carrier y) : connectedComponentIn (C.carrier ∪ cover K)ᶜ z = farRegion J₁.carrier y

The first cell is a component of ℝ² ∖ (C ∪ P), with frontier J₁.

theorem Schoenflies.IsPolygonalCrosscut.cell_isComponent_compl₂ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) {z : Plane} (hz : z ∈ farRegion J₂.carrier y) : connectedComponentIn (C.carrier ∪ cover K)ᶜ z = farRegion J₂.carrier y

theorem Schoenflies.IsPolygonalCrosscut.isComponent {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) {z : Plane} (hz : z ∉ C.carrier ∪ cover K) : connectedComponentIn (C.carrier ∪ cover K)ᶜ z = farRegion J₁.carrier y ∨ connectedComponentIn (C.carrier ∪ cover K)ᶜ z = farRegion J₂.carrier y ∨ connectedComponentIn (C.carrier ∪ cover K)ᶜ z = connectedComponentIn C.carrierᶜ y

"ℝ² ∖ (C ∪ P) has exactly three regions." Every component is one of the three named sets, and each of the three is a component (cell_isComponent_compl₁, …₂, near_isComponent). Their frontiers are J₁, J₂ and C.

The blueprint's two cases

theorem Schoenflies.IsPolygonalCrosscut.mem_outside₁ {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) (hy : y ∈ outside C.carrier) : y ∈ outside J₁.carrier

Seen from the unbounded region of C, J₁ too has y outside it: otherwise the unbounded Ext(C) would sit inside the bounded Int(J₁).

theorem Schoenflies.IsPolygonalCrosscut.cell₁_eq_inside {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) (hy : y ∈ outside C.carrier) : farRegion J₁.carrier y = inside J₁.carrier

theorem Schoenflies.IsPolygonalCrosscut.cell₂_eq_inside {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) (hy : y ∈ outside C.carrier) : farRegion J₂.carrier y = inside J₂.carrier

theorem Schoenflies.IsPolygonalCrosscut.inside_diff_eq {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) (hy : y ∈ outside C.carrier) : inside C.carrier \ cover K = inside J₁.carrier ∪ inside J₂.carrier

Theorem 2.8(a). If the crosscut runs inside C — that is, if the reference point y lies in Ext(C) — then Int(C) ∖ P is exactly the union of the two bounded regions of J₁ and J₂, and those two are disjoint.

theorem Schoenflies.IsPolygonalCrosscut.outside_diff_eq {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) (hy : y ∈ inside C.carrier) : outside C.carrier \ cover K = farRegion J₁.carrier y ∪ farRegion J₂.carrier y

Theorem 2.8(b). If the crosscut runs outside C — that is, if y ∈ Int(C) — then Ext(C) ∖ P has exactly the two regions farRegion Jᵢ.carrier y, whose frontiers are J₁ and J₂ (frontier_cell₁, frontier_cell₂) and which are components of it (cell_isComponent₁, …₂). Which of the two is Int(Jᵢ) and which Ext(Jᵢ) is settled by inside_exactly_one.

theorem Schoenflies.IsPolygonalCrosscut.inside_exactly_one {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) (hy : y ∈ inside C.carrier) : y ∈ inside J₁.carrier ↔ y ∉ inside J₂.carrier

In case (b), Int(C) lies inside exactly one of J₁, J₂ — the blueprint's "relabel so that it lies inside J₁".

theorem Schoenflies.polygonal_crosscut {m m₁ m₂ : ℕ} {C : ClosedPolygon m} {J₁ : ClosedPolygon m₁} {J₂ : ClosedPolygon m₂} {K : List Piece} {a : ZMod (m + 3)} {k : ℕ} {y : Plane} (h : IsPolygonalCrosscut C J₁ J₂ K a k y) : farRegion C.carrier y \ cover K = farRegion J₁.carrier y ∪ farRegion J₂.carrier y ∧ Disjoint (farRegion J₁.carrier y) (farRegion J₂.carrier y) ∧ (∀ z ∈ farRegion J₁.carrier y, connectedComponentIn (farRegion C.carrier y \ cover K) z = farRegion J₁.carrier y) ∧ (∀ z ∈ farRegion J₂.carrier y, connectedComponentIn (farRegion C.carrier y \ cover K) z = farRegion J₂.carrier y) ∧ frontier (farRegion J₁.carrier y) = J₁.carrier ∧ frontier (farRegion J₂.carrier y) = J₂.carrier ∧ closure (farRegion J₁.carrier y) ∩ C.carrier = C.arc a k ∧ closure (farRegion J₂.carrier y) ∩ C.carrier = C.arc (a + ↑k) (m + 3 - k) ∧ ∀ z ∉ C.carrier ∪ cover K, connectedComponentIn (C.carrier ∪ cover K)ᶜ z = farRegion J₁.carrier y ∨ connectedComponentIn (C.carrier ∪ cover K)ᶜ z = farRegion J₂.carrier y ∨ connectedComponentIn (C.carrier ∪ cover K)ᶜ z = connectedComponentIn C.carrierᶜ y

Theorem 2.8 (two-sided polygonal crosscuts). Let C be a simple closed polygon, K the edge list of a polygonal crosscut cutting it at the vertices a and a + k, and J₁, J₂ the two closed polygons formed by the crosscut with the two arcs. Let y be a point of the region of ℝ² ∖ C that the crosscut does not enter, and write Ω = farRegion C.carrier y for the other region and Vᵢ = farRegion Jᵢ.carrier y for the region of ℝ² ∖ Jᵢ on the far side from y. Then

• Ω ∖ P is the disjoint union of V₁ and V₂, which are its two connected components;
• their frontiers are J₁ and J₂, and the closure of Vᵢ meets C exactly in the arc Aᵢ;
• ℝ² ∖ (C ∪ P) has exactly three regions, V₁, V₂ and the region of y.

Case (a) of the blueprint is IsPolygonalCrosscut.inside_diff_eq, which rewrites Ω as Int(C) and Vᵢ as Int(Jᵢ); case (b) is IsPolygonalCrosscut.outside_diff_eq.