Two-sided polygonal strips

This module builds the collar of Lemma 1.8: an open neighbourhood N of a simple closed polygon P whose complement in N splits into two connected open sets, the two local sides.

The blueprint's construction is "a small closed disk about every vertex, a thin rectangular block about every edge, chosen so that consecutive blocks overlap and nonadjacent closures are disjoint". The blocks here are

• Plane.cone v A R — the open sector of radius R about a vertex v cut out by an arc A of directions, and
• Plane.strip a u t₁ t₂ s₁ s₂ — the open rectangle around a directed edge, written in the edge's own coordinates t = ⟪u, x - a⟫ (along) and s = det u (x - a) (across).

Everything about the side matching at a vertex comes from Schoenflies/Direction.lean through the orientation form; no angle is named. The one new direction fact needed here is the sign-free repackaging Plane.germs_split': the blueprint's germs_split assumes 0 < det r₁ r₂, but a polygon turns both ways, and it turns out that which named arc carries the left germs does not depend on the sense of the turn — it is always arcCCW r₂ r₁. Only the side of the smallness hypothesis moves.

The constants

The blueprint says "the blocks may be chosen so that consecutive edge and vertex blocks overlap in the prescribed small rectangles around the radial segments, while the closures of all nonadjacent blocks are disjoint" without naming the constants. Schoenflies.StripData names them: a cone radius R, a trim lam by which each edge block stops short of its endpoints, and a half-width rho. They should be chosen in this order (this is the recipe the unproved exists_stripData has to follow):

1. R from the vertex separations, from the distance of each vertex to the nonincident edges (with a factor 2 of slack, spent in dist_core_vertex), and from the prescribed open set;
2. lam := R / 5, which makes 2 * lam < R (the cones reach past the ends of the blocks they must overlap) and 4 * lam < ‖edge‖ (the blocks are nonempty);
3. rho from the distance of each trimmed edge to the other edges, and from the germ threshold rho * (1 + |⟪r₁, r₂⟫|) ≤ lam * |det r₁ r₂| at every vertex — this last is the quantitative form of "make the strips narrow enough that this side matching holds in every vertex disk", and it is the only inequality in the list that is not a separation of compact sets.

Blueprint

• Plane.germs_split' — the sign-free vertex matching inside Lemma 1.8.
• Schoenflies.ClosedPolygon — a simple closed polygonal curve presented by its cyclic vertex list.
• Schoenflies.StripData — the choice of constants, as a hypothesis.
• Schoenflies.StripData.sideL, .sideR, .nbhd, .sideL_disjoint_sideR — the two labelled sides of the collar, and that they are disjoint.

Where the rest of Lemma 1.8 lives

This module builds the apparatus and proves the hard half: the germ matching at a corner and the disjointness of the two labelled sides. The other two obligations are discharged next door, and were split out only because they were built concurrently:

• Schoenflies/StripConstants.lean — exists_stripData and exists_stripData_subset, which produce the constants, the latter with the collar inside a prescribed open set.
• Schoenflies/StripConnected.lean — that each side is connected, and nbhd \ carrier = sideL ∪ sideR.

Schoenflies.polygonal_collar in Schoenflies/Compose.lean is the three composed into the blueprint's Lemma 1.8 (a). ClosedPolygon.collar below is a definition, not the theorem.

What is still missing from Lemma 1.8 as a whole: the local two-sidedness clause (every sufficiently small disk about a point of the curve meets the complement in exactly two components, one in each side), and part (b), the arc case.

A sign-free vertex matching

Plane.germs_split fixes the orientation with 0 < det r₁ r₂. A polygon turns both ways, so the collar needs the statement without that hypothesis. The content of the repackaging is that the conclusion does not move: the two left germs always land on arcCCW r₂ r₁ and the two right germs on arcCCW r₁ r₂. What moves is which pair needs the smallness hypothesis, so the sign-free form simply imposes it on both, with absolute values.

