Two-sided collars along a simple polygonal arc

Schoenflies/CrosscutAtMostTwo.lean proves Lemma "At most two sides" assuming Schoenflies.HasArcCollars: every compact piece of D ∩ P has a two-sided collar inside D. This module discharges that hypothesis for a polygonal arc presented by its vertex list.

The route: a linear chain, not a cyclic one

Schoenflies/Strip.lean builds the collar of blueprint Lemma 1.8 for a ClosedPolygon, whose vertex family is indexed by ZMod (m + 3). The apparatus is redone here on a linear index — route (A) of the three the blueprint's arc case admits. Closing the arc into a polygon (route (B)) was rejected: it needs a return path from one end of the arc back to the other meeting the arc only at its ends, and producing one is the two-sided collar of the arc all over again.

Two things change from the cyclic case, and both make the arc case easier.

• There are no sectors at the two extreme vertices. An edge block already stops short of both of its endpoints by the trim lam, so the collar of the whole chain of blocks is an open neighbourhood of the arc minus two small end caps — which is all that is wanted, because the compact piece K sits at positive distance from the two endpoints of a crosscut (they are outside D and K is inside).
• The neighbourhood is open by construction. The collar of a closed polygon has to contain the curve, so StripData.nbhd is a union of open sets plus the carrier, and StripData.nbhd_eq is needed to see that it is open. Here nbhd is defined outright as the union of the vertex balls and the edge tubes; it contains the arc only away from its two ends, and there is nothing to prove.

What does not change is the germ argument at a corner: Plane.germs_split' is applied exactly as in the cyclic case, with the incoming ray at vertex i + 1 written A.back i and the outgoing one A.tang (i + 1).

The one thing left open

PolyArc is a presentation: a simple polygonal arc given by its vertex list, exactly as ClosedPolygon presents a simple closed polygonal curve. Everything is proved for a PolyArc, and Schoenflies.polyArc_crosscut_at_most_two is Lemma "At most two sides" for one with no hypothesis left standing at all. What is not proved is the converse presentation statement: that a set which happens to be a simple polygonal arc is the carrier of some PolyArc. That is the arc analogue of Schoenflies.exists_closedPolygon, which Schoenflies/Realization.lean proves for a Jordan curve; it is normalisation, not geometry. Schoenflies.hasArcCollars therefore carries it as the hypothesis Schoenflies.IsPolyArcCarrier. See the note at the end of the file for the route.

The presentation is checked in both other directions, so neither the structure nor the hypothesis is vacuous or accidentally false: Schoenflies.PolyArc.isArcBetween_carrier and Schoenflies.PolyArc.isPolygonal_carrier say the carrier of a PolyArc is a simple polygonal arc, and Schoenflies.isPolyArcCarrier_segment exhibits one.

Blueprint

• Schoenflies.PolyArc — a simple polygonal arc presented by its vertex list; the arc analogue of Schoenflies.ClosedPolygon.
• Schoenflies.ArcStrip — the constants of blueprint Lemma 1.8 (b), as a structure: the cone radius R, the trim lam, the half-width rho, and the separations they satisfy. The arc analogue of Schoenflies.StripData, with the two clauses that make the collar fit inside the prescribed region and clear of the two endpoints.
• Schoenflies.ArcStrip.nbhd, .sideL, .sideR — the collar N and its two tracks N_L, N_R of Lemma 1.8 (b).
• Schoenflies.ArcStrip.nbhd_diff_carrier, .isConnected_sideL, .isConnected_sideR, .sideL_disjoint_sideR, .subset_closure_sideL, .subset_closure_sideR — the clauses of Lemma 1.8 (b).
• Schoenflies.exists_arcStrip — the constants exist. The arc analogue of Schoenflies.exists_stripData_subset.
• Schoenflies.ArcStrip.collar, Schoenflies.PolyArc.exists_arcCollar, Schoenflies.PolyArc.hasArcCollars — Lemma 1.8 (b) itself, as the interface Schoenflies.ArcCollar that Schoenflies/CrosscutAtMostTwo.lean consumes.
• Schoenflies.PolyArc.isArcBetween_carrier, Schoenflies.PolyArc.isPolygonal_carrier — the carrier of a PolyArc is a simple polygonal arc between its two extreme vertices.
• Schoenflies.polyArc_crosscut_at_most_two, Schoenflies.polyArc_crosscut_components_exhaust — Lemma "At most two sides" for a polygonal arc presented by a vertex list, with no further assumptions.
• Schoenflies.hasArcCollars, Schoenflies.crosscut_at_most_two_of_polyArc, Schoenflies.crosscut_components_exhaust_of_polyArc — the same for a set P presented by Schoenflies.IsPolyArcCarrier.
• Schoenflies.segmentPolyArc, Schoenflies.isPolyArcCarrier_segment — a straight crosscut as a PolyArc, which recovers Schoenflies.hasArcCollars_segment as a special case.

Simple polygonal arcs

A polygonal arc is presented by its vertex list v 0, …, v (n + 1); its edges are the n + 1 segments edge i = [v i, v (i + 1)] for i ≤ n, and its interior vertices — the ones that carry a corner, and hence a sector of the collar — are v 1, …, v n.

The vertex function is indexed by all of ℕ and asked to be injective outright, rather than injective on {0, …, n + 1}. Nothing past v (n + 1) is ever looked at except through A.tang i and A.len i, which are only well behaved when v i ≠ v (i + 1); asking for global injectivity buys that for free and removes an i ≤ n side condition from every lemma about the edge frame. It costs a discharger nothing: a finite vertex list is padded to an injective sequence by any tail of fresh points.

structure Schoenflies.PolyArc (n : ℕ) : Type

A simple polygonal arc, presented by its vertex list. The arc runs from vertex 0 to vertex (n + 1) along the n + 1 edges [vertex i, vertex (i + 1)], i ≤ n.

• vertex : ℕ → Plane

  The vertices, in order along the arc. Only vertex 0, …, vertex (n + 1) are on it.

• vertex_inj : Function.Injective self.vertex

  The vertices are distinct.

• edges_meet (i : ℕ) : i ≤ n → ∀ j ≤ n, 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 : ℕ) : i < n → (self.vertex i - self.vertex (i + 1)).det (self.vertex (i + 2) - self.vertex (i + 1)) ≠ 0

  No redundant vertex: the two edges at an interior vertex are not collinear. The two extreme vertices carry no condition, because the collar puts no sector there.

The turned vector of a reversed direction

theorem Schoenflies.Plane.perp_neg (u : Plane) : (-u).perp = -u.perp

Turning the reverse of a vector is the reverse of turning it.

noncomputable def Schoenflies.PolyArc.len {n : ℕ} (A : PolyArc n) (i : ℕ) : ℝ

The length of edge i.

Equations

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

noncomputable def Schoenflies.PolyArc.tang {n : ℕ} (A : PolyArc n) (i : ℕ) : Plane

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

Equations

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

noncomputable def Schoenflies.PolyArc.back {n : ℕ} (A : PolyArc n) (i : ℕ) : Plane

The incoming ray at vertex (i + 1): the direction back along edge i.

Equations

• A.back i = (A.vertex i - A.vertex (i + 1)).dir

noncomputable def Schoenflies.PolyArc.off {n : ℕ} (A : PolyArc n) (i : ℕ) (t s : ℝ) : Plane

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

Equations

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

noncomputable def Schoenflies.PolyArc.pt {n : ℕ} (A : PolyArc n) (i : ℕ) (c : ℝ) : Plane

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

Equations

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

def Schoenflies.PolyArc.edge {n : ℕ} (A : PolyArc n) (i : ℕ) : Set Plane

Edge i of the arc.

Equations

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

def Schoenflies.PolyArc.carrier {n : ℕ} (A : PolyArc n) : Set Plane

