Realizing a simple polygonal arc as a PolyArc

Schoenflies/ArcCollars.lean proves blueprint Lemma 1.8 (b) — the two-sided collar of an arc, hence Schoenflies.HasArcCollars — for an arc presented by its vertex list, a Schoenflies.PolyArc, and carries the presentation itself as the hypothesis Schoenflies.IsPolyArcCarrier. Nothing on main could supply that hypothesis for anything but a straight segment, so lem:crosscut-at-most-two and thm:general-crosscut were not in fact unblocked. This module closes the gap: a set that is both an arc between two points and polygonal is the carrier of a PolyArc.

This is the arc analogue of Schoenflies.exists_closedPolygon, and the route is the one Schoenflies/Realization.lean takes in the closed case, on a linear index instead of a cyclic one. The closed-case machinery is reused verbatim wherever it does not mention the loop.

The three steps

1. Cut the point set into pieces. Schoenflies.exists_isClean gives a finite list Q of nondegenerate segments occupying P, with pairwise disjoint interiors and no end interior to any of them; the two endpoints a, b of the arc are put on the cut list, so both are ends of pieces.

2. Order the pieces along the arc. The parametrisation f reaches an end of a piece at finitely many parameters; listed in increasing order they cut [0, 1] into gaps. A gap image is connected and misses the ends, so it lies in one piece interior; the interior is connected and covered by the closed gap images, so it lies in that one gap. Gaps and pieces correspond one to one and the ends, in the order f reaches them, are a linear vertex list.

   The only change from the closed case is bookkeeping at the far end. There the loop returns to f 0, so the parameters live in [0, 1) and the last gap wraps; here f 1 = b is a genuine extra vertex. Taking the parameter set to be {t ∈ [0, 1) | f t is an end of a piece} — exactly the set Schoenflies/Realization.lean uses — makes Schoenflies.parNext of the last index equal 1 by definition, which is precisely the missing right end. So Schoenflies.par, Schoenflies.parNext and Schoenflies.exists_mem_gap are used unchanged, and n parameters give n edges and n + 1 vertices.

3. Delete redundant vertices. Schoenflies.PreArc is a PolyArc less its corner field, and Schoenflies.PreArc.deleteVertex removes one vertex at which the two edges are collinear. Each deletion shortens the list by one, so the induction terminates; unlike the cyclic case it can never get stuck, because a one-edge arc satisfies corner vacuously.

Why the arc is not closed into a curve first

The tempting shortcut is to join b back to a by one extra polygonal path far from the arc, apply Schoenflies.exists_closedPolygon_arcs to the resulting Jordan curve, and read the arc off the cyclic list. It is circular. The return path has to meet P only at a and b, so it has to leave a in a direction along which the arc does not run; knowing that there is such a direction — that P is locally one segment at a — is a consequence of the realization, not an input to it. A straight segment from b to a will not do either: an arc can perfectly well cross the chord joining its endpoints. And avoiding P in the large needs ℝ² ∖ P connected, which is thm:arc-complement, stated there with an explicit hypothesis. Route (A) below needs none of this.

Padding the vertex list

PolyArc.vertex is a function on all of ℕ asked to be globally injective — the convention its docstring records, which supplies A.tang i and A.len i directly. A realization produces n + 1 vertices and nothing beyond, so the list has to be padded. Schoenflies.exists_injective_extend does it once and for all, by walking off along the first coordinate past every value the finite list takes.

Blueprint

There is no blueprint label for this statement: like the closed-curve realization theorem of Schoenflies/Realization.lean it is the bridge the blueprint takes for granted when it says "let P be a simple polygonal arc with vertices v_0, …, v_{n+1}". Its consumers are lem:polygonal-collar (b) and, through it, lem:crosscut-at-most-two and thm:general-crosscut.

• Schoenflies.exists_injective_extend — a finite injective vertex list extends to an injective sequence.
• Schoenflies.PreArc — a PolyArc less the corner field: a simple polygonal arc presented by a vertex list, redundant vertices allowed. The arc analogue of Schoenflies.PrePolygon.
• Schoenflies.skipIdx, Schoenflies.PreArc.deleteVertex, Schoenflies.PreArc.carrier_deleteVertex — the blueprint's "delete redundant vertices at which two consecutive edges are collinear", as an operation. The arc analogue of Schoenflies.PrePolygon.deleteLast, and simpler: with a linear index no rotation is needed, so the vertex to be deleted stays where it is.
• Schoenflies.PreArc.exists_polyArc — the deletion run to completion. The arc analogue of Schoenflies.PrePolygon.exists_closedPolygon_of_prePolygon.
• Schoenflies.exists_preArc_of_isArcBetween — steps 1 and 2: a set-level simple polygonal arc is the carrier of a vertex list. The arc analogue of Schoenflies.exists_prePolygon_of_isJordanCurve.
• Schoenflies.isPolyArcCarrier_of_isPolygonal — the realization theorem for arcs, and the discharge of Schoenflies.IsPolyArcCarrier.
• Schoenflies.hasArcCollars_of_isPolygonal — blueprint Lemma 1.8 (b) for a set-level simple polygonal arc, with nothing left standing.
• Schoenflies.IsCrosscut.hasArcCollars, Schoenflies.crosscut_at_most_two_of_isPolygonal — the same at the call site of thm:general-crosscut.