theorem Schoenflies.Plane.germs_split' {r₁ r₂ : Plane} {t s : ℝ} (h : r₁.det r₂ ≠ 0) (hs : 0 < s) (hsmall : s * |inner ℝ r₁ r₂| < t * |r₁.det r₂|) : (t • r₁ - s • r₁.perp ∈ r₂.arcCCW r₁ ∧ t • r₂ + s • r₂.perp ∈ r₂.arcCCW r₁) ∧ t • r₁ + s • r₁.perp ∈ r₁.arcCCW r₂ ∧ t • r₂ - s • r₂.perp ∈ r₁.arcCCW r₂

The vertex matching, sign-free. With r₁ the ray back along the incoming edge and r₂ the ray out along the outgoing edge, the two left half-strip germs lie on arcCCW r₂ r₁ and the two right ones on arcCCW r₁ r₂, whichever way the polygon turns. The hypothesis s * |⟪r₁, r₂⟫| < t * |det r₁ r₂| is the blueprint's "s/t small", written without a division and without a sign.

The two arcs, without a sign hypothesis

theorem Schoenflies.Plane.arcCCW_disjoint' {r₁ r₂ : Plane} (h : r₁.det r₂ ≠ 0) : Disjoint (r₁.arcCCW r₂) (r₂.arcCCW r₁)

The two arcs bounded by a pair of rays are disjoint, whichever the sign of det r₁ r₂.

theorem Schoenflies.Plane.mem_ray_or_mem_arcCCW' {d r₁ r₂ : Plane} (h : r₁.det r₂ ≠ 0) (hd : d ≠ 0) : (∃ (c : ℝ), 0 < c ∧ d = c • r₁) ∨ (∃ (c : ℝ), 0 < c ∧ d = c • r₂) ∨ d ∈ r₁.arcCCW r₂ ∨ d ∈ r₂.arcCCW r₁

The two rays and the two arcs exhaust the nonzero vectors, whichever the sign of det r₁ r₂.

theorem Schoenflies.Plane.notMem_arcCCW_smul {c : ℝ} (u w : Plane) (hc : 0 ≤ c) : c • u ∉ u.arcCCW w ∧ c • u ∉ w.arcCCW u

A nonnegative multiple of a bounding ray lies on neither arc: the arcs are open, and 0 is on neither. This is what keeps the two incident edges out of the vertex sectors.

theorem Schoenflies.Plane.isLinearMap_det_right (u : Plane) : IsLinearMap ℝ fun (d : Plane) => u.det d

Half-spaces through the origin are convex; det u · is linear.

theorem Schoenflies.Plane.isLinearMap_det_left (w : Plane) : IsLinearMap ℝ fun (d : Plane) => d.det w

theorem Schoenflies.Plane.convex_det_right_pos (u : Plane) : Convex ℝ {d : Plane | 0 < u.det d}

theorem Schoenflies.Plane.convex_det_right_neg (u : Plane) : Convex ℝ {d : Plane | u.det d < 0}

theorem Schoenflies.Plane.convex_det_left_pos (w : Plane) : Convex ℝ {d : Plane | 0 < d.det w}

theorem Schoenflies.Plane.convex_det_left_neg (w : Plane) : Convex ℝ {d : Plane | d.det w < 0}

theorem Schoenflies.Plane.isConnected_arcCCW_ball {u w : Plane} {ρ : ℝ} (h : u.det w ≠ 0) (hρ : 0 < ρ) : IsConnected (u.arcCCW w ∩ Metric.ball 0 ρ)

An arc met with a ball about the origin is connected. When the arc is the short one it is an intersection of two half-planes, hence convex; when it is the long one it is a union of two half-planes, and -(u + w) lies in both.

Vertex sectors

The "small closed disk about a vertex" of the blueprint is replaced by an open sector: the part of a ball about the vertex lying in a prescribed arc of directions. The two sectors cut out by the two arcs are exactly the two components of the ball minus the two incident radial segments, which is what makes the labelling at a vertex well defined.