The carrier of the arc: the union of its n + 1 edges.

Equations

• A.carrier = ⋃ (i : ℕ), ⋃ (_ : i ≤ n), A.edge i

theorem Schoenflies.PolyArc.mem_carrier_iff {n : ℕ} {A : PolyArc n} {x : Plane} : x ∈ A.carrier ↔ ∃ i ≤ n, x ∈ A.edge i

theorem Schoenflies.PolyArc.edge_subset_carrier {n : ℕ} {A : PolyArc n} {i : ℕ} (hi : i ≤ n) : A.edge i ⊆ A.carrier

theorem Schoenflies.PolyArc.vertex_ne {n : ℕ} {A : PolyArc n} {i : ℕ} : A.vertex i ≠ A.vertex (i + 1)

theorem Schoenflies.PolyArc.sub_ne_zero_of_edge {n : ℕ} {A : PolyArc n} {i : ℕ} : A.vertex (i + 1) - A.vertex i ≠ 0

theorem Schoenflies.PolyArc.len_pos {n : ℕ} {A : PolyArc n} {i : ℕ} : 0 < A.len i

theorem Schoenflies.PolyArc.isDirection_tang {n : ℕ} {A : PolyArc n} {i : ℕ} : (A.tang i).IsDirection

theorem Schoenflies.PolyArc.len_smul_tang {n : ℕ} {A : PolyArc n} {i : ℕ} : A.len i • A.tang i = A.vertex (i + 1) - A.vertex i

theorem Schoenflies.PolyArc.vertex_succ_eq {n : ℕ} {A : PolyArc n} {i : ℕ} : A.vertex (i + 1) = A.vertex i + A.len i • A.tang i

theorem Schoenflies.PolyArc.back_eq {n : ℕ} {A : PolyArc n} {i : ℕ} : A.back i = -A.tang i

The incoming ray at vertex (i + 1) is the reverse of the tangent of edge i.

theorem Schoenflies.PolyArc.isDirection_back {n : ℕ} {A : PolyArc n} {i : ℕ} : (A.back i).IsDirection

theorem Schoenflies.PolyArc.perp_back {n : ℕ} {A : PolyArc n} {i : ℕ} : (A.back i).perp = -(A.tang i).perp

theorem Schoenflies.PolyArc.det_rays_ne_zero {n : ℕ} {A : PolyArc n} {i : ℕ} (hi : i < n) : (A.back i).det (A.tang (i + 1)) ≠ 0

The corner condition, read on the two unit rays at an interior vertex.

The edge frame

theorem Schoenflies.PolyArc.off_zero_zero {n : ℕ} {A : PolyArc n} {i : ℕ} : A.off i 0 0 = A.vertex i

theorem Schoenflies.PolyArc.pt_zero {n : ℕ} {A : PolyArc n} {i : ℕ} : A.pt i 0 = A.vertex i

theorem Schoenflies.PolyArc.pt_eq {n : ℕ} {A : PolyArc n} {i : ℕ} {c : ℝ} : A.pt i c = A.vertex i + c • A.tang i

theorem Schoenflies.PolyArc.pt_len {n : ℕ} {A : PolyArc n} {i : ℕ} : A.pt i (A.len i) = A.vertex (i + 1)

theorem Schoenflies.PolyArc.off_sub_vertex {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} : A.off i t s - A.vertex i = t • A.tang i + s • (A.tang i).perp

theorem Schoenflies.PolyArc.pt_sub_vertex {n : ℕ} {A : PolyArc n} {i : ℕ} {c : ℝ} : A.pt i c - A.vertex i = c • A.tang i

theorem Schoenflies.PolyArc.dist_pt_vertex {n : ℕ} {A : PolyArc n} {i : ℕ} {c : ℝ} : dist (A.pt i c) (A.vertex i) = |c|

theorem Schoenflies.PolyArc.off_sub_vertex_succ {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} : A.off i t s - A.vertex (i + 1) = (t - A.len i) • A.tang i + s • (A.tang i).perp

theorem Schoenflies.PolyArc.off_sub_vertex_succ_ray {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} : A.off i t s - A.vertex (i + 1) = (A.len i - t) • A.back i - s • (A.back i).perp

The same difference written in the frame of the incoming ray, which is the form the germ argument at vertex (i + 1) consumes.

theorem Schoenflies.PolyArc.dist_off_vertex_le {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} : dist (A.off i t s) (A.vertex i) ≤ |t| + |s|

theorem Schoenflies.PolyArc.dist_off_vertex_succ_le {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} : dist (A.off i t s) (A.vertex (i + 1)) ≤ |t - A.len i| + |s|

theorem Schoenflies.PolyArc.dist_pt_vertex_succ {n : ℕ} {A : PolyArc n} {i : ℕ} {c : ℝ} : dist (A.pt i c) (A.vertex (i + 1)) = |c - A.len i|

theorem Schoenflies.PolyArc.dist_off_pt {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} : dist (A.off i t s) (A.pt i t) = |s|

@[simp]

theorem Schoenflies.PolyArc.coordAlong_off {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} : (A.vertex i).coordAlong (A.tang i) (A.off i t s) = t

@[simp]

theorem Schoenflies.PolyArc.coordAcross_off {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} : (A.vertex i).coordAcross (A.tang i) (A.off i t s) = s

theorem Schoenflies.PolyArc.off_coord {n : ℕ} (A : PolyArc n) (i : ℕ) (x : Plane) : x = A.off i ((A.vertex i).coordAlong (A.tang i) x) ((A.vertex i).coordAcross (A.tang i) x)

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

Edges as sets

theorem Schoenflies.PolyArc.mem_edge_iff {n : ℕ} {A : PolyArc n} {i : ℕ} {x : Plane} : x ∈ A.edge i ↔ ∃ c ∈ Set.Icc 0 (A.len i), x = A.pt i c

theorem Schoenflies.PolyArc.pt_mem_edge {n : ℕ} {A : PolyArc n} {i : ℕ} {c : ℝ} (hc : c ∈ Set.Icc 0 (A.len i)) : A.pt i c ∈ A.edge i

theorem Schoenflies.PolyArc.vertex_mem_edge {n : ℕ} {A : PolyArc n} {i : ℕ} : A.vertex i ∈ A.edge i

theorem Schoenflies.PolyArc.vertex_succ_mem_edge {n : ℕ} {A : PolyArc n} {i : ℕ} : A.vertex (i + 1) ∈ A.edge i

theorem Schoenflies.PolyArc.vertex_mem_carrier {n : ℕ} {A : PolyArc n} {i : ℕ} (hi : i ≤ n) : A.vertex i ∈ A.carrier

theorem Schoenflies.PolyArc.mem_edge_sub {n : ℕ} {A : PolyArc n} {i : ℕ} {x : Plane} (hx : x ∈ A.edge i) : ∃ (c : ℝ), 0 ≤ c ∧ x - A.vertex i = c • A.tang i

A point of edge i, seen from the vertex it leaves, is a nonnegative multiple of the outgoing ray.

theorem Schoenflies.PolyArc.mem_edge_sub_succ {n : ℕ} {A : PolyArc n} {i : ℕ} {x : Plane} (hx : x ∈ A.edge i) : ∃ (c : ℝ), 0 ≤ c ∧ x - A.vertex (i + 1) = c • A.back i

A point of edge i, seen from the vertex it arrives at, is a nonnegative multiple of the incoming ray there.

theorem Schoenflies.PolyArc.vertex_add_smul_back {n : ℕ} {A : PolyArc n} {i : ℕ} {c : ℝ} : A.vertex (i + 1) + c • A.back i = A.pt i (A.len i - c)

Walking back along the incoming ray from vertex (i + 1) traverses edge i.