Padding a finite vertex list to an injective sequence

PolyArc asks for a globally injective vertex : ℕ → Plane; a realization only produces n + 2 points. The padding walks off along the first coordinate, past every value the finite part takes, which keeps the extension injective and disjoint from the finite part.

theorem Schoenflies.exists_injective_extend {N : ℕ} (v : ℕ → Plane) (hv : ∀ i < N, ∀ j < N, v i = v j → i = j) : ∃ (w : ℕ → Plane), Function.Injective w ∧ ∀ k < N, w k = v k

A vertex list injective on an initial segment extends to an injective sequence. This is the padding convention Schoenflies.PolyArc's docstring describes, supplied once.

The index map of a deletion

On a linear index there is nothing to rotate: a vertex is deleted where it stands, and skipIdx i is the inclusion of the shortened index set into the old one — the identity up to i, a shift by one beyond it. It is the arc analogue of Schoenflies.PrePolygon.emb, and much simpler, because that one has to wrap.

def Schoenflies.skipIdx (i k : ℕ) : ℕ

The index map that skips over vertex i + 1.

Equations

• Schoenflies.skipIdx i k = if k ≤ i then k else k + 1

theorem Schoenflies.skipIdx_of_le {i k : ℕ} (h : k ≤ i) : skipIdx i k = k

theorem Schoenflies.skipIdx_of_lt {i k : ℕ} (h : i < k) : skipIdx i k = k + 1

theorem Schoenflies.skipIdx_injective (i : ℕ) : Function.Injective (skipIdx i)

theorem Schoenflies.skipIdx_succ {i k : ℕ} (h : k ≠ i) : skipIdx i (k + 1) = skipIdx i k + 1

theorem Schoenflies.skipIdx_ne_left {i k : ℕ} (h : k ≠ i) : skipIdx i k ≠ i

theorem Schoenflies.skipIdx_ne_right (i k : ℕ) : skipIdx i k ≠ i + 1

Arcs before normalization

PreArc is PolyArc with the corner field removed, exactly as Schoenflies.PrePolygon is Schoenflies.ClosedPolygon with it removed. Realization produces one of these; normalization turns it into a PolyArc.

structure Schoenflies.PreArc (n : ℕ) : Type

A simple polygonal arc presented by its vertex list, with redundant vertices allowed: Schoenflies.PolyArc less its corner field.

• 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.

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

Edge i of the arc.

Equations

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

