A crosscut cuts a region into at most two pieces

Lemma "At most two sides": if D is a region and P is a simple polygonal arc whose endpoints lie outside D and whose remaining points lie in D, then D ∖ P has at most two components. This is the missing half of the crosscut theorem — the crosscut-cells lemma (Schoenflies.crosscut_cells) already exhibits two components, and this says there are no others.

"At most two" as a covering statement

Nothing here talks about the set of components. What is proved, and what the crosscut theorem consumes, is the constructive form: two points z_L, z_R of D ∖ P such that every point of D ∖ P lies in the component of one of them (crosscut_at_most_two). Handed two components that are known to be distinct — which is exactly what the crosscut-cells lemma supplies — that turns into "every point lies in one of those two" (crosscut_components_exhaust), which is the sentence the crosscut theorem actually needs.

The proof is a clopen argument, not the blueprint's path argument

The blueprint traces a polygonal arc γ from an arbitrary x ∈ D ∖ P to a reference point z₀ ∈ P, takes the first point z of γ on P, and pushes x into a track of a strip around the subarc of P from z to z₀. The first-hitting-point step is only there to find a point of D ∖ P next to P; once one knows that a whole neighbourhood of every point of P ∩ D is covered by the two components, the statement is a connectedness argument and no path is needed:

• T, the set of points of D ∖ P in neither of the two components, is open, because a component of an open subset of the plane is open and two components are equal or disjoint (isOpen_notMem_two_components);
• U, the union of the two components with every open piece of D whose complement of P is covered, is open and contains all of P ∩ D;
• U and T are disjoint, cover D, and U meets D; so T = ∅ because D is connected.

That is covered_by_two_of_local, and it is where "at most two" really comes from. The arc, the polygonality and the endpoint hypotheses enter only through the collar.

The collar is a hypothesis: Schoenflies/Strip.lean is stated for a closed curve

The local input the argument needs is blueprint Lemma 1.8 (b) — a two-sided collar of a compact subarc of P ∖ ∂P. Schoenflies/Strip.lean, Schoenflies/StripLocal.lean and Schoenflies/Compose.lean build the collar of a ClosedPolygon, a closed curve, and the note at the end of StripLocal.lean says in as many words that the arc case "is not formalised". There is no way to get it from the closed case: the two tracks of a closed collar are connected because they run all the way round the curve, and intersecting them with D destroys exactly that.

So HasArcCollars D P is an explicit hypothesis of every theorem below. It is blueprint Lemma 1.8 (b) with the prescribed open set taken to be D, together with the "local sides" clause of that lemma in the form StripLocal.lean already proves in the closed case (StripData.carrier_subset_closure_sideL): every point of the subarc is in the closure of both tracks. ArcCollar is the bundled datum, so a discharger returns a construction rather than an existential.

Blueprint

• Schoenflies.ArcCollar, Schoenflies.HasArcCollars — Lemma 1.8 (b) (two-sided polygonal strips, the arc case) as an interface: the collar of one compact subarc as data, and the hypothesis that every compact subarc has one.
• Schoenflies.isOpen_notMem_two_components, Schoenflies.covered_by_two_of_local — the clopen step, which is the whole of the lemma once the collar is available.
• Schoenflies.crosscut_at_most_two — Lemma "At most two sides".
• Schoenflies.crosscut_components_exhaust — the same, applied to two components already known to be distinct; this is the form Theorem "Crosscut theorem" cites.
• Schoenflies.Plane.mem_segment_iff_coord, Schoenflies.hasArcCollars_segment — Lemma 1.8 (b) for a straight crosscut, which is the blueprint's edge block and nothing else. With it, Schoenflies.segment_crosscut_at_most_two is Lemma "At most two sides" for a straight crosscut with no hypothesis left standing, and certifies that HasArcCollars is satisfiable.

The collar of a compact subarc, as data

Blueprint Lemma 1.8 (b). nbhd is the neighbourhood N, left and right are the two tracks N_L, N_R. The prescribed open set of the blueprint is D, which is all this development ever prescribes.

Two clauses of the blueprint are dropped because nothing here uses them: that the tracks are open and that they are disjoint. Two are kept and are essential: that each track is connected — that is the whole point of a collar, and it is what ties the local picture at one point of the arc to the local picture at another — and that every point of the subarc is in the closure of both tracks, which is the blueprint's "the two sets N_L, N_R are the two local sides of the curve" in the form StripLocal.lean proves it for a closed polygon.

structure Schoenflies.ArcCollar (D P K : Set Plane) : Type