def Schoenflies.Plane.cone (v : Plane) (A : Set Plane) (ρ : ℝ) : Set Plane

The open sector of radius ρ about v spanned by the set A of directions.

Equations

• v.cone A ρ = {x : Schoenflies.Plane | x - v ∈ A} ∩ Metric.ball v ρ

theorem Schoenflies.Plane.mem_cone_iff {x : Plane} {ρ : ℝ} {v : Plane} {A : Set Plane} : x ∈ v.cone A ρ ↔ x - v ∈ A ∧ dist x v < ρ

theorem Schoenflies.Plane.cone_subset_ball {ρ : ℝ} {v : Plane} {A : Set Plane} : v.cone A ρ ⊆ Metric.ball v ρ

theorem Schoenflies.Plane.isOpen_cone {ρ : ℝ} {v : Plane} {A : Set Plane} (hA : IsOpen A) : IsOpen (v.cone A ρ)

theorem Schoenflies.Plane.cone_eq_image (v : Plane) (A : Set Plane) (ρ : ℝ) : v.cone A ρ = (fun (d : Plane) => v + d) '' (A ∩ Metric.ball 0 ρ)

A sector is the translate of an arc met with a ball at the origin, so it inherits its connectedness from Plane.isConnected_arcCCW_ball.

theorem Schoenflies.Plane.isConnected_cone_arcCCW {u w : Plane} {ρ : ℝ} (v : Plane) (h : u.det w ≠ 0) (hρ : 0 < ρ) : IsConnected (v.cone (u.arcCCW w) ρ)

Edge blocks

The block around a directed edge is described in the edge's own frame: coordAlong is the progress along the edge and coordAcross the signed distance to its line. Both are affine, so the block is an intersection of four open half-planes — open and convex at a glance.

noncomputable def Schoenflies.Plane.coordAlong (a u x : Plane) : ℝ

Progress along the directed edge that starts at a with unit tangent u.

Equations

• a.coordAlong u x = inner ℝ u (x - a)

def Schoenflies.Plane.coordAcross (a u x : Plane) : ℝ

Signed distance from x to the line of the directed edge that starts at a with unit tangent u; positive on the left.

Equations

• a.coordAcross u x = u.det (x - a)

theorem Schoenflies.Plane.det_eq_inner_perp (u v : Plane) : u.det v = inner ℝ u.perp v

The orientation form is the inner product against the turned vector.

theorem Schoenflies.Plane.abs_det_le (u v : Plane) : |u.det v| ≤ ‖u‖ * ‖v‖

@[simp]

theorem Schoenflies.Plane.coordAlong_param {u : Plane} (hu : u.IsDirection) (a : Plane) (t s : ℝ) : a.coordAlong u (a + t • u + s • u.perp) = t

@[simp]

theorem Schoenflies.Plane.coordAcross_param {u : Plane} (hu : u.IsDirection) (a : Plane) (t s : ℝ) : a.coordAcross u (a + t • u + s • u.perp) = s

theorem Schoenflies.Plane.frame_decomp {u : Plane} (hu : u.IsDirection) (a x : Plane) : x = a + a.coordAlong u x • u + a.coordAcross u x • u.perp

The frame is complete: every point is recovered from its two coordinates.

theorem Schoenflies.Plane.abs_coordAlong_sub_le {u : Plane} (hu : u.IsDirection) (a x y : Plane) : |a.coordAlong u x - a.coordAlong u y| ≤ dist x y

Both coordinates are 1-Lipschitz, which is how a small ball about a point of the edge stays inside the block.

theorem Schoenflies.Plane.abs_coordAcross_sub_le {u : Plane} (hu : u.IsDirection) (a x y : Plane) : |a.coordAcross u x - a.coordAcross u y| ≤ dist x y

def Schoenflies.Plane.strip (a u : Plane) (t₁ t₂ s₁ s₂ : ℝ) : Set Plane

The open block around the directed edge from a with unit tangent u: the points whose progress lies in (t₁, t₂) and whose signed distance lies in (s₁, s₂).