def Schoenflies.PreArc.carrier {n : ℕ} (A : PreArc 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.PreArc.mem_carrier_iff {n : ℕ} {A : PreArc n} {x : Plane} : x ∈ A.carrier ↔ ∃ i ≤ n, x ∈ A.edge i

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

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

Deleting a redundant vertex

The blueprint's opening move in the strip lemma, "delete redundant vertices at which two consecutive edges are collinear", as an operation rather than an invariant.

theorem Schoenflies.PreArc.edge_union_of_det_eq_zero {n i : ℕ} (A : PreArc n) (hi : i < n) (hdet : (A.vertex i - A.vertex (i + 1)).det (A.vertex (i + 1 + 1) - A.vertex (i + 1)) = 0) : segment ℝ (A.vertex i) (A.vertex (i + 1 + 1)) = A.edge i ∪ A.edge (i + 1)

A redundant vertex is interior to the segment joining its neighbours, so the two edges at it merge into a single one. This is Schoenflies.PrePolygon.mem_openSegment_of_det_eq_zero' read on a linear index.

theorem Schoenflies.PreArc.vertex_notMem_edge {n i k : ℕ} (A : PreArc n) (hi : i < n) (hk : k ≤ n) (hk1 : k ≠ i) (hk2 : k ≠ i + 1) : A.vertex (i + 1) ∉ A.edge k

The middle vertex of a merge lies on no other edge: it is an end of edge i, and an edge meeting edge i there would have it as one of its own ends.

theorem Schoenflies.PreArc.skip_edges_meet {n i : ℕ} (A : PreArc (n + 1)) (hi : i < n + 1) (hdet : (A.vertex i - A.vertex (i + 1)).det (A.vertex (i + 1 + 1) - A.vertex (i + 1)) = 0) (j : ℕ) : j ≤ n → ∀ k ≤ n, j ≠ k → segment ℝ (A.vertex (skipIdx i j)) (A.vertex (skipIdx i (j + 1))) ∩ segment ℝ (A.vertex (skipIdx i k)) (A.vertex (skipIdx i (k + 1))) ⊆ {A.vertex (skipIdx i j), A.vertex (skipIdx i (j + 1))}

The shortened vertex list is still simple. The merged edge is the union of the two it replaces, and the only point that could escape the two-point bound — the deleted vertex — lies on no other edge.

def Schoenflies.PreArc.deleteVertex {n i : ℕ} (A : PreArc (n + 1)) (hi : i < n + 1) (hdet : (A.vertex i - A.vertex (i + 1)).det (A.vertex (i + 1 + 1) - A.vertex (i + 1)) = 0) : PreArc n

The vertex list with a redundant vertex deleted.

Equations

• A.deleteVertex hi hdet = { vertex := fun (k : ℕ) => A.vertex (Schoenflies.skipIdx i k), vertex_inj := ⋯, edges_meet := ⋯ }

@[simp]

theorem Schoenflies.PreArc.deleteVertex_vertex {n i : ℕ} (A : PreArc (n + 1)) (hi : i < n + 1) (hdet : (A.vertex i - A.vertex (i + 1)).det (A.vertex (i + 1 + 1) - A.vertex (i + 1)) = 0) (k : ℕ) : (A.deleteVertex hi hdet).vertex k = A.vertex (skipIdx i k)

theorem Schoenflies.PreArc.deleteVertex_vertex_zero {n i : ℕ} (A : PreArc (n + 1)) (hi : i < n + 1) (hdet : (A.vertex i - A.vertex (i + 1)).det (A.vertex (i + 1 + 1) - A.vertex (i + 1)) = 0) : (A.deleteVertex hi hdet).vertex 0 = A.vertex 0

theorem Schoenflies.PreArc.deleteVertex_vertex_last {n i : ℕ} (A : PreArc (n + 1)) (hi : i < n + 1) (hdet : (A.vertex i - A.vertex (i + 1)).det (A.vertex (i + 1 + 1) - A.vertex (i + 1)) = 0) : (A.deleteVertex hi hdet).vertex (n + 1) = A.vertex (n + 1 + 1)

theorem Schoenflies.PreArc.carrier_deleteVertex {n i : ℕ} (A : PreArc (n + 1)) (hi : i < n + 1) (hdet : (A.vertex i - A.vertex (i + 1)).det (A.vertex (i + 1 + 1) - A.vertex (i + 1)) = 0) : (A.deleteVertex hi hdet).carrier = A.carrier

Deleting a redundant vertex does not move the arc.

theorem Schoenflies.PreArc.exists_polyArc (n : ℕ) (A : PreArc n) : ∃ (m : ℕ) (B : PolyArc m), B.carrier = A.carrier ∧ B.vertex 0 = A.vertex 0 ∧ B.vertex (m + 1) = A.vertex (n + 1)

Every PreArc normalizes to a PolyArc with the same carrier and the same two extreme vertices. This is the blueprint's "delete redundant vertices at which two consecutive edges are collinear", run to completion. Unlike the closed case the induction can never get stuck: a one-edge arc satisfies corner vacuously.

From a clean presentation to a linear vertex list

The arc reaches an end of a piece at finitely many parameters. Between two consecutive ones it runs through one whole piece interior — the gap image is connected and misses the ends, so it lies in one interior; and the interior, being connected and covered by the closed gap images, lies in that one gap. So the ends, listed in the order the arc reaches them, are the vertex list of a PreArc whose edges are the pieces.

The parameter set is taken inside [0, 1), exactly as in the closed case, so that Schoenflies.parNext of the last index is 1 by definition. That is not a trick: f 1 = b is the last vertex, and this is what puts it there. Both a and b are forced onto the cut list, which is what makes 0 a parameter and b an end of a piece.

theorem Schoenflies.exists_preArc_of_isArcBetween {P : Set Plane} {a b : Plane} (hP : IsArcBetween P a b) (hpoly : IsPolygonal P) : ∃ (n : ℕ) (A : PreArc n), A.carrier = P ∧ A.vertex 0 = a ∧ A.vertex (n + 1) = b

A simple polygonal arc is the carrier of a vertex list. The arc analogue of Schoenflies.exists_prePolygon_of_isJordanCurve.

The realization theorem for arcs

Realization followed by normalization. This is the statement Schoenflies/ArcCollars.lean names at the end of its file as the one thing it does not prove.

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

Every simple polygonal arc is the carrier of a PolyArc. The arc analogue of Schoenflies.exists_closedPolygon, and the discharge of Schoenflies.IsPolyArcCarrier.

No a ≠ b hypothesis is needed: an arc between two points has them distinct, because its parametrisation is injective on [0, 1].

theorem Schoenflies.hasArcCollars_of_isPolygonal {D P : Set Plane} {a b : Plane} (hD : IsOpen D) (ha : a ∉ D) (hb : b ∉ D) (hPD : P \ {a, b} ⊆ D) (hP : IsArcBetween P a b) (hpoly : IsPolygonal P) : HasArcCollars D P

Blueprint Lemma 1.8 (b) for a set-level simple polygonal arc, with nothing left standing. This is Schoenflies.hasArcCollars with its presentation hypothesis discharged.

theorem Schoenflies.crosscut_at_most_two_of_isPolygonal {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) : ∃ 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 set-level simple polygonal arc (lem:crosscut-at-most-two), with nothing left standing.

theorem Schoenflies.crosscut_components_exhaust_of_isPolygonal {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) (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, with nothing left standing.

The collar hypothesis at the call site of thm:general-crosscut

Schoenflies.IsCrosscut carries exactly what the discharge needs: P is an arc from p to q, P is polygonal, and P ∖ {p, q} lies in inside C, whose openness comes from the curve being closed. So hcollars is never again a hypothesis of the crosscut theorem — only thm:jordan is.

theorem Schoenflies.IsCrosscut.hasArcCollars {C P : Set Plane} {p q : Plane} (h : IsCrosscut C P p q) : HasArcCollars (inside C) P

The collar hypothesis of thm:general-crosscut, discharged.

theorem Schoenflies.general_crosscut' {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : inside C \ P = inside (A₁ ∪ P) ∪ inside (A₂ ∪ P) ∧ Disjoint (inside (A₁ ∪ P)) (inside (A₂ ∪ P)) ∧ (inside (A₁ ∪ P)).Nonempty ∧ (inside (A₂ ∪ P)).Nonempty ∧ inside (A₁ ∪ P) ≠ inside (A₂ ∪ P) ∧ (∀ z ∈ inside (A₁ ∪ P), connectedComponentIn (inside C \ P) z = inside (A₁ ∪ P)) ∧ (∀ z ∈ inside (A₂ ∪ P), connectedComponentIn (inside C \ P) z = inside (A₂ ∪ P)) ∧ (∀ z ∈ inside C \ P, connectedComponentIn (inside C \ P) z = inside (A₁ ∪ P) ∨ connectedComponentIn (inside C \ P) z = inside (A₂ ∪ P)) ∧ closure (inside (A₁ ∪ P)) ∩ C = A₁ ∧ closure (inside (A₂ ∪ P)) ∩ C = A₂

Theorem "Crosscut theorem", first sentence (thm:general-crosscut), with the collar hypothesis discharged: only thm:jordan is left.

theorem Schoenflies.general_crosscut_three_regions' {C P A₁ A₂ : Set Plane} {p q : Plane} (hjordan : ∀ (S : Set Plane), IsJordanCurve S → IsSeparating S) (h : IsCrosscut C P p q) (hcut : IsCutPair C p q A₁ A₂) : (C ∪ P)ᶜ = outside C ∪ inside (A₁ ∪ P) ∪ inside (A₂ ∪ P) ∧ (∀ z ∈ outside C, connectedComponentIn (C ∪ P)ᶜ z = outside C) ∧ (∀ z ∈ inside (A₁ ∪ P), connectedComponentIn (C ∪ P)ᶜ z = inside (A₁ ∪ P)) ∧ (∀ z ∈ inside (A₂ ∪ P), connectedComponentIn (C ∪ P)ᶜ z = inside (A₂ ∪ P)) ∧ (∀ z ∈ (C ∪ P)ᶜ, connectedComponentIn (C ∪ P)ᶜ z = outside C ∨ connectedComponentIn (C ∪ P)ᶜ z = inside (A₁ ∪ P) ∨ connectedComponentIn (C ∪ P)ᶜ z = inside (A₂ ∪ P)) ∧ Disjoint (outside C) (inside (A₁ ∪ P)) ∧ Disjoint (outside C) (inside (A₂ ∪ P)) ∧ Disjoint (inside (A₁ ∪ P)) (inside (A₂ ∪ P)) ∧ outside C ≠ inside (A₁ ∪ P) ∧ outside C ≠ inside (A₂ ∪ P) ∧ inside (A₁ ∪ P) ≠ inside (A₂ ∪ P) ∧ frontier (outside C) = C ∧ frontier (inside (A₁ ∪ P)) = A₁ ∪ P ∧ frontier (inside (A₂ ∪ P)) = A₂ ∪ P

Theorem "Crosscut theorem", second sentence (thm:general-crosscut), with the collar hypothesis discharged.