A two-sided collar of the compact subarc K of P, inside the region D: an open neighbourhood nbhd of K contained in D, whose complement of P splits into two connected tracks, each of which approaches every point of K.

Note that the splitting clause is stated for nbhd ∖ P and not for nbhd ∖ K: an open neighbourhood of K necessarily contains points of P beyond the ends of K, and it is the whole of P that has to be removed for the tracks to lie in D ∖ P. That is how the blueprint states it too.

• nbhd : Set Plane

  the neighbourhood N of the subarc

• left : Set Plane

  the left track N_L

• right : Set Plane

  the right track N_R

• isOpen_nbhd : IsOpen self.nbhd
• subset_nbhd : K ⊆ self.nbhd
• nbhd_subset : self.nbhd ⊆ D
• nbhd_diff : self.nbhd \ P = self.left ∪ self.right
• isConnected_left : IsConnected self.left
• isConnected_right : IsConnected self.right
• subset_closure_left : K ⊆ closure self.left
• subset_closure_right : K ⊆ closure self.right

def Schoenflies.HasArcCollars (D P : Set Plane) : Prop

Blueprint Lemma 1.8 (b) as a hypothesis. Every nondegenerate compact connected piece of P lying inside D has a two-sided collar inside D.

A compact connected subset of an arc is a compact subarc, so this is the blueprint's "if P is an arc and K is a compact subarc of P ∖ ∂P" — the condition K ⊆ D ∩ P is what "K avoids the endpoints" amounts to here, since the endpoints of a crosscut are outside D.

Nondegeneracy is asked for because the blueprint's proof builds the collar out of edge blocks and vertex disks along K, which needs K to contain an edge; a consumer that has a genuine subarc always has it.

Equations

• Schoenflies.HasArcCollars D P = ∀ K ⊆ D ∩ P, IsCompact K → IsPreconnected K → K.Nontrivial → Nonempty (Schoenflies.ArcCollar D P K)

theorem Schoenflies.ArcCollar.left_subset_nbhd_diff {D P K : Set Plane} (C : ArcCollar D P K) : C.left ⊆ C.nbhd \ P

theorem Schoenflies.ArcCollar.right_subset_nbhd_diff {D P K : Set Plane} (C : ArcCollar D P K) : C.right ⊆ C.nbhd \ P

theorem Schoenflies.ArcCollar.nbhd_diff_subset_diff {D P K : Set Plane} (C : ArcCollar D P K) : C.nbhd \ P ⊆ D \ P

theorem Schoenflies.ArcCollar.left_subset_diff {D P K : Set Plane} (C : ArcCollar D P K) : C.left ⊆ D \ P

theorem Schoenflies.ArcCollar.right_subset_diff {D P K : Set Plane} (C : ArcCollar D P K) : C.right ⊆ D \ P

noncomputable def Schoenflies.ArcCollar.ptL {D P K : Set Plane} (C : ArcCollar D P K) : Plane

The reference point on the left of the arc. Exported as a function of the collar rather than produced by an existential, so that a consumer holding a collar holds the point.

Equations

• C.ptL = ⋯.some

noncomputable def Schoenflies.ArcCollar.ptR {D P K : Set Plane} (C : ArcCollar D P K) : Plane

The reference point on the right of the arc.

Equations

• C.ptR = ⋯.some

theorem Schoenflies.ArcCollar.ptL_mem {D P K : Set Plane} (C : ArcCollar D P K) : C.ptL ∈ C.left

theorem Schoenflies.ArcCollar.ptR_mem {D P K : Set Plane} (C : ArcCollar D P K) : C.ptR ∈ C.right

theorem Schoenflies.ArcCollar.ptL_mem_diff {D P K : Set Plane} (C : ArcCollar D P K) : C.ptL ∈ D \ P

theorem Schoenflies.ArcCollar.ptR_mem_diff {D P K : Set Plane} (C : ArcCollar D P K) : C.ptR ∈ D \ P

theorem Schoenflies.ArcCollar.meeting_subset_components {D P K' : Set Plane} (C₀ : ArcCollar D P K') {S : Set Plane} (hS : IsPreconnected S) (hSsub : S ⊆ D \ P) (hmeet : (C₀.nbhd ∩ S).Nonempty) : S ⊆ connectedComponentIn (D \ P) C₀.ptL ∪ connectedComponentIn (D \ P) C₀.ptR

A connected piece of D ∖ P that meets the neighbourhood of a collar lies in one of the two components that collar's reference points name.

The piece meets nbhd in a point off P, which is therefore in one of the two tracks; the piece and that track together are connected inside D ∖ P and contain the corresponding reference point.