theorem Schoenflies.PolyArc.mem_edge_of_smul_back {n : ℕ} {A : PolyArc n} {i : ℕ} {c : ℝ} (hc0 : 0 ≤ c) (hc1 : c ≤ A.len i) : A.vertex (i + 1) + c • A.back i ∈ A.edge i

theorem Schoenflies.PolyArc.mem_edge_of_smul_tang {n : ℕ} {A : PolyArc n} {i : ℕ} {c : ℝ} (hc0 : 0 ≤ c) (hc1 : c ≤ A.len i) : A.vertex i + c • A.tang i ∈ A.edge i

theorem Schoenflies.PolyArc.isCompact_edge {n : ℕ} {A : PolyArc n} {i : ℕ} : IsCompact (A.edge i)

theorem Schoenflies.PolyArc.continuous_pt {n : ℕ} (A : PolyArc n) (i : ℕ) : Continuous (A.pt i)

What simplicity gives

theorem Schoenflies.PolyArc.vertex_notMem_edge {n : ℕ} {A : PolyArc n} {i j : ℕ} (hi : i ≤ n + 1) (hj : j ≤ n) (h1 : i ≠ j) (h2 : i ≠ j + 1) : A.vertex i ∉ A.edge j

Simplicity, first form. A vertex lies on no edge but the (at most two) edges incident to it.

def Schoenflies.PolyArc.trimmed {n : ℕ} (A : PolyArc n) (i : ℕ) (lam : ℝ) : Set Plane

The trimmed core of edge i: the points at distance at least lam from both endpoints.

Equations

• A.trimmed i lam = A.pt i '' Set.Icc lam (A.len i - lam)

theorem Schoenflies.PolyArc.pt_mem_trimmed {n : ℕ} {A : PolyArc n} {i : ℕ} {c lam : ℝ} (hc : c ∈ Set.Icc lam (A.len i - lam)) : A.pt i c ∈ A.trimmed i lam

theorem Schoenflies.PolyArc.isCompact_trimmed {n : ℕ} {A : PolyArc n} {i : ℕ} {lam : ℝ} : IsCompact (A.trimmed i lam)

theorem Schoenflies.PolyArc.trimmed_subset_edge {n : ℕ} {A : PolyArc n} {i : ℕ} {lam : ℝ} (hlam : 0 < lam) : A.trimmed i lam ⊆ A.edge i

theorem Schoenflies.PolyArc.trimmed_disjoint_edge {n : ℕ} {A : PolyArc n} {i j : ℕ} {lam : ℝ} (hlam : 0 < lam) (hi : i ≤ n) (hj : j ≤ n) (hij : j ≠ i) : Disjoint (A.trimmed i lam) (A.edge j)

Simplicity, second form. The trimmed core of an edge misses every other edge: the two common points edges_meet allows are the endpoints, and the trim removes them.

The four germs at an interior vertex

Plane.germs_split' applied at the interior vertex v (i + 1), whose incoming ray is A.back i and whose outgoing ray is A.tang (i + 1). The smallness of the offset is left as a hypothesis; the block versions supply it from the germ field of an ArcStrip.

theorem Schoenflies.PolyArc.off_sub_mem_arcL_start {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} (hi : i < n) (hs : 0 < s) (hsm : s * |inner ℝ (A.back i) (A.tang (i + 1))| < t * |(A.back i).det (A.tang (i + 1))|) : A.off (i + 1) t s - A.vertex (i + 1) ∈ (A.tang (i + 1)).arcCCW (A.back i)

theorem Schoenflies.PolyArc.off_sub_mem_arcR_start {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} (hi : i < n) (hs : s < 0) (hsm : -s * |inner ℝ (A.back i) (A.tang (i + 1))| < t * |(A.back i).det (A.tang (i + 1))|) : A.off (i + 1) t s - A.vertex (i + 1) ∈ (A.back i).arcCCW (A.tang (i + 1))

theorem Schoenflies.PolyArc.off_sub_mem_arcL_finish {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} (hi : i < n) (hs : 0 < s) (hsm : s * |inner ℝ (A.back i) (A.tang (i + 1))| < (A.len i - t) * |(A.back i).det (A.tang (i + 1))|) : A.off i t s - A.vertex (i + 1) ∈ (A.tang (i + 1)).arcCCW (A.back i)

theorem Schoenflies.PolyArc.off_sub_mem_arcR_finish {n : ℕ} {A : PolyArc n} {i : ℕ} {t s : ℝ} (hi : i < n) (hs : s < 0) (hsm : -s * |inner ℝ (A.back i) (A.tang (i + 1))| < (A.len i - t) * |(A.back i).det (A.tang (i + 1))|) : A.off i t s - A.vertex (i + 1) ∈ (A.back i).arcCCW (A.tang (i + 1))

The constants

ArcStrip is the arc analogue of Schoenflies.StripData: the blueprint's "choose the blocks so that consecutive ones overlap and nonadjacent closures are disjoint", with every constant named. Three fields have no counterpart in the closed case, and they are what makes the collar a collar of K inside D: ball_subset and tube_subset put every piece inside the prescribed open set, and sep_ends keeps K clear of the two ends of the arc, where the collar has no pieces.

sep_ends is not a restriction in the intended application: the two endpoints of a crosscut lie outside D and K lies inside, so the distance from K to either endpoint is positive and R is chosen below it.

structure Schoenflies.ArcStrip {n : ℕ} (A : PolyArc n) (D K : Set Plane) : Type

The constants of the collar of a compact piece K of the simple polygonal arc A, inside a prescribed open set D.

• 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 : ℕ) : i ≤ n → 4 * self.lam < A.len i

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

• R_le_len (i : ℕ) : i ≤ n → self.R ≤ A.len i

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

• sep_vertex (i : ℕ) : i ≤ n + 1 → ∀ j ≤ n + 1, i ≠ j → 2 * self.R ≤ dist (A.vertex i) (A.vertex j)

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

• sep_vertex_edge (i : ℕ) : i ≤ n + 1 → ∀ j ≤ n, i ≠ j → i ≠ j + 1 → ∀ y ∈ A.edge j, 2 * self.R ≤ dist (A.vertex i) y

  A vertex is 2R away from every nonincident edge.

• sep_trim_edge (i : ℕ) : i ≤ n → ∀ j ≤ n, j ≠ i → ∀ c ∈ Set.Icc self.lam (A.len i - self.lam), ∀ y ∈ A.edge j, 2 * self.rho ≤ dist (A.pt i c) y

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

• germ (i : ℕ) : i < n → self.rho * (1 + |inner ℝ (A.back i) (A.tang (i + 1))|) ≤ self.lam * |(A.back i).det (A.tang (i + 1))|

  The vertex-matching threshold, at the interior vertices only.

• ball_subset (i : ℕ) : i < n → Metric.ball (A.vertex (i + 1)) self.R ⊆ D

  The sector at an interior vertex is inside the prescribed open set.

• tube_subset (i : ℕ) : i ≤ n → ∀ c ∈ Set.Icc self.lam (A.len i - self.lam), Metric.ball (A.pt i c) self.rho ⊆ D

  The block of an edge is inside the prescribed open set: a rho-ball about a point of the trimmed core is.

• subset_carrier : K ⊆ A.carrier

  The compact piece is inside the arc…

• sep_ends (x : Plane) : x ∈ K → self.R ≤ dist x (A.vertex 0) ∧ self.R ≤ dist x (A.vertex (n + 1))

  …and clear of its two endpoints, where the collar has no pieces.