Equations

• a.strip u t₁ t₂ s₁ s₂ = {x : Schoenflies.Plane | t₁ < a.coordAlong u x ∧ a.coordAlong u x < t₂ ∧ s₁ < a.coordAcross u x ∧ a.coordAcross u x < s₂}

theorem Schoenflies.Plane.mem_strip_iff {u a x : Plane} {t₁ t₂ s₁ s₂ : ℝ} : x ∈ a.strip u t₁ t₂ s₁ s₂ ↔ t₁ < a.coordAlong u x ∧ a.coordAlong u x < t₂ ∧ s₁ < a.coordAcross u x ∧ a.coordAcross u x < s₂

theorem Schoenflies.Plane.continuous_coordAlong (a u : Plane) : Continuous (a.coordAlong u)

theorem Schoenflies.Plane.continuous_coordAcross (a u : Plane) : Continuous (a.coordAcross u)

theorem Schoenflies.Plane.isOpen_strip (a u : Plane) (t₁ t₂ s₁ s₂ : ℝ) : IsOpen (a.strip u t₁ t₂ s₁ s₂)

theorem Schoenflies.Plane.convex_strip (a u : Plane) (t₁ t₂ s₁ s₂ : ℝ) : Convex ℝ (a.strip u t₁ t₂ s₁ s₂)

theorem Schoenflies.Plane.mem_strip_param {u : Plane} (hu : u.IsDirection) (a : Plane) {t s t₁ t₂ s₁ s₂ : ℝ} : a + t • u + s • u.perp ∈ a.strip u t₁ t₂ s₁ s₂ ↔ t₁ < t ∧ t < t₂ ∧ s₁ < s ∧ s < s₂

theorem Schoenflies.Plane.dist_foot {u : Plane} (hu : u.IsDirection) (a x : Plane) : dist x (a + a.coordAlong u x • u) = |a.coordAcross u x|

A point of a block is at distance |coordAcross| from the foot of its perpendicular on the edge line, which is the point of the edge with the same progress.

Simple closed polygons

A polygon is presented by its cyclic vertex list. Indexing by ZMod (m + 3) builds in both the cyclic successor and the requirement that there are at least three vertices, and it makes NeZero available without a side hypothesis.

structure Schoenflies.ClosedPolygon (m : ℕ) : Type

A simple closed polygonal curve, presented by its cyclic vertex list.

• vertex : ZMod (m + 3) → Plane

  The vertices, in cyclic order.

• vertex_inj : Function.Injective self.vertex

  The vertices are distinct.

• edges_meet (i j : ZMod (m + 3)) : i ≠ j → segment ℝ (self.vertex i) (self.vertex (i + 1)) ∩ segment ℝ (self.vertex j) (self.vertex (j + 1)) ⊆ {self.vertex i, self.vertex (i + 1)}

  Simplicity: an edge meets any other edge only at one of its own endpoints.

• corner (i : ZMod (m + 3)) : (self.vertex (i - 1) - self.vertex i).det (self.vertex (i + 1) - self.vertex i) ≠ 0

  No redundant vertex: the two edges at a vertex are not collinear. The blueprint deletes such vertices before starting, and the vertex matching needs det ≠ 0 there.

theorem Schoenflies.ClosedPolygon.one_ne_zero' {m : ℕ} : 1 ≠ 0

theorem Schoenflies.ClosedPolygon.succ_ne_self {m : ℕ} (i : ZMod (m + 3)) : i + 1 ≠ i

theorem Schoenflies.ClosedPolygon.vertex_ne {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) : P.vertex i ≠ P.vertex (i + 1)

Edges, in their own frame

noncomputable def Schoenflies.ClosedPolygon.len {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) : ℝ

The length of the edge leaving vertex i.

Equations

• P.len i = ‖P.vertex (i + 1) - P.vertex i‖

noncomputable def Schoenflies.ClosedPolygon.tang {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) : Plane

The unit tangent of the edge leaving vertex i, which is also the outgoing ray at i.