theorem Schoenflies.ArcCollar.nbhd_diff_subset_components {D P K K' : Set Plane} (C₀ : ArcCollar D P K') (C : ArcCollar D P K) {z : Plane} (hz' : z ∈ K') (hz : z ∈ K) : C.nbhd \ P ⊆ connectedComponentIn (D \ P) C₀.ptL ∪ connectedComponentIn (D \ P) C₀.ptR

The whole of a second collar is covered by the two components named by the first, as soon as the two subarcs share a point.

Both tracks of C approach the shared point z, and C₀.nbhd is an open neighbourhood of it, so each track of C meets C₀.nbhd; meeting_subset_components then places each of them in one of the two components. This is the blueprint's "one track meets B_L and the other meets B_R", with the two half-disks replaced by the fixed collar.

The clopen step

theorem Schoenflies.isOpen_notMem_two_components {S : Set Plane} (hS : IsOpen S) (zL zR : Plane) : IsOpen {y : Plane | y ∈ S ∧ y ∉ connectedComponentIn S zL ∧ y ∉ connectedComponentIn S zR}

The points of an open set that are in neither of two prescribed components form an open set: each such point drags its whole component with it, and a component of an open subset of the plane is open.

theorem Schoenflies.covered_by_two_of_local {D P : Set Plane} (hDopen : IsOpen D) (hDconn : IsPreconnected D) (hPclosed : IsClosed P) {zL zR : Plane} (hzL : zL ∈ D \ P) (hloc : ∀ w ∈ D ∩ P, ∃ (V : Set Plane), IsOpen V ∧ w ∈ V ∧ V ⊆ D ∧ V \ P ⊆ connectedComponentIn (D \ P) zL ∪ connectedComponentIn (D \ P) zR) {x : Plane} (hx : x ∈ D \ P) : x ∈ connectedComponentIn (D \ P) zL ∨ x ∈ connectedComponentIn (D \ P) zR

The clopen step, and the whole of "at most two sides" once a collar is available. If every point of P inside the region D has a neighbourhood inside D whose complement of P is covered by the components of two fixed points z_L, z_R, then all of D ∖ P is covered by those two components.

The set T of points of D ∖ P in neither component is open; the union U of the two components with all the good neighbourhoods is open, contains P ∩ D and meets D; the two are disjoint and cover D. Connectedness of D kills T.

Lemma "At most two sides"

theorem Schoenflies.crosscut_at_most_two {D P : Set Plane} {a b : Plane} (hDopen : IsOpen D) (hDconn : IsPreconnected D) (hP : IsArcBetween P a b) (_hPpoly : IsPolygonal P) (ha : a ∉ D) (hb : b ∉ D) (hPD : P \ {a, b} ⊆ D) (hcollars : HasArcCollars D P) : ∃ zL ∈ D \ P, ∃ zR ∈ D \ P, ∀ x ∈ D \ P, x ∈ connectedComponentIn (D \ P) zL ∨ x ∈ connectedComponentIn (D \ P) zR

Lemma "At most two sides". Let D be a region and P a simple polygonal arc whose endpoints a, b lie outside D and whose remaining points lie in D. Then there are two points z_L, z_R of D ∖ P such that every point of D ∖ P lies in the component of one of them — that is, D ∖ P has at most two components.

IsPolygonal P is carried because the blueprint statement carries it, and because it is what makes HasArcCollars dischargeable; this proof does not use it, since all the geometry is inside the collar.

The reference points are the two reference points of the collar of the middle third of the arc: K₀ = f '' [1/4, 3/4] for a parametrisation f of P. Any other nondegenerate compact subarc would do, and ArcCollar.nbhd_diff_subset_components is stated so that a consumer that has a collar of its own can use its reference points instead.

theorem Schoenflies.covered_by_two_components_of_ne {S : Set Plane} {zL zR v₁ v₂ : Plane} (h : ∀ x ∈ S, x ∈ connectedComponentIn S zL ∨ x ∈ connectedComponentIn S zR) (h₁ : v₁ ∈ S) (h₂ : v₂ ∈ S) (hne : connectedComponentIn S v₁ ≠ connectedComponentIn S v₂) (x : Plane) : x ∈ S → x ∈ connectedComponentIn S v₁ ∨ x ∈ connectedComponentIn S v₂

"At most two", read off two components already known to be distinct. This is the form Theorem "Crosscut theorem" cites: the crosscut-cells lemma hands it two distinct components of D ∖ P, and this says there is nothing else.

Stated for an arbitrary set S, since it is pure component bookkeeping: if everything is covered by the components of z_L, z_R and v₁, v₂ have different components, then those two components are the two, in one order or the other.