theorem Schoenflies.ArcStrip.lam_pos {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : 0 < S.lam

theorem Schoenflies.ArcStrip.R_pos {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : 0 < S.R

theorem Schoenflies.ArcStrip.rho_lt_R {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : S.rho < S.R

theorem Schoenflies.ArcStrip.lam_lt_R {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : S.lam < S.R

The four families of blocks

def Schoenflies.ArcStrip.blockL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) (i : ℕ) : Set Plane

The left block of edge i.

Equations

• S.blockL i = (A.vertex i).strip (A.tang i) S.lam (A.len i - S.lam) 0 S.rho

def Schoenflies.ArcStrip.blockR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) (i : ℕ) : Set Plane

The right block of edge i.

Equations

• S.blockR i = (A.vertex i).strip (A.tang i) S.lam (A.len i - S.lam) (-S.rho) 0

def Schoenflies.ArcStrip.tube {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) (i : ℕ) : Set Plane

The full tube of edge i: the trimmed edge thickened by rho on both sides.

Equations

• S.tube i = (A.vertex i).strip (A.tang i) S.lam (A.len i - S.lam) (-S.rho) S.rho

def Schoenflies.ArcStrip.sectorL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) (i : ℕ) : Set Plane

The left sector at the interior vertex vertex (i + 1).

Equations

• S.sectorL i = (A.vertex (i + 1)).cone ((A.tang (i + 1)).arcCCW (A.back i)) S.R

def Schoenflies.ArcStrip.sectorR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) (i : ℕ) : Set Plane

The right sector at the interior vertex vertex (i + 1).

Equations

• S.sectorR i = (A.vertex (i + 1)).cone ((A.back i).arcCCW (A.tang (i + 1))) S.R

def Schoenflies.ArcStrip.chainL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (T : ArcStrip A D K) : ℕ → Set Plane

The k-th link of the left chain: the block of edge 0 to start with, and thereafter the sector at vertex k glued to the block of edge k. Consecutive links overlap in the block of the earlier edge, which is what makes the union connected.

Equations

• T.chainL 0 = T.blockL 0
• T.chainL k.succ = T.sectorL k ∪ T.blockL (k + 1)

def Schoenflies.ArcStrip.chainR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (T : ArcStrip A D K) : ℕ → Set Plane

The k-th link of the right chain.

Equations

• T.chainR 0 = T.blockR 0
• T.chainR k.succ = T.sectorR k ∪ T.blockR (k + 1)

def Schoenflies.ArcStrip.sideL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : Set Plane

The left track of the collar.

Equations

• S.sideL = ⋃ (k : ℕ), ⋃ (_ : k ≤ n), S.chainL k

def Schoenflies.ArcStrip.sideR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : Set Plane

The right track of the collar.

Equations

• S.sideR = ⋃ (k : ℕ), ⋃ (_ : k ≤ n), S.chainR k