Equations

• P.tang i = (P.vertex (i + 1) - P.vertex i).dir

noncomputable def Schoenflies.ClosedPolygon.rayIn {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) : Plane

The incoming ray at vertex i: the direction back along the edge that arrives there.

Equations

• P.rayIn i = (P.vertex (i - 1) - P.vertex i).dir

noncomputable def Schoenflies.ClosedPolygon.off {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) (t s : ℝ) : Plane

The point of the plane at progress t and signed offset s in the frame of edge i.

Equations

• P.off i t s = P.vertex i + t • P.tang i + s • (P.tang i).perp

noncomputable def Schoenflies.ClosedPolygon.pt {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) (c : ℝ) : Plane

The point of edge i at distance c from its initial vertex.

Equations

• P.pt i c = P.off i c 0

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

The edge leaving vertex i.

Equations

• P.edge i = segment ℝ (P.vertex i) (P.vertex (i + 1))

def Schoenflies.ClosedPolygon.carrier {m : ℕ} (P : ClosedPolygon m) : Set Plane

The carrier of the polygon: the union of its edges.

Equations

• P.carrier = ⋃ (i : ZMod (m + 3)), P.edge i

theorem Schoenflies.ClosedPolygon.sub_ne_zero_of_edge {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : P.vertex (i + 1) - P.vertex i ≠ 0

theorem Schoenflies.ClosedPolygon.len_pos {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : 0 < P.len i

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

theorem Schoenflies.ClosedPolygon.len_smul_tang {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : P.len i • P.tang i = P.vertex (i + 1) - P.vertex i

theorem Schoenflies.ClosedPolygon.off_zero_zero {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : P.off i 0 0 = P.vertex i

theorem Schoenflies.ClosedPolygon.pt_zero {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : P.pt i 0 = P.vertex i

theorem Schoenflies.ClosedPolygon.pt_len {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : P.pt i (P.len i) = P.vertex (i + 1)

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

theorem Schoenflies.ClosedPolygon.pt_sub_vertex {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {c : ℝ} : P.pt i c - P.vertex i = c • P.tang i

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

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

@[simp]

theorem Schoenflies.ClosedPolygon.coordAlong_off {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s : ℝ} : (P.vertex i).coordAlong (P.tang i) (P.off i t s) = t

@[simp]

theorem Schoenflies.ClosedPolygon.coordAcross_off {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s : ℝ} : (P.vertex i).coordAcross (P.tang i) (P.off i t s) = s

theorem Schoenflies.ClosedPolygon.off_coord {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) (x : Plane) : x = P.off i ((P.vertex i).coordAlong (P.tang i) x) ((P.vertex i).coordAcross (P.tang i) x)

Every point is the point of some frame position, so the two coordinates identify it.

theorem Schoenflies.ClosedPolygon.off_injective {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s t' s' : ℝ} (h : P.off i t s = P.off i t' s') : t = t' ∧ s = s'

theorem Schoenflies.ClosedPolygon.mem_edge_iff {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {x : Plane} : x ∈ P.edge i ↔ ∃ c ∈ Set.Icc 0 (P.len i), x = P.pt i c

theorem Schoenflies.ClosedPolygon.pt_mem_edge {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {c : ℝ} (hc : c ∈ Set.Icc 0 (P.len i)) : P.pt i c ∈ P.edge i

theorem Schoenflies.ClosedPolygon.vertex_mem_edge {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : P.vertex i ∈ P.edge i

theorem Schoenflies.ClosedPolygon.vertex_mem_carrier {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : P.vertex i ∈ P.carrier

theorem Schoenflies.ClosedPolygon.edge_subset_carrier {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : P.edge i ⊆ P.carrier

theorem Schoenflies.ClosedPolygon.rayIn_succ {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : P.rayIn (i + 1) = -P.tang i

The incoming ray at i + 1 is the reverse of the tangent of edge i. This is the identity that lets the two germs at a shared vertex be compared.

theorem Schoenflies.ClosedPolygon.vertex_pred_ne {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : P.vertex (i - 1) - P.vertex i ≠ 0

theorem Schoenflies.ClosedPolygon.det_rays_ne_zero {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : (P.rayIn i).det (P.tang i) ≠ 0

theorem Schoenflies.ClosedPolygon.mem_edge_pred_sub {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {x : Plane} (hx : x ∈ P.edge (i - 1)) : ∃ (c : ℝ), 0 ≤ c ∧ x - P.vertex i = c • P.rayIn i

A point of the edge arriving at i is a nonnegative multiple of the incoming ray away from the vertex; a point of the edge leaving i is a nonnegative multiple of the outgoing one. This is what keeps the two incident edges out of both sectors at i.

theorem Schoenflies.ClosedPolygon.mem_edge_sub {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {x : Plane} (hx : x ∈ P.edge i) : ∃ (c : ℝ), 0 ≤ c ∧ x - P.vertex i = c • P.tang i

theorem Schoenflies.ClosedPolygon.pt_eq {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {c : ℝ} : P.pt i c = P.vertex i + c • P.tang i

The constants

StripData is the blueprint's "choose the blocks so that consecutive ones overlap and nonadjacent closures are disjoint", with every constant named. The three numbers are a cone radius R, a trim lam and a half-width rho; the separation hypotheses are exactly the instances of Lemma 1.4 (b) that the construction consumes, and germ is the vertex-matching threshold. Producing them is the unproved exists_stripData; see the Status section.

structure Schoenflies.StripData {m : ℕ} (P : ClosedPolygon m) : Type

The constants of the collar of a simple closed polygon.

• R : ℝ

  The radius of the vertex sectors.

• lam : ℝ

  The distance by which an edge block stops short of each endpoint of its edge.

• rho : ℝ

  The half-width of an edge block.

• rho_pos : 0 < self.rho
• rho_lt_lam : self.rho < self.lam
• two_lam_lt_R : 2 * self.lam < self.R

  The sectors reach past the ends of the blocks they have to overlap.

• four_lam_lt_len (i : ZMod (m + 3)) : 4 * self.lam < P.len i

  The blocks are nonempty, with room to spare at both ends.

• R_le_len (i : ZMod (m + 3)) : self.R ≤ P.len i

  A sector does not run past the far end of an incident edge.

• sep_vertex (i j : ZMod (m + 3)) : i ≠ j → 2 * self.R ≤ dist (P.vertex i) (P.vertex j)

  Distinct vertices are 2R apart, so distinct sectors are disjoint.

• sep_vertex_edge (i j : ZMod (m + 3)) : j ≠ i - 1 → j ≠ i → ∀ y ∈ P.edge j, 2 * self.R ≤ dist (P.vertex i) y

  A vertex is 2R away from every nonincident edge. The factor 2 is the slack that a block of half-width rho ≤ R needs in notMem_sectorL_of_far.

• sep_trim_edge (i j : ZMod (m + 3)) : j ≠ i → ∀ c ∈ Set.Icc self.lam (P.len i - self.lam), ∀ y ∈ P.edge j, 2 * self.rho ≤ dist (P.pt i c) y

  The trimmed edge i is 2 * rho away from every other edge.

• germ (i : ZMod (m + 3)) : self.rho * (1 + |inner ℝ (P.rayIn i) (P.tang i)|) ≤ self.lam * |(P.rayIn i).det (P.tang i)|

  The vertex-matching threshold. This is the only hypothesis that is not a separation of compact sets: it says the blocks are narrow enough, relative to how far they stop short of the vertices, for Plane.germs_split' to apply at every corner.

theorem Schoenflies.StripData.lam_pos {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : 0 < D.lam

theorem Schoenflies.StripData.R_pos {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : 0 < D.R

theorem Schoenflies.StripData.rho_lt_R {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : D.rho < D.R

The four families of blocks

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

The left block of edge i.

Equations

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

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

The right block of edge i.

Equations

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

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

The left sector at vertex i: the arc arcCCW (tang i) (rayIn i) is the one carrying both left germs, by Plane.germs_split'.

Equations

• D.sectorL i = (P.vertex i).cone ((P.tang i).arcCCW (P.rayIn i)) D.R

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

The right sector at vertex i.

Equations

• D.sectorR i = (P.vertex i).cone ((P.rayIn i).arcCCW (P.tang i)) D.R

def Schoenflies.StripData.sideL {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : Set Plane

The left side of the collar.

Equations

• D.sideL = ⋃ (i : ZMod (m + 3)), D.sectorL i ∪ D.blockL i

def Schoenflies.StripData.sideR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : Set Plane

The right side of the collar.

Equations

• D.sideR = ⋃ (i : ZMod (m + 3)), D.sectorR i ∪ D.blockR i

def Schoenflies.StripData.nbhd {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : Set Plane

The collar itself.

Equations

• D.nbhd = D.sideL ∪ D.sideR ∪ P.carrier

theorem Schoenflies.StripData.mem_blockL_iff {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} : x ∈ D.blockL i ↔ D.lam < (P.vertex i).coordAlong (P.tang i) x ∧ (P.vertex i).coordAlong (P.tang i) x < P.len i - D.lam ∧ 0 < (P.vertex i).coordAcross (P.tang i) x ∧ (P.vertex i).coordAcross (P.tang i) x < D.rho

theorem Schoenflies.StripData.mem_blockR_iff {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} : x ∈ D.blockR i ↔ D.lam < (P.vertex i).coordAlong (P.tang i) x ∧ (P.vertex i).coordAlong (P.tang i) x < P.len i - D.lam ∧ -D.rho < (P.vertex i).coordAcross (P.tang i) x ∧ (P.vertex i).coordAcross (P.tang i) x < 0

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

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

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

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

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

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

theorem Schoenflies.StripData.convex_blockL {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : Convex ℝ (D.blockL i)

theorem Schoenflies.StripData.convex_blockR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} : Convex ℝ (D.blockR i)

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

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

Where the blocks live

A block sits inside the rho-neighbourhood of the trimmed edge, and a sector inside the ball of radius R about its vertex. Every "nonadjacent blocks are disjoint" step below is one of these two containments against one of the separation hypotheses.

theorem Schoenflies.StripData.exists_foot {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} (h : x ∈ D.blockL i ∪ D.blockR i) : ∃ c ∈ Set.Icc D.lam (P.len i - D.lam), dist x (P.pt i c) < D.rho

The foot of the perpendicular from a point of a block lies on the trimmed edge, within rho of the point.

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

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

The germ argument at a vertex

These four lemmas are the whole content of "at a vertex the left sides of the incoming and outgoing strips enter the same component of the vertex disk minus the two incident rays". Each is one projection of Plane.germs_split', applied to the frame decomposition of a point of a block.

theorem Schoenflies.StripData.germ_ineq {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {t s : ℝ} (ht : D.lam < t) (hs0 : 0 < s) (hs : s < D.rho) : s * |inner ℝ (P.rayIn i) (P.tang i)| < t * |(P.rayIn i).det (P.tang i)|

The threshold hypothesis, specialised to a point of a block.

theorem Schoenflies.StripData.blockL_sub_mem_arcL_start {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} (h : x ∈ D.blockL i) : x - P.vertex i ∈ (P.tang i).arcCCW (P.rayIn i)

A point of the left block of edge i, seen from the vertex it leaves, is the outgoing left germ, hence in the left arc there.

theorem Schoenflies.StripData.blockL_sub_mem_arcL_finish {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} (h : x ∈ D.blockL i) : x - P.vertex (i + 1) ∈ (P.tang (i + 1)).arcCCW (P.rayIn (i + 1))

The same point, seen from the vertex it arrives at, is the incoming left germ.

theorem Schoenflies.StripData.blockR_sub_mem_arcR_start {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} (h : x ∈ D.blockR i) : x - P.vertex i ∈ (P.rayIn i).arcCCW (P.tang i)

A point of the right block of edge i, seen from the vertex it leaves, is the outgoing right germ, hence in the right arc there.

theorem Schoenflies.StripData.blockR_sub_mem_arcR_finish {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} (h : x ∈ D.blockR i) : x - P.vertex (i + 1) ∈ (P.rayIn (i + 1)).arcCCW (P.tang (i + 1))

The same point, seen from the vertex it arrives at, is the incoming right germ.

Nonadjacent blocks are disjoint

Everything here is one of the separation hypotheses of StripData against one of the two containments exists_foot and sector_subset_ball.

theorem Schoenflies.StripData.pt_mem_edge_of_trim {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {c : ℝ} (hc : c ∈ Set.Icc D.lam (P.len i - D.lam)) : P.pt i c ∈ P.edge i

theorem Schoenflies.StripData.block_notMem_edge {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i j : ZMod (m + 3)} {x : Plane} (h : x ∈ D.blockL i ∪ D.blockR i) (hj : j ≠ i) : x ∉ P.edge j

A block misses every edge but its own.

theorem Schoenflies.StripData.block_notMem_own_edge {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} (h : x ∈ D.blockL i ∪ D.blockR i) : x ∉ P.edge i

A block misses its own edge, because its points have nonzero offset.

theorem Schoenflies.StripData.block_notMem_carrier {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} (h : x ∈ D.blockL i ∪ D.blockR i) : x ∉ P.carrier

theorem Schoenflies.StripData.block_notMem_ball_vertex {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i j : ZMod (m + 3)} {x : Plane} (h : x ∈ D.blockL i ∪ D.blockR i) (hj1 : j ≠ i) (hj2 : j ≠ i + 1) : x ∉ Metric.ball (P.vertex j) D.R

A block stays out of the sectors at every vertex other than its own two.

theorem Schoenflies.StripData.sector_notMem_far_edge {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i j : ZMod (m + 3)} {x : Plane} (h : x ∈ Metric.ball (P.vertex i) D.R) (hj1 : j ≠ i - 1) (hj2 : j ≠ i) : x ∉ P.edge j

A sector misses every edge that is not incident to its vertex.

theorem Schoenflies.StripData.sectorL_notMem_carrier {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} (h : x ∈ D.sectorL i) : x ∉ P.carrier

A sector misses the two edges incident to its vertex: their points lie on the two bounding rays, and the arcs are open.

theorem Schoenflies.StripData.sectorR_notMem_carrier {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {x : Plane} (h : x ∈ D.sectorR i) : x ∉ P.carrier

theorem Schoenflies.StripData.sideL_disjoint_carrier {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : Disjoint D.sideL P.carrier

theorem Schoenflies.StripData.sideR_disjoint_carrier {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : Disjoint D.sideR P.carrier

The two sides are disjoint

Four families times four families. The pairs with distinct indices are settled by distance; the pairs at a shared index are settled by Plane.arcCCW_disjoint' through the germ lemmas.

theorem Schoenflies.StripData.blockL_disjoint_blockR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i j : ZMod (m + 3)} {x : Plane} (hL : x ∈ D.blockL i) (hR : x ∈ D.blockR j) : False

theorem Schoenflies.StripData.blockL_disjoint_sectorR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i j : ZMod (m + 3)} {x : Plane} (hL : x ∈ D.blockL i) (hR : x ∈ D.sectorR j) : False

theorem Schoenflies.StripData.sectorL_disjoint_blockR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i j : ZMod (m + 3)} {x : Plane} (hL : x ∈ D.sectorL i) (hR : x ∈ D.blockR j) : False

theorem Schoenflies.StripData.sectorL_disjoint_sectorR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i j : ZMod (m + 3)} {x : Plane} (hL : x ∈ D.sectorL i) (hR : x ∈ D.sectorR j) : False

theorem Schoenflies.StripData.sideL_disjoint_sideR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : Disjoint D.sideL D.sideR