The collar hypothesis is not vacuous: a straight crosscut

The collar of a straight crosscut is a rectangle, and the free-standing frame toolkit of Schoenflies/Strip.lean — coordAlong, coordAcross, strip, isOpen_strip, convex_strip, dist_foot, frame_decomp — builds it directly, with no cyclic vertex family in sight. So HasArcCollars is discharged outright in the simplest crosscut configuration, and segment_crosscut_at_most_two below is a hypothesis-free instance of the lemma.

This is the shape a general discharger has to reproduce along a chain of edges: it is exactly the blueprint's edge block, and what is missing is the vertex disks between consecutive blocks and the end cross-sections.

theorem Schoenflies.Plane.exists_direction_length {a b : Plane} (hab : a ≠ b) : ∃ (u : Plane) (L : ℝ), 0 < L ∧ u.IsDirection ∧ L • u = b - a

A nondegenerate segment has a unit direction and a length: L • u = b - a with ‖u‖ = 1.

Stated as an existential so that the direction and the length are opaque to the consumer. Writing them as dir (b - a) and ‖b - a‖ makes every subsequent rewrite of b reach inside them, which is exactly the friction the strip apparatus avoids by carrying tang and len as fields.

theorem Schoenflies.Plane.mem_segment_iff_coord {a b u x : Plane} {L : ℝ} (hL : 0 < L) (hu : u.IsDirection) (hLu : L • u = b - a) : x ∈ segment ℝ a b ↔ a.coordAcross u x = 0 ∧ a.coordAlong u x ∈ Set.Icc 0 L

A nondegenerate segment, read in the frame of its own direction. Its points are the ones at signed distance zero whose progress along the direction lies between 0 and the length.

This is the segment analogue of ClosedPolygon.mem_edge_iff, which is stated for an edge of a closed polygon and so is unavailable for a lone segment.

theorem Schoenflies.Plane.eq_foot_of_coordAcross_eq_zero {a u x : Plane} (hu : u.IsDirection) (h0 : a.coordAcross u x = 0) : x = a + a.coordAlong u x • u

A point at signed distance zero is the point of the line with its own progress.

theorem Schoenflies.hasArcCollars_segment {D : Set Plane} {a b : Plane} (hab : a ≠ b) (hDopen : IsOpen D) (ha : a ∉ D) (hb : b ∉ D) (hPD : segment ℝ a b \ {a, b} ⊆ D) : HasArcCollars D (segment ℝ a b)

A straight crosscut has two-sided collars. For a nondegenerate segment whose endpoints lie outside the region and whose remaining points lie inside, blueprint Lemma 1.8 (b) is a rectangle: an open block around the subarc, of half-width small enough to stay inside the region, split by the line of the segment into two convex halves.

This discharges HasArcCollars in the one case the existing strip apparatus reaches without an arc collar being built, and so certifies that the hypothesis of crosscut_at_most_two is satisfiable.

theorem Schoenflies.segment_crosscut_at_most_two {D : Set Plane} {a b : Plane} (hab : a ≠ b) (hDopen : IsOpen D) (hDconn : IsPreconnected D) (ha : a ∉ D) (hb : b ∉ D) (hPD : segment ℝ a b \ {a, b} ⊆ D) : ∃ zL ∈ D \ segment ℝ a b, ∃ zR ∈ D \ segment ℝ a b, ∀ x ∈ D \ segment ℝ a b, x ∈ connectedComponentIn (D \ segment ℝ a b) zL ∨ x ∈ connectedComponentIn (D \ segment ℝ a b) zR

A straight crosscut cuts a region into at most two pieces, with no hypothesis left standing: hasArcCollars_segment discharges the collar.

theorem Schoenflies.crosscut_components_exhaust {D P : Set Plane} {a b v₁ v₂ : Plane} (hDopen : IsOpen D) (hDconn : IsPreconnected D) (hP : IsArcBetween P a b) (hPpoly : IsPolygonal P) (ha : a ∉ D) (hb : b ∉ D) (hPD : P \ {a, b} ⊆ D) (hcollars : HasArcCollars D P) (h₁ : v₁ ∈ D \ P) (h₂ : v₂ ∈ D \ P) (hne : connectedComponentIn (D \ P) v₁ ≠ connectedComponentIn (D \ P) v₂) (x : Plane) : x ∈ D \ P → x ∈ connectedComponentIn (D \ P) v₁ ∨ x ∈ connectedComponentIn (D \ P) v₂

Lemma "At most two sides", in the form the crosscut theorem consumes. Two distinct components of D ∖ P exhaust it.