def Schoenflies.ArcStrip.nbhd {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : Set Plane

The collar: the union of the edge tubes and the balls about the interior vertices. Unlike the closed case it is not a neighbourhood of the whole arc — it stops short of the two endpoints — and it is manifestly open.

Equations

• S.nbhd = (⋃ (i : ℕ), ⋃ (_ : i ≤ n), S.tube i) ∪ ⋃ (i : ℕ), ⋃ (_ : i < n), Metric.ball (A.vertex (i + 1)) S.R

theorem Schoenflies.ArcStrip.mem_blockL_iff {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} : x ∈ S.blockL i ↔ S.lam < (A.vertex i).coordAlong (A.tang i) x ∧ (A.vertex i).coordAlong (A.tang i) x < A.len i - S.lam ∧ 0 < (A.vertex i).coordAcross (A.tang i) x ∧ (A.vertex i).coordAcross (A.tang i) x < S.rho

theorem Schoenflies.ArcStrip.mem_blockR_iff {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} : x ∈ S.blockR i ↔ S.lam < (A.vertex i).coordAlong (A.tang i) x ∧ (A.vertex i).coordAlong (A.tang i) x < A.len i - S.lam ∧ -S.rho < (A.vertex i).coordAcross (A.tang i) x ∧ (A.vertex i).coordAcross (A.tang i) x < 0

theorem Schoenflies.ArcStrip.mem_tube_iff {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} : x ∈ S.tube i ↔ S.lam < (A.vertex i).coordAlong (A.tang i) x ∧ (A.vertex i).coordAlong (A.tang i) x < A.len i - S.lam ∧ -S.rho < (A.vertex i).coordAcross (A.tang i) x ∧ (A.vertex i).coordAcross (A.tang i) x < S.rho

theorem Schoenflies.ArcStrip.mem_blockL_off {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {t s : ℝ} : A.off i t s ∈ S.blockL i ↔ S.lam < t ∧ t < A.len i - S.lam ∧ 0 < s ∧ s < S.rho

theorem Schoenflies.ArcStrip.mem_blockR_off {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {t s : ℝ} : A.off i t s ∈ S.blockR i ↔ S.lam < t ∧ t < A.len i - S.lam ∧ -S.rho < s ∧ s < 0

theorem Schoenflies.ArcStrip.mem_tube_off {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {t s : ℝ} : A.off i t s ∈ S.tube i ↔ S.lam < t ∧ t < A.len i - S.lam ∧ -S.rho < s ∧ s < S.rho

theorem Schoenflies.ArcStrip.isOpen_blockL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : IsOpen (S.blockL i)

theorem Schoenflies.ArcStrip.isOpen_blockR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : IsOpen (S.blockR i)

theorem Schoenflies.ArcStrip.isOpen_tube {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : IsOpen (S.tube i)

theorem Schoenflies.ArcStrip.isOpen_sectorL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : IsOpen (S.sectorL i)

theorem Schoenflies.ArcStrip.isOpen_sectorR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : IsOpen (S.sectorR i)

theorem Schoenflies.ArcStrip.convex_blockL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : Convex ℝ (S.blockL i)

theorem Schoenflies.ArcStrip.convex_blockR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : Convex ℝ (S.blockR i)

theorem Schoenflies.ArcStrip.isConnected_sectorL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : IsConnected (S.sectorL i)

theorem Schoenflies.ArcStrip.isConnected_sectorR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : IsConnected (S.sectorR i)

theorem Schoenflies.ArcStrip.blockL_subset_tube {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : S.blockL i ⊆ S.tube i

theorem Schoenflies.ArcStrip.blockR_subset_tube {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : S.blockR i ⊆ S.tube i

theorem Schoenflies.ArcStrip.sectorL_subset_ball {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : S.sectorL i ⊆ Metric.ball (A.vertex (i + 1)) S.R

theorem Schoenflies.ArcStrip.sectorR_subset_ball {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} : S.sectorR i ⊆ Metric.ball (A.vertex (i + 1)) S.R

theorem Schoenflies.ArcStrip.exists_foot {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} (h : x ∈ S.tube i) : ∃ c ∈ Set.Icc S.lam (A.len i - S.lam), dist x (A.pt i c) < S.rho

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

theorem Schoenflies.ArcStrip.pt_mem_edge_of_trim {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {c : ℝ} (hc : c ∈ Set.Icc S.lam (A.len i - S.lam)) : A.pt i c ∈ A.edge i

The germ argument at an interior vertex

theorem Schoenflies.ArcStrip.germ_ineq {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) {t s : ℝ} (ht : S.lam < t) (hs0 : 0 < s) (hs : s < S.rho) : s * |inner ℝ (A.back i) (A.tang (i + 1))| < t * |(A.back i).det (A.tang (i + 1))|

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

theorem Schoenflies.ArcStrip.blockL_sub_mem_arcL_start {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} (hi : i < n) (h : x ∈ S.blockL (i + 1)) : x - A.vertex (i + 1) ∈ (A.tang (i + 1)).arcCCW (A.back i)

A point of the left block of edge i + 1, seen from the interior vertex it leaves, is in the left arc there.

theorem Schoenflies.ArcStrip.blockL_sub_mem_arcL_finish {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} (hi : i < n) (h : x ∈ S.blockL i) : x - A.vertex (i + 1) ∈ (A.tang (i + 1)).arcCCW (A.back i)

A point of the left block of edge i, seen from the interior vertex it arrives at.

theorem Schoenflies.ArcStrip.blockR_sub_mem_arcR_start {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} (hi : i < n) (h : x ∈ S.blockR (i + 1)) : x - A.vertex (i + 1) ∈ (A.back i).arcCCW (A.tang (i + 1))

theorem Schoenflies.ArcStrip.blockR_sub_mem_arcR_finish {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} (hi : i < n) (h : x ∈ S.blockR i) : x - A.vertex (i + 1) ∈ (A.back i).arcCCW (A.tang (i + 1))

Two shapes of bounded union

Both tracks and the collar are unions over an initial segment of ℕ. These two rewrites are the only interface to that indexing.

theorem Schoenflies.mem_iUnion_le_nat {α : Type u_1} {F : ℕ → Set α} {m : ℕ} {x : α} : x ∈ ⋃ (i : ℕ), ⋃ (_ : i ≤ m), F i ↔ ∃ i ≤ m, x ∈ F i

theorem Schoenflies.mem_iUnion_lt_nat {α : Type u_1} {F : ℕ → Set α} {m : ℕ} {x : α} : x ∈ ⋃ (i : ℕ), ⋃ (_ : i < m), F i ↔ ∃ i < m, x ∈ F i

Nonadjacent blocks are disjoint

Every step is one of the separation hypotheses of ArcStrip against one of the two containments exists_foot and sectorL_subset_ball.

theorem Schoenflies.ArcStrip.tube_notMem_edge {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i j : ℕ} {x : Plane} (hi : i ≤ n) (hj : j ≤ n) (hji : j ≠ i) (h : x ∈ S.tube i) : x ∉ A.edge j

A tube misses every edge but its own.

theorem Schoenflies.ArcStrip.block_notMem_own_edge {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} (h : x ∈ S.blockL i ∪ S.blockR i) : x ∉ A.edge i

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

theorem Schoenflies.ArcStrip.block_notMem_carrier {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} (hi : i ≤ n) (h : x ∈ S.blockL i ∪ S.blockR i) : x ∉ A.carrier

theorem Schoenflies.ArcStrip.tube_notMem_ball_vertex {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i j : ℕ} {x : Plane} (hi : i ≤ n) (hj : j ≤ n + 1) (hj1 : j ≠ i) (hj2 : j ≠ i + 1) (h : x ∈ S.tube i) : x ∉ Metric.ball (A.vertex j) S.R

A tube stays out of the sectors at every vertex other than its edge's own two.

theorem Schoenflies.ArcStrip.sector_notMem_far_edge {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i j : ℕ} {x : Plane} (hi : i ≤ n + 1) (hj : j ≤ n) (h1 : i ≠ j) (h2 : i ≠ j + 1) (h : x ∈ Metric.ball (A.vertex i) S.R) : x ∉ A.edge j

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

theorem Schoenflies.ArcStrip.sectorL_notMem_carrier {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} (hi : i < n) (h : x ∈ S.sectorL i) : x ∉ A.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.ArcStrip.sectorR_notMem_carrier {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} {x : Plane} (hi : i < n) (h : x ∈ S.sectorR i) : x ∉ A.carrier

The two tracks, as sets

theorem Schoenflies.ArcStrip.blockL_subset_chainL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) (k : ℕ) : S.blockL k ⊆ S.chainL k

theorem Schoenflies.ArcStrip.blockR_subset_chainR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) (k : ℕ) : S.blockR k ⊆ S.chainR k

theorem Schoenflies.ArcStrip.mem_sideL_iff {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {x : Plane} : x ∈ S.sideL ↔ (∃ i ≤ n, x ∈ S.blockL i) ∨ ∃ i < n, x ∈ S.sectorL i

theorem Schoenflies.ArcStrip.mem_sideR_iff {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {x : Plane} : x ∈ S.sideR ↔ (∃ i ≤ n, x ∈ S.blockR i) ∨ ∃ i < n, x ∈ S.sectorR i

theorem Schoenflies.ArcStrip.blockL_subset_sideL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i ≤ n) : S.blockL i ⊆ S.sideL

theorem Schoenflies.ArcStrip.blockR_subset_sideR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i ≤ n) : S.blockR i ⊆ S.sideR

theorem Schoenflies.ArcStrip.sectorL_subset_sideL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : S.sectorL i ⊆ S.sideL

theorem Schoenflies.ArcStrip.sectorR_subset_sideR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : S.sectorR i ⊆ S.sideR

theorem Schoenflies.ArcStrip.sideL_disjoint_carrier {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : Disjoint S.sideL A.carrier

theorem Schoenflies.ArcStrip.sideR_disjoint_carrier {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : Disjoint S.sideR A.carrier

theorem Schoenflies.ArcStrip.sideL_subset_nbhd {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : S.sideL ⊆ S.nbhd

theorem Schoenflies.ArcStrip.sideR_subset_nbhd {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : S.sideR ⊆ S.nbhd

The collar minus the arc is exactly the two tracks

theorem Schoenflies.ArcStrip.ball_diff_carrier_subset {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : Metric.ball (A.vertex (i + 1)) S.R \ A.carrier ⊆ S.sectorL i ∪ S.sectorR i

A vertex ball minus the arc is covered by the two sectors at that vertex. A point of the ball off the arc points in some direction from the vertex; 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.ArcStrip.tube_diff_carrier_subset {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i ≤ n) : S.tube i \ A.carrier ⊆ S.blockL i ∪ S.blockR i

A tube minus the arc is its two blocks.

theorem Schoenflies.ArcStrip.nbhd_diff_carrier {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : S.nbhd \ A.carrier = S.sideL ∪ S.sideR

Lemma 1.8 (b), the set equality. Removing the arc from the collar leaves exactly the two labelled tracks.

theorem Schoenflies.ArcStrip.isOpen_nbhd {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : IsOpen S.nbhd

theorem Schoenflies.ArcStrip.nbhd_subset {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : S.nbhd ⊆ D

The collar is inside the prescribed open set.

Chaining a linear family

The union of the left pieces is connected because consecutive pieces overlap. Unlike the cyclic case there is no closing overlap to discard: the chain 0, 1, …, N is exactly the spanning tree of the overlap graph.

theorem Schoenflies.isConnected_iUnion_chain {α : Type u_1} [TopologicalSpace α] {F : ℕ → Set α} (N : ℕ) : (∀ k ≤ N, IsConnected (F k)) → (∀ k < N, (F k ∩ F (k + 1)).Nonempty) → IsConnected (⋃ (k : ℕ), ⋃ (_ : k ≤ N), F k)

A family of connected sets indexed by an initial segment of ℕ, in which every member meets its successor, has connected union.

theorem Schoenflies.exists_offset_bound {ε b X k : ℝ} (hε : 0 < ε) (hb : 0 < b) (hX : 0 < X) (hk : 0 < k) : ∃ (σ : ℝ), 0 < σ ∧ σ < ε ∧ σ < b ∧ σ * k < X

One positive offset below an accuracy, below a geometric bound, and small enough against a germ threshold. This is the arc's replacement for the exists_common_bound of Schoenflies/StripLocal.lean, which is private there.

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 interior vertex in question.

theorem Schoenflies.ArcStrip.lam_lt_three_halves_lam {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : S.lam < 3 * S.lam / 2

theorem Schoenflies.ArcStrip.three_halves_lam_lt {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i ≤ n) : 3 * S.lam / 2 < A.len i - S.lam

theorem Schoenflies.ArcStrip.overlap_dist_lt {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : 3 * S.lam / 2 + S.rho / 2 < S.R

theorem Schoenflies.ArcStrip.mem_blockL_overlap_start {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : A.off (i + 1) (3 * S.lam / 2) (S.rho / 2) ∈ S.blockL (i + 1)

theorem Schoenflies.ArcStrip.mem_blockR_overlap_start {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : A.off (i + 1) (3 * S.lam / 2) (-(S.rho / 2)) ∈ S.blockR (i + 1)

theorem Schoenflies.ArcStrip.mem_blockL_overlap_finish {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : A.off i (A.len i - 3 * S.lam / 2) (S.rho / 2) ∈ S.blockL i

theorem Schoenflies.ArcStrip.mem_blockR_overlap_finish {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : A.off i (A.len i - 3 * S.lam / 2) (-(S.rho / 2)) ∈ S.blockR i

theorem Schoenflies.ArcStrip.mem_overlapL_start {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : A.off (i + 1) (3 * S.lam / 2) (S.rho / 2) ∈ S.blockL (i + 1) ∩ S.sectorL i

The overlap at the departure vertex.

theorem Schoenflies.ArcStrip.mem_overlapL_finish {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : A.off i (A.len i - 3 * S.lam / 2) (S.rho / 2) ∈ S.blockL i ∩ S.sectorL i

The overlap at the arrival vertex.

theorem Schoenflies.ArcStrip.mem_overlapR_start {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : A.off (i + 1) (3 * S.lam / 2) (-(S.rho / 2)) ∈ S.blockR (i + 1) ∩ S.sectorR i

theorem Schoenflies.ArcStrip.mem_overlapR_finish {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) : A.off i (A.len i - 3 * S.lam / 2) (-(S.rho / 2)) ∈ S.blockR i ∩ S.sectorR i

theorem Schoenflies.ArcStrip.blockL_nonempty {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i ≤ n) : (S.blockL i).Nonempty

theorem Schoenflies.ArcStrip.blockR_nonempty {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i ≤ n) : (S.blockR i).Nonempty

theorem Schoenflies.ArcStrip.isConnected_blockL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i ≤ n) : IsConnected (S.blockL i)

theorem Schoenflies.ArcStrip.isConnected_blockR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i ≤ n) : IsConnected (S.blockR i)

The two tracks are connected

theorem Schoenflies.ArcStrip.isConnected_chainL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {k : ℕ} (hk : k ≤ n) : IsConnected (S.chainL k)

theorem Schoenflies.ArcStrip.isConnected_chainR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {k : ℕ} (hk : k ≤ n) : IsConnected (S.chainR k)

theorem Schoenflies.ArcStrip.chainL_meet {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {k : ℕ} (hk : k < n) : (S.chainL k ∩ S.chainL (k + 1)).Nonempty

theorem Schoenflies.ArcStrip.chainR_meet {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {k : ℕ} (hk : k < n) : (S.chainR k ∩ S.chainR (k + 1)).Nonempty

theorem Schoenflies.ArcStrip.isConnected_sideL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : IsConnected S.sideL

The left track of the collar is connected.

theorem Schoenflies.ArcStrip.isConnected_sideR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : IsConnected S.sideR

The right track of the collar is connected.

theorem Schoenflies.ArcStrip.isOpen_sideL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : IsOpen S.sideL

theorem Schoenflies.ArcStrip.isOpen_sideR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : IsOpen S.sideR

The two tracks are disjoint

Not a clause of Schoenflies.ArcCollar — the consumer does not need it — but it comes out of the same four families times four families as in the cyclic case, and a later consumer will want it.

theorem Schoenflies.ArcStrip.blockL_disjoint_blockR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i j : ℕ} {x : Plane} (hi : i ≤ n) (hj : j ≤ n) (hL : x ∈ S.blockL i) (hR : x ∈ S.blockR j) : False

theorem Schoenflies.ArcStrip.blockL_disjoint_sectorR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i j : ℕ} {x : Plane} (hi : i ≤ n) (hj : j < n) (hL : x ∈ S.blockL i) (hR : x ∈ S.sectorR j) : False

theorem Schoenflies.ArcStrip.sectorL_disjoint_blockR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i j : ℕ} {x : Plane} (hi : i < n) (hj : j ≤ n) (hL : x ∈ S.sectorL i) (hR : x ∈ S.blockR j) : False

theorem Schoenflies.ArcStrip.sectorL_disjoint_sectorR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i j : ℕ} {x : Plane} (hi : i < n) (hj : j < n) (hL : x ∈ S.sectorL i) (hR : x ∈ S.sectorR j) : False

theorem Schoenflies.ArcStrip.sideL_disjoint_sideR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : Disjoint S.sideL S.sideR

The two tracks of the collar are disjoint.

The compact piece is inside the collar

sep_ends is what makes this work: a point of K on the first edge is at least R from the first vertex, so it is never in the gap the collar leaves at that end, and symmetrically at the other end.

theorem Schoenflies.ArcStrip.subset_nbhd {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : K ⊆ S.nbhd

K is inside the collar.

Both tracks approach every point of K

theorem Schoenflies.ArcStrip.exists_near_sectorL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) {ε : ℝ} (hε : 0 < ε) : ∃ y ∈ S.sectorL i, dist y (A.vertex (i + 1)) < ε

A sector comes arbitrarily close to its vertex: shrink a point of it towards the vertex, which stays in the arc because an arc of directions is a cone.

theorem Schoenflies.ArcStrip.exists_near_sectorR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {i : ℕ} (hi : i < n) {ε : ℝ} (hε : 0 < ε) : ∃ y ∈ S.sectorR i, dist y (A.vertex (i + 1)) < ε

theorem Schoenflies.ArcStrip.exists_near_sides {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) {x : Plane} (hx : x ∈ K) {ε : ℝ} (hε : 0 < ε) : (∃ y ∈ S.sideL, dist x y < ε) ∧ ∃ y ∈ S.sideR, dist x y < ε

Both tracks come arbitrarily close to every point of K. In the middle of an edge this is the block; at an interior vertex it is exists_near_sectorL; in between it is the germ with the progress held fixed and the offset shrunk below the corner's threshold. The two cases the cyclic argument does not have — a point near an extreme vertex, where there is no sector — are excluded by sep_ends.

theorem Schoenflies.ArcStrip.subset_closure_sideL {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : K ⊆ closure S.sideL

Every point of K is in the closure of the left track.

theorem Schoenflies.ArcStrip.subset_closure_sideR {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : K ⊆ closure S.sideR

Every point of K is in the closure of the right track.

Lemma 1.8 (b)

def Schoenflies.ArcStrip.collar {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : ArcCollar D A.carrier K

The two-sided collar of the compact piece K along the arc, as the record Schoenflies.ArcCollar that Schoenflies/CrosscutAtMostTwo.lean consumes. The construction is exported, not existentially packaged: nbhd, sideL and sideR are definitions with an API of their own, and Schoenflies.ArcStrip.sideL_disjoint_sideR and Schoenflies.ArcStrip.isOpen_sideL are two clauses of Lemma 1.8 (b) that the record drops.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Schoenflies.ArcStrip.collar_nbhd {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : S.collar.nbhd = S.nbhd

@[simp]

theorem Schoenflies.ArcStrip.collar_left {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : S.collar.left = S.sideL

@[simp]

theorem Schoenflies.ArcStrip.collar_right {n : ℕ} {A : PolyArc n} {D K : Set Plane} (S : ArcStrip A D K) : S.collar.right = S.sideR

Choosing the constants

The blueprint's own recipe, in the blueprint's order, with the two clauses about the prescribed open set folded in at the step where they can be met.

1. R from the edge lengths, the pairwise vertex separations, the distance from each vertex to each nonincident edge, the openness of D at each interior vertex, and the distance from K to the two endpoints of the arc.
2. lam := R / 5, which gives 2 lam < R and, through R ≤ len i, also 4 lam < len i.
3. rho from the distance of each trimmed edge to every other edge, from the germ threshold at every interior vertex, and from the compact separation of each trimmed edge from the complement of D. Step 3 is where "the collar is inside D" is really paid for: a trimmed core is a compact subset of D, because the only points of the arc outside D are its two endpoints and the trim removes them.

theorem Schoenflies.PolyArc.pt_ne_vertex_zero {n : ℕ} {A : PolyArc n} {i : ℕ} {c lam : ℝ} (hlam : 0 < lam) (hi : i ≤ n) (hc : c ∈ Set.Icc lam (A.len i - lam)) : A.pt i c ≠ A.vertex 0

A point of a trimmed core is not the first vertex of the arc: on the first edge the trim keeps it away, and on any other edge simplicity does.

theorem Schoenflies.PolyArc.pt_ne_vertex_last {n : ℕ} {A : PolyArc n} {i : ℕ} {c lam : ℝ} (hlam : 0 < lam) (hi : i ≤ n) (hc : c ∈ Set.Icc lam (A.len i - lam)) : A.pt i c ≠ A.vertex (n + 1)

…nor the last vertex of the arc.

theorem Schoenflies.PolyArc.exists_cone_radius {n : ℕ} (A : PolyArc n) {D K : Set Plane} (hD : IsOpen D) (hKcompact : IsCompact K) (hKD : K ⊆ D) (hint : ∀ (j : ℕ), 1 ≤ j → j ≤ n → A.vertex j ∈ D) (ha : A.vertex 0 ∉ D) (hb : A.vertex (n + 1) ∉ D) : ∃ R > 0, (∀ i ≤ n, R ≤ A.len i) ∧ (∀ i ≤ n + 1, ∀ j ≤ n + 1, i ≠ j → 2 * R ≤ dist (A.vertex i) (A.vertex j)) ∧ (∀ i ≤ n + 1, ∀ j ≤ n, i ≠ j → i ≠ j + 1 → ∀ y ∈ A.edge j, 2 * R ≤ dist (A.vertex i) y) ∧ (∀ i < n, Metric.ball (A.vertex (i + 1)) R ⊆ D) ∧ ∀ x ∈ K, R ≤ dist x (A.vertex 0) ∧ R ≤ dist x (A.vertex (n + 1))

Step 1: the cone radius.

theorem Schoenflies.PolyArc.exists_half_width {n : ℕ} (A : PolyArc n) {D : Set Plane} {lam : ℝ} (hD : IsOpen D) (hlam : 0 < lam) (hcore : ∀ i ≤ n, A.trimmed i lam ⊆ D) : ∃ rho > 0, rho < lam ∧ (∀ i ≤ n, ∀ j ≤ n, j ≠ i → ∀ c ∈ Set.Icc lam (A.len i - lam), ∀ y ∈ A.edge j, 2 * rho ≤ dist (A.pt i c) y) ∧ (∀ i < n, rho * (1 + |inner ℝ (A.back i) (A.tang (i + 1))|) ≤ lam * |(A.back i).det (A.tang (i + 1))|) ∧ ∀ i ≤ n, ∀ c ∈ Set.Icc lam (A.len i - lam), Metric.ball (A.pt i c) rho ⊆ D

Step 3: the half-width.

theorem Schoenflies.exists_arcStrip {n : ℕ} (A : PolyArc n) {D K : Set Plane} (hD : IsOpen D) (ha : A.vertex 0 ∉ D) (hb : A.vertex (n + 1) ∉ D) (hPD : A.carrier \ {A.vertex 0, A.vertex (n + 1)} ⊆ D) (hKcompact : IsCompact K) (hKsub : K ⊆ D ∩ A.carrier) : Nonempty (ArcStrip A D K)

Lemma 1.8 (b), the constants. A simple polygonal arc whose two endpoints lie outside the region D and whose remaining points lie inside it carries an ArcStrip for every compact piece K of D ∩ P.

Lemma 1.8 (b), and HasArcCollars

theorem Schoenflies.PolyArc.exists_arcCollar {n : ℕ} (A : PolyArc n) {D K : Set Plane} (hD : IsOpen D) (ha : A.vertex 0 ∉ D) (hb : A.vertex (n + 1) ∉ D) (hPD : A.carrier \ {A.vertex 0, A.vertex (n + 1)} ⊆ D) (hKcompact : IsCompact K) (hKsub : K ⊆ D ∩ A.carrier) : Nonempty (ArcCollar D A.carrier K)

Two-sided polygonal strips, the arc case. Every compact piece of the arc lying inside the region has a two-sided collar there. The collar is ArcStrip.collar, a construction, not an existential: Schoenflies.exists_arcStrip produces the constants and every part of the collar is a definition with an API.

theorem Schoenflies.PolyArc.hasArcCollars {n : ℕ} (A : PolyArc n) {D : Set Plane} (hD : IsOpen D) (ha : A.vertex 0 ∉ D) (hb : A.vertex (n + 1) ∉ D) (hPD : A.carrier \ {A.vertex 0, A.vertex (n + 1)} ⊆ D) : HasArcCollars D A.carrier

HasArcCollars for a polygonal arc. This is the hypothesis of Schoenflies.crosscut_at_most_two, discharged.

Note that neither connectedness nor nontriviality of K is used: the collar exists for every compact subset of D ∩ P.

def Schoenflies.IsPolyArcCarrier (P : Set Plane) (a b : Plane) : Prop

P is a simple polygonal arc from a to b, presented by a vertex list. This is the arc analogue of what Schoenflies.exists_closedPolygon proves for a Jordan curve, and it is the one thing this module does not prove; see the note at the end of the file.

Equations

• Schoenflies.IsPolyArcCarrier P a b = ∃ (n : ℕ) (A : Schoenflies.PolyArc n), A.carrier = P ∧ A.vertex 0 = a ∧ A.vertex (n + 1) = b

theorem Schoenflies.hasArcCollars {D P : Set Plane} {a b : Plane} (hD : IsOpen D) (ha : a ∉ D) (hb : b ∉ D) (hPD : P \ {a, b} ⊆ D) (hchain : IsPolyArcCarrier P a b) : HasArcCollars D P

HasArcCollars for a set presented as the carrier of a PolyArc. The conclusion is literally the Schoenflies.HasArcCollars that Schoenflies/CrosscutAtMostTwo.lean carries as a hypothesis, and the hypotheses are those of Schoenflies.crosscut_at_most_two together with the presentation of P by a vertex list.

theorem Schoenflies.crosscut_at_most_two_of_polyArc {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) (hchain : IsPolyArcCarrier P a b) : ∃ zL ∈ D \ P, ∃ zR ∈ D \ P, ∀ x ∈ D \ P, x ∈ connectedComponentIn (D \ P) zL ∨ x ∈ connectedComponentIn (D \ P) zR

Lemma "At most two sides" for a polygonal arc presented by a vertex list.

theorem Schoenflies.crosscut_components_exhaust_of_polyArc {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) (hchain : IsPolyArcCarrier P a b) (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, for a polygonal arc presented by a vertex list.

The presentation is faithful: the carrier is a simple polygonal arc

PolyArc is a presentation, so the interface owes a check in the other direction: that the carrier of a PolyArc really is a simple polygonal arc between its two extreme vertices. Both halves are an induction along the chain of edges, and the only input is simplicity: consecutive edges meet exactly at the vertex they share, and nonconsecutive ones not at all.

With them, Lemma "At most two sides" for an arc presented by a vertex list has no hypothesis left standing — Schoenflies.polyArc_crosscut_at_most_two.

def Schoenflies.PolyArc.prefixCarrier {n : ℕ} (A : PolyArc n) (k : ℕ) : Set Plane

The union of the first k + 1 edges.

Equations

• A.prefixCarrier k = ⋃ (i : ℕ), ⋃ (_ : i ≤ k), A.edge i

theorem Schoenflies.PolyArc.mem_prefixCarrier_iff {n k : ℕ} {A : PolyArc n} {x : Plane} : x ∈ A.prefixCarrier k ↔ ∃ i ≤ k, x ∈ A.edge i

theorem Schoenflies.PolyArc.prefixCarrier_zero {n : ℕ} {A : PolyArc n} : A.prefixCarrier 0 = A.edge 0

theorem Schoenflies.PolyArc.prefixCarrier_succ {n k : ℕ} {A : PolyArc n} : A.prefixCarrier (k + 1) = A.prefixCarrier k ∪ A.edge (k + 1)

theorem Schoenflies.PolyArc.prefixCarrier_last {n : ℕ} (A : PolyArc n) : A.prefixCarrier n = A.carrier

theorem Schoenflies.PolyArc.prefixCarrier_meet {n k : ℕ} {A : PolyArc n} (hk : k + 1 ≤ n) (z : Plane) : z ∈ A.prefixCarrier k → z ∈ A.edge (k + 1) → z = A.vertex (k + 1)

Consecutive edges meet exactly at the vertex they share, and nonconsecutive ones not at all: the union of the first k + 1 edges meets edge k + 1 only at vertex (k + 1).

theorem Schoenflies.PolyArc.isArcBetween_prefixCarrier {n : ℕ} (A : PolyArc n) (k : ℕ) : k ≤ n → IsArcBetween (A.prefixCarrier k) (A.vertex 0) (A.vertex (k + 1))

The union of the first k + 1 edges is an arc from the first vertex to vertex (k + 1).

theorem Schoenflies.PolyArc.isArcBetween_carrier {n : ℕ} (A : PolyArc n) : IsArcBetween A.carrier (A.vertex 0) (A.vertex (n + 1))

The carrier of a PolyArc is an arc between its two extreme vertices.

theorem Schoenflies.PolyArc.isPolygonal_prefixCarrier {n : ℕ} (A : PolyArc n) (k : ℕ) : IsPolygonal (A.prefixCarrier k)

theorem Schoenflies.PolyArc.isPolygonal_carrier {n : ℕ} (A : PolyArc n) : IsPolygonal A.carrier

The carrier of a PolyArc is polygonal.

theorem Schoenflies.polyArc_crosscut_at_most_two {n : ℕ} (A : PolyArc n) {D : Set Plane} (hDopen : IsOpen D) (hDconn : IsPreconnected D) (ha : A.vertex 0 ∉ D) (hb : A.vertex (n + 1) ∉ D) (hPD : A.carrier \ {A.vertex 0, A.vertex (n + 1)} ⊆ D) : ∃ zL ∈ D \ A.carrier, ∃ zR ∈ D \ A.carrier, ∀ x ∈ D \ A.carrier, x ∈ connectedComponentIn (D \ A.carrier) zL ∨ x ∈ connectedComponentIn (D \ A.carrier) zR

Lemma "At most two sides" for a polygonal arc presented by a vertex list, with nothing left standing. The arc hypothesis and the polygonality hypothesis of Schoenflies.crosscut_at_most_two are supplied by the presentation itself, and the collar hypothesis by Schoenflies.PolyArc.hasArcCollars.

theorem Schoenflies.polyArc_crosscut_components_exhaust {n : ℕ} (A : PolyArc n) {D : Set Plane} {v₁ v₂ : Plane} (hDopen : IsOpen D) (hDconn : IsPreconnected D) (ha : A.vertex 0 ∉ D) (hb : A.vertex (n + 1) ∉ D) (hPD : A.carrier \ {A.vertex 0, A.vertex (n + 1)} ⊆ D) (h₁ : v₁ ∈ D \ A.carrier) (h₂ : v₂ ∈ D \ A.carrier) (hne : connectedComponentIn (D \ A.carrier) v₁ ≠ connectedComponentIn (D \ A.carrier) v₂) (x : Plane) : x ∈ D \ A.carrier → x ∈ connectedComponentIn (D \ A.carrier) v₁ ∨ x ∈ connectedComponentIn (D \ A.carrier) v₂

Lemma "At most two sides", in the form the crosscut theorem consumes, for a polygonal arc presented by a vertex list, with nothing left standing.

The presentation is not vacuous: a straight crosscut

A nondegenerate segment is a PolyArc 0: one edge, no interior vertex, so both edges_meet and corner are vacuous. The vertex function is padded past the segment by walking on in the same direction, which keeps it injective — this is the padding convention the structure's docstring describes, in its simplest instance. With it, Schoenflies.hasArcCollars_segment of Schoenflies/CrosscutAtMostTwo.lean is a special case of Schoenflies.hasArcCollars, which certifies that Schoenflies.IsPolyArcCarrier is satisfiable and that the whole apparatus above is not vacuous.

noncomputable def Schoenflies.segmentPolyArc {a b : Plane} (hab : a ≠ b) : PolyArc 0

The one-edge arc from a to b, with its vertex list padded injectively past b.

Equations

• Schoenflies.segmentPolyArc hab = { vertex := fun (k : ℕ) => a + ↑k • (b - a), vertex_inj := ⋯, edges_meet := ⋯, corner := ⋯ }

@[simp]

theorem Schoenflies.segmentPolyArc_vertex_zero {a b : Plane} (hab : a ≠ b) : (segmentPolyArc hab).vertex 0 = a

@[simp]

theorem Schoenflies.segmentPolyArc_vertex_one {a b : Plane} (hab : a ≠ b) : (segmentPolyArc hab).vertex 1 = b

theorem Schoenflies.segmentPolyArc_carrier {a b : Plane} (hab : a ≠ b) : (segmentPolyArc hab).carrier = segment ℝ a b

theorem Schoenflies.isPolyArcCarrier_segment {a b : Plane} (hab : a ≠ b) : IsPolyArcCarrier (segment ℝ a b) a b

A nondegenerate segment is presented by a vertex list.

What is still missing

Exactly one thing: Schoenflies.IsPolyArcCarrier. Everything above is proved for an arc presented by its vertex list, and Schoenflies.hasArcCollars therefore carries that presentation as a hypothesis in place of the blueprint's set-level "P is a simple polygonal arc" (IsArcBetween P a b together with IsPolygonal P).

The missing theorem is

theorem isPolyArcCarrier_of_isPolygonal {P : Set Plane} {a b : Plane}
    (hP : IsArcBetween P a b) (hpoly : IsPolygonal P) (hab : a ≠ b) : IsPolyArcCarrier P a b

the arc analogue of Schoenflies.exists_closedPolygon, which Schoenflies/Realization.lean proves for a Jordan curve. It is a normalisation statement, not geometry: it says a set that happens to be both an arc and a finite union of segments can be cut into a chain. The route is the one Schoenflies/Realization.lean takes in the closed case, and its three steps are:

1. Schoenflies.IsArcBetween.exists_poly_eq already gives a vertex list vs with poly vs = P, vs.head = a, vs.getLast = b. That list may backtrack: nothing yet says its vertices occur in order along P.
2. Order them. Each segment [vs i, vs (i+1)] is contained in P and is an arc between its ends, so by Schoenflies.IsArcBetween.eq_of_subset it is the subarc of P between the two parameters. The parameters of the vs i, sorted and deduplicated, therefore cut [0, 1] into intervals each of which is covered by one of those segments, and the subarc over each is a segment. That is the chain, with vertex_inj and edges_meet immediate from injectivity of the parametrisation.
3. Delete redundant vertices, i.e. merge two consecutive collinear edges into one. This is the blueprint's own first sentence ("Delete redundant vertices at which two consecutive edges are collinear") and is what corner needs; the closed-curve analogue is Schoenflies.PrePolygon.exists_closedPolygon_of_prePolygon.

None of the three is formalised for an arc. The remaining results require no such interface.