The collar of a closed polygon is two-sided

Schoenflies/Strip.lean builds the blocks of Lemma 1.8 and proves the hard local half of the statement: the two labelled sides are disjoint. This module closes the lemma for a closed polygon by supplying the two remaining global facts.

• Each side is connected. The blueprint says "consecutive edge and vertex blocks overlap in a nonempty labelled half-strip, so the union of all left pieces is connected". Here that overlap is produced explicitly: StripData.mem_overlapL_start puts the point at frame position (3 lam / 2, rho / 2) in both blockL i and sectorL i, and StripData.mem_overlapL_finish puts the point at (len i - 3 lam / 2, rho / 2) in both blockL i and sectorL (i + 1). The two StripData constraints that make these work are exactly the two the structure advertises for the purpose: four_lam_lt_len keeps the frame position inside the block, and two_lam_lt_R keeps it inside the sector, since 3 lam / 2 + rho / 2 < 2 lam < R.

  The chaining is then a finite induction along chainL, and it does not need the wrap-around: connectedness of a union of connected sets only needs some spanning tree of the overlap graph, and the linear chain 0, 1, …, m + 2 is one. The blueprint's "the labels return consistently after one circuit" is a statement about the labelling, not about connectedness, and it is Strip.sideL_disjoint_sideR, already proved: it is what makes sideL and sideR two sets rather than one.

• The collar is a neighbourhood, and removing the curve leaves exactly the two sides. StripData.nbhd_diff_carrier is immediate from the two disjointness results of Strip.lean. Openness of nbhd is not: nbhd contains the curve, so it has to be recognised as a union of open sets. StripData.nbhd_eq does that, rewriting it as the union of the vertex balls and the full edge tubes; the two inclusions are ball_diff_carrier_subset and tube_diff_carrier_subset one way, and the covering of each edge by "near the first vertex, near the second vertex, or in the trimmed middle" the other way.

Blueprint

• Schoenflies.StripData.isConnected_sideL, .isConnected_sideR — "the union of all left pieces is connected; the same is true on the right", inside Lemma 1.8 (a).
• Schoenflies.StripData.nbhd_diff_carrier — N \ P = N_L ⊔ N_R, Lemma 1.8 (a).
• Schoenflies.StripData.collar — Lemma 1.8 (a) for a closed polygon, given the constants.

Producing the constants is exists_stripData, which lives elsewhere; every statement here is for a given D : StripData P, exactly as in Schoenflies/Strip.lean.

Two frames at one edge

Everything below needs the edge frame read from both ends: Strip.lean has the departure end, and the overlap with the sector at the far vertex needs the arrival end.

theorem Schoenflies.ClosedPolygon.isDirection_rayIn {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : (P.rayIn i).IsDirection

The incoming ray at a vertex is a unit vector.

theorem Schoenflies.ClosedPolygon.off_sub_vertex_succ {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s : ℝ} : P.off i t s - P.vertex (i + 1) = (t - P.len i) • P.tang i + s • (P.tang i).perp

The far vertex of edge i sits at frame position (len i, 0).

theorem Schoenflies.ClosedPolygon.dist_off_vertex_succ_le {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s : ℝ} : dist (P.off i t s) (P.vertex (i + 1)) ≤ |t - P.len i| + |s|

The block-to-far-sector distance bound, the mirror of dist_off_vertex_le.

theorem Schoenflies.ClosedPolygon.dist_pt_vertex_succ {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {c : ℝ} : dist (P.pt i c) (P.vertex (i + 1)) = |c - P.len i|

The distance from a point of edge i to the edge's far endpoint, the mirror of dist_pt_vertex.

The two incident edges, as rays out of a vertex

mem_edge_sub and mem_edge_pred_sub read a point of an incident edge as a multiple of a ray. The converses are what says that a ball about a vertex minus the curve is covered by the two sectors: a direction on one of the two rays is on the curve, not beside it.

theorem Schoenflies.ClosedPolygon.vertex_add_smul_rayIn {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) (c : ℝ) : P.vertex i + c • P.rayIn i = P.pt (i - 1) (P.len (i - 1) - c)

Walking back along the incoming ray from vertex i traverses the previous edge.

theorem Schoenflies.ClosedPolygon.mem_edge_pred_of_smul_rayIn {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {c : ℝ} (hc0 : 0 ≤ c) (hc1 : c ≤ P.len (i - 1)) : P.vertex i + c • P.rayIn i ∈ P.edge (i - 1)

A point of the incoming ray at distance at most the previous edge's length lies on that edge.

theorem Schoenflies.ClosedPolygon.mem_edge_of_smul_tang {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {c : ℝ} (hc0 : 0 ≤ c) (hc1 : c ≤ P.len i) : P.vertex i + c • P.tang i ∈ P.edge i

A point of the outgoing ray at distance at most the edge's length lies on that edge.

The overlaps

The blueprint's "consecutive edge and vertex blocks overlap in a nonempty labelled half-strip". Both witnesses sit at across-coordinate rho / 2, at along-coordinate 3 lam / 2 from the vertex in question. The two hypotheses of StripData that were put there for this are four_lam_lt_len — which gives 3 lam / 2 < len i - lam, so the point is inside the block — and two_lam_lt_R together with rho < lam — which gives 3 lam / 2 + rho / 2 < 2 lam < R, so the point is inside the sector.

theorem Schoenflies.StripData.lam_lt_three_halves_lam {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : D.lam < 3 * D.lam / 2

The along-coordinate of the witnesses clears the near trim.

theorem Schoenflies.StripData.three_halves_lam_lt {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : 3 * D.lam / 2 < P.len i - D.lam

…and stays short of the far one, by four_lam_lt_len.

theorem Schoenflies.StripData.overlap_dist_lt {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : 3 * D.lam / 2 + D.rho / 2 < D.R

…and the whole witness stays inside the sector, by rho_lt_lam and two_lam_lt_R.

theorem Schoenflies.StripData.mem_overlapL_start {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : P.off i (3 * D.lam / 2) (D.rho / 2) ∈ D.blockL i ∩ D.sectorL i

The overlap at the departure vertex. The point at frame position (3 lam / 2, rho / 2) of edge i lies both in the left block of that edge and in the left sector at i.

theorem Schoenflies.StripData.mem_overlapL_finish {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : P.off i (P.len i - 3 * D.lam / 2) (D.rho / 2) ∈ D.blockL i ∩ D.sectorL (i + 1)

The overlap at the arrival vertex. The point at frame position (len i - 3 lam / 2, rho / 2) of edge i lies both in the left block of that edge and in the left sector at i + 1.

theorem Schoenflies.StripData.mem_overlapR_start {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : P.off i (3 * D.lam / 2) (-(D.rho / 2)) ∈ D.blockR i ∩ D.sectorR i

The right-hand mirror of mem_overlapL_start.

theorem Schoenflies.StripData.mem_overlapR_finish {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : P.off i (P.len i - 3 * D.lam / 2) (-(D.rho / 2)) ∈ D.blockR i ∩ D.sectorR (i + 1)

The right-hand mirror of mem_overlapL_finish.

theorem Schoenflies.StripData.blockL_nonempty {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : (D.blockL i).Nonempty

theorem Schoenflies.StripData.blockR_nonempty {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : (D.blockR i).Nonempty

theorem Schoenflies.StripData.isConnected_blockL {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : IsConnected (D.blockL i)

theorem Schoenflies.StripData.isConnected_blockR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : IsConnected (D.blockR i)

Chaining a cyclic family

The union of the left pieces is connected because consecutive pieces overlap. This is a fact about any cyclically indexed family, and it is worth isolating: it is used once on the left and once on the right, and it is where the "cyclic" of the blueprint gets examined.

The point to notice is that the closing overlap F (last) ∩ F 0 is not used. A union of connected sets is connected as soon as the overlap graph is connected, and the path 0 — 1 — ⋯ — N-1 already spans it; the extra edge back to 0 is a cycle, not a new vertex. The blueprint's "the labels return consistently after one circuit" is therefore not needed here: it is needed to know that the left label and the right label never collide, which is StripData.sideL_disjoint_sideR, and that is already proved.

theorem Schoenflies.isConnected_iUnion_zmod {α : Type u_1} [TopologicalSpace α] {N : ℕ} [NeZero N] (F : ZMod N → Set α) (hconn : ∀ (i : ZMod N), IsConnected (F i)) (hmeet : ∀ (i : ZMod N), (F i ∩ F (i + 1)).Nonempty) : IsConnected (⋃ (i : ZMod N), F i)

A cyclically indexed family of connected sets in which every member meets its successor has connected union. Only the overlaps along the linear chain 0, 1, …, N - 1 are consumed.

The two sides are connected

def Schoenflies.StripData.pieceL {m : ℕ} {P : ClosedPolygon m} (D : StripData P) (i : ZMod (m + 3)) : Set Plane

The left piece at index i: the left sector at vertex i glued to the left block of the edge leaving i.

Equations

• D.pieceL i = D.sectorL i ∪ D.blockL i

def Schoenflies.StripData.pieceR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) (i : ZMod (m + 3)) : Set Plane

The right piece at index i.

Equations

• D.pieceR i = D.sectorR i ∪ D.blockR i

theorem Schoenflies.StripData.sideL_eq_iUnion {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : D.sideL = ⋃ (i : ZMod (m + 3)), D.pieceL i

theorem Schoenflies.StripData.sideR_eq_iUnion {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : D.sideR = ⋃ (i : ZMod (m + 3)), D.pieceR i

theorem Schoenflies.StripData.isConnected_pieceL {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : IsConnected (D.pieceL i)

A piece is connected: its sector and its block overlap, at mem_overlapL_start.

theorem Schoenflies.StripData.isConnected_pieceR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : IsConnected (D.pieceR i)

theorem Schoenflies.StripData.pieceL_inter_succ_nonempty {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : (D.pieceL i ∩ D.pieceL (i + 1)).Nonempty

Consecutive pieces overlap: the block of edge i reaches into the sector at i + 1.

theorem Schoenflies.StripData.pieceR_inter_succ_nonempty {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : (D.pieceR i ∩ D.pieceR (i + 1)).Nonempty

theorem Schoenflies.StripData.isConnected_sideL {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : IsConnected D.sideL

The left side of the collar is connected.

theorem Schoenflies.StripData.isConnected_sideR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : IsConnected D.sideR

The right side of the collar is connected.

theorem Schoenflies.StripData.isOpen_sideL {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : IsOpen D.sideL

theorem Schoenflies.StripData.isOpen_sideR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : IsOpen D.sideR

The collar minus the curve is exactly the two sides

nbhd was defined as sideL ∪ sideR ∪ carrier, so this is only the two disjointness statements of Strip.lean read backwards.

theorem Schoenflies.StripData.nbhd_diff_carrier {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : D.nbhd \ P.carrier = D.sideL ∪ D.sideR

Lemma 1.8 (a), the set equality. Removing the curve from the collar leaves exactly the two labelled sides. With sideL_disjoint_sideR this is N \ P = N_L ⊔ N_R.

theorem Schoenflies.StripData.carrier_subset_nbhd {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : P.carrier ⊆ D.nbhd

The collar is open

nbhd contains the curve, so openness is not formal: it has to be exhibited as a union of open sets. The two families are the vertex balls and the full edge tubes — the block of half-width rho on both sides of the trimmed edge, core included. Each of the two is covered by nbhd because its points off the curve are labelled (ball_diff_carrier_subset, tube_diff_carrier_subset); conversely they cover nbhd, the only nontrivial part being that they cover the curve itself, which is the three-way split of an edge into "within R of the first vertex", "within R of the second", and "in the trimmed middle".

def Schoenflies.StripData.tube {m : ℕ} {P : ClosedPolygon m} (D : StripData P) (i : ZMod (m + 3)) : Set Plane

The full tube of edge i: the trimmed edge thickened by rho on both sides. It is the union of the two blocks with the piece of the edge between them.

Equations

• D.tube i = (P.vertex i).strip (P.tang i) D.lam (P.len i - D.lam) (-D.rho) D.rho

theorem Schoenflies.StripData.isOpen_tube {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : IsOpen (D.tube i)

theorem Schoenflies.StripData.mem_tube_off {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {t s : ℝ} : P.off i t s ∈ D.tube i ↔ D.lam < t ∧ t < P.len i - D.lam ∧ -D.rho < s ∧ s < D.rho

theorem Schoenflies.StripData.blockL_subset_tube {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : D.blockL i ⊆ D.tube i

theorem Schoenflies.StripData.blockR_subset_tube {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : D.blockR i ⊆ D.tube i

theorem Schoenflies.StripData.ball_diff_carrier_subset {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : Metric.ball (P.vertex i) D.R \ P.carrier ⊆ D.sectorL i ∪ D.sectorR i

A vertex ball minus the curve is covered by the two sectors at that vertex. A point of the ball off the curve points in some direction from the vertex; by mem_ray_or_mem_arcCCW' that direction is either one of the two incident rays — and then the point is on the incident edge, because R_le_len says the sector does not run past the far end — or on one of the two arcs, and then the point is in the corresponding sector.

theorem Schoenflies.StripData.tube_diff_carrier_subset {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : D.tube i \ P.carrier ⊆ D.blockL i ∪ D.blockR i

A tube minus the curve is its two blocks. The only points of a tube on the curve are those on the core of its own edge.

theorem Schoenflies.StripData.carrier_subset_balls_union_tubes {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : P.carrier ⊆ (⋃ (i : ZMod (m + 3)), Metric.ball (P.vertex i) D.R) ∪ ⋃ (i : ZMod (m + 3)), D.tube i

Each edge is covered by the ball at its first vertex, the ball at its second, and its own tube: lam < R leaves no gap in the middle.

theorem Schoenflies.StripData.nbhd_eq {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : D.nbhd = (⋃ (i : ZMod (m + 3)), Metric.ball (P.vertex i) D.R) ∪ ⋃ (i : ZMod (m + 3)), D.tube i

The collar is the union of the vertex balls and the edge tubes. This is the presentation that makes it visibly open.

theorem Schoenflies.StripData.isOpen_nbhd {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : IsOpen D.nbhd

Lemma 1.8 (a)

theorem Schoenflies.StripData.collar {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : IsOpen D.nbhd ∧ P.carrier ⊆ D.nbhd ∧ D.nbhd \ P.carrier = D.sideL ∪ D.sideR ∧ IsOpen D.sideL ∧ IsOpen D.sideR ∧ IsConnected D.sideL ∧ IsConnected D.sideR ∧ Disjoint D.sideL D.sideR

Two-sided polygonal strips, the closed case. Given the constants, the collar of a simple closed polygon is an open neighbourhood of the curve whose complement in it is the disjoint union of the two connected open local sides. This is Lemma 1.8 (a) of the blueprint, modulo exists_stripData, which produces the constants.

theorem Schoenflies.StripData.exists_collar {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : ∃ (N : Set Plane) (NL : Set Plane) (NR : Set Plane), IsOpen N ∧ P.carrier ⊆ N ∧ IsOpen NL ∧ IsOpen NR ∧ IsConnected NL ∧ IsConnected NR ∧ Disjoint NL NR ∧ N \ P.carrier = NL ∪ NR

The existential form of Lemma 1.8 (a): a simple closed polygonal curve for which the constants exist has an open neighbourhood N with N \ P the disjoint union of two connected open sets.