The arcs of a PrePolygon, and inserting a vertex

Schoenflies.PrePolygon is Schoenflies.ClosedPolygon without the corner field, so its vertices may sit anywhere on the curve. This module carries §1 and §2 of the blueprint for such a presentation: the edge list of an arc, the arc as a set, the two arcs of a splitting, and the construction that makes the whole thing worth having — a prescribed point of the curve can be made a vertex.

Everything below is the Schoenflies.ClosedPolygon development of Schoenflies/PolygonBridge.lean, Schoenflies/ParitySplitting.lean, Schoenflies/PolygonalCrosscut.lean and Schoenflies/Realization.lean with the structure changed; every proof uses only vertex_inj and edges_meet, and corner is never mentioned.

Why this module exists

Schoenflies/Graph/K33Land.lean and Schoenflies/FaceCyclesLand.lean each needed the same apparatus and each transcribed it, the second under an FC suffix. The two copies were not alpha-equivalent — insertLast in particular carried an extra hypothesis in one of them — so the import checker never complained, and there were two of everything. This module is the single copy; both consumers import it.

The one signature that genuinely differed is Schoenflies.PrePolygon.insertLast. The FaceCyclesLand copy took, besides hz : z ∈ openSegment ℝ (P.vertex (-1)) (P.vertex 0), a hypothesis ∀ j, P.vertex j ≠ z saying the new point is not already a vertex. That is not an extra assumption but a consequence: Schoenflies.PrePolygon.vertex_ne_of_mem_openSegment derives it from hz. The general form — the one with hz alone — is what survives here.

Inserting a vertex, and why it is the crux

Schoenflies.PrePolygon.deleteLast removes a vertex at which the curve runs straight (the blueprint's Lemma 1.8); Schoenflies.PrePolygon.insertLast is the inverse move, and it is the reason PrePolygon is the right structure for a consumer that needs named points to be vertices. The vertex is inserted at the end of the list, interior to the last edge, so that the only edge that changes is the last one, which splits in two; Schoenflies.PrePolygon.rotate brings any edge there. Simplicity survives because the far end of the split edge lies on neither half.

Blueprint

• Schoenflies.PrePolygon.vertex_natCast_ne, …edge_meet_earlier — the elementary simplicity facts, §1.
• Schoenflies.PrePolygon.chain, …mem_chain_iff, …isArcBetween_chain — the union of the first k edges, and that it is an arc.
• Schoenflies.PrePolygon.arcPieces, …arcPieces_add, …arcPieces_full, …isChainFrom_arcPieces, …arcPieces_split_perm, …sameEdges_arcPieces_split, …parity_splitting — the edge list of an arc, and Lemma 2.7 for it.
• Schoenflies.PrePolygon.arc, …arc_union, …arc_inter, …isArcBetween_arc, …arc_not_subset_endpoints, …isCompact_arc — the two arcs of a splitting, §2.
• Schoenflies.PrePolygon.parity_ne_iff_mem_farRegion — thm:polygonal-jordan read as a separation criterion.
• Schoenflies.PrePolygon.arcList, …poly_arcList, …isPolygonal_arc — an arc as a polyline, which is how it is glued to a crosscut.
• Schoenflies.segment_halves_inter, Schoenflies.right_notMem_left_half, Schoenflies.left_notMem_right_half — §1: cutting a segment at an interior point, in order. General-purpose; they belong beside Schoenflies.segment_split in Schoenflies/SegmentCut.lean.
• Schoenflies.PrePolygon.insertLast, …carrier_insertLast, Schoenflies.PrePolygon.exists_prePolygon_insert, …exists_prePolygon_vertices — the inverse of the blueprint's "delete redundant vertices" (Lemma 1.8): insert one, anywhere on the curve.
• Schoenflies.exists_prePolygon_points, …exists_prePolygon_split — §1, the realization theorem with the cut points anywhere on the curve. Compare Schoenflies.exists_closedPolygon_split, which requires them to be corners.

Indices, edges and the elementary simplicity facts

Verbatim the Schoenflies.ClosedPolygon facts of Schoenflies/PolygonBridge.lean whose proofs use only vertex_inj and edges_meet.

theorem Schoenflies.PrePolygon.vertex_natCast_ne {m : ℕ} {P : PrePolygon m} {j l : ℕ} (hj : j < m + 3) (hl : l < m + 3) (hjl : j ≠ l) : P.vertex ↑j ≠ P.vertex ↑l

Distinct indices below the modulus name distinct vertices.

theorem Schoenflies.PrePolygon.edge_meet_earlier {m : ℕ} {P : PrePolygon m} {j l : ℕ} (hjl : j < l) (hl : l + 1 < m + 3) {z : Plane} (hzj : z ∈ P.edge ↑j) (hzl : z ∈ P.edge ↑l) : z = P.vertex ↑l

An edge meets an earlier edge only at its own initial vertex.

The chain of the first k edges, and that it is an arc

def Schoenflies.PrePolygon.chain {m : ℕ} (P : PrePolygon m) : ℕ → Set Plane

The union of the edges leaving vertices 0, 1, …, k.

Equations

• P.chain 0 = P.edge 0
• P.chain k.succ = P.chain k ∪ P.edge ↑(k + 1)

theorem Schoenflies.PrePolygon.mem_chain_iff {m : ℕ} {P : PrePolygon m} {k : ℕ} {z : Plane} : z ∈ P.chain k ↔ ∃ j ≤ k, z ∈ P.edge ↑j

theorem Schoenflies.PrePolygon.isArcBetween_chain {m : ℕ} (P : PrePolygon m) (k : ℕ) : k + 1 < m + 3 → IsArcBetween (P.chain k) (P.vertex 0) (P.vertex ↑(k + 1))

The partial chains are arcs. One edge at a time, glued at the vertex they share.

The edge list of an arc

Schoenflies.ClosedPolygon.arcPieces with the structure changed; every proof below uses only vertex_inj and edges_meet, so it is the old proof verbatim.

def Schoenflies.PrePolygon.arcPieces {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ) : List Piece

The edge list of the arc of P that leaves vertex a and runs forward through k edges.

Equations

• P.arcPieces a k = List.map (fun (t : ℕ) => (P.vertex (a + ↑t), P.vertex (a + ↑t + 1))) (List.range k)

@[simp]

theorem Schoenflies.PrePolygon.arcPieces_toPre {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) : C.toPre.arcPieces a k = C.arcPieces a k

Forgetting the corner field does not change the edge list of an arc.

@[simp]

theorem Schoenflies.PrePolygon.arcPieces_zero {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) : P.arcPieces a 0 = []

theorem Schoenflies.PrePolygon.arcPieces_add {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k l : ℕ) : P.arcPieces a (k + l) = P.arcPieces a k ++ P.arcPieces (a + ↑k) l

Running through k + l edges is running through k and then through l.

theorem Schoenflies.PrePolygon.arcPieces_full {m : ℕ} (P : PrePolygon m) : P.arcPieces 0 (m + 3) = P.pieces

Running through all m + 3 edges from vertex 0 is the whole edge list.

theorem Schoenflies.PrePolygon.mem_pieces_of_mem_arcPieces {m : ℕ} {P : PrePolygon m} {a : ZMod (m + 3)} {k : ℕ} {Q : Piece} (hQ : Q ∈ P.arcPieces a k) : Q ∈ P.pieces

Every edge of an arc is an edge of the polygon.

theorem Schoenflies.PrePolygon.arcPieces_nondeg {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ) (Q : Piece) : Q ∈ P.arcPieces a k → Q.Nondeg

theorem Schoenflies.PrePolygon.arcPieces_hgt_ne {m : ℕ} {P : PrePolygon m} {a : ZMod (m + 3)} {k : ℕ} {u : Plane} (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) (Q : Piece) : Q ∈ P.arcPieces a k → hgt u Q.1 ≠ hgt u Q.2

theorem Schoenflies.PrePolygon.isChainFrom_arcPieces {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ) : IsChainFrom (P.arcPieces a k) (P.vertex a) (P.vertex (a + ↑k))

An arc is a chain from its first vertex to its last.

theorem Schoenflies.PrePolygon.arcPieces_full_perm {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) : (P.arcPieces a (m + 3)).Perm P.pieces

The two arcs from a vertex use every edge exactly once.

theorem Schoenflies.PrePolygon.arcPieces_split_perm {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk : k ≤ m + 3) : (P.arcPieces a k ++ P.arcPieces (a + ↑k) (m + 3 - k)).Perm P.pieces

The split. For k ≤ m + 3 the two arcs at a and a + k between them use every edge of P exactly once.

theorem Schoenflies.PrePolygon.sameEdges_arcPieces_split {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk : k ≤ m + 3) : SameEdges P.pieces (P.arcPieces a k ++ P.arcPieces (a + ↑k) (m + 3 - k))

theorem Schoenflies.PrePolygon.cover_arcPieces_union {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk : k ≤ m + 3) : cover (P.arcPieces a k) ∪ cover (P.arcPieces (a + ↑k) (m + 3 - k)) = P.carrier

The two arcs between them carry the polygon.

theorem Schoenflies.PrePolygon.cover_arcPieces_subset {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ) : cover (P.arcPieces a k) ⊆ P.carrier

theorem Schoenflies.PrePolygon.arcPieces_append_hgt_ne {m : ℕ} {P : PrePolygon m} {a : ZMod (m + 3)} {k : ℕ} {u : Plane} {K : List Piece} (hC : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) (hK : ∀ Q ∈ K, hgt u Q.1 ≠ hgt u Q.2) (Q : Piece) : Q ∈ P.arcPieces a k ++ K → hgt u Q.1 ≠ hgt u Q.2

theorem Schoenflies.PrePolygon.carrier_eq_of_sameEdges {m : ℕ} {P : PrePolygon m} {a : ZMod (m + 3)} {k m' : ℕ} {J : PrePolygon m'} {K : List Piece} (h : SameEdges J.pieces (P.arcPieces a k ++ K)) : J.carrier = cover (P.arcPieces a k) ∪ cover K

A curve of the split occupies its arc together with the crosscut.

theorem Schoenflies.PrePolygon.notMem_carrier_of_sameEdges {m : ℕ} {P : PrePolygon m} {a : ZMod (m + 3)} {k m' : ℕ} {J : PrePolygon m'} {K : List Piece} (h : SameEdges J.pieces (P.arcPieces a k ++ K)) {x : Plane} (hxC : x ∉ P.carrier) (hxK : x ∉ cover K) : x ∉ J.carrier

A point off P and off the crosscut is off J.

theorem Schoenflies.PrePolygon.parity_splitting {m k : ℕ} (P : PrePolygon m) (u : Plane) (a : ZMod (m + 3)) (hk : k ≤ m + 3) {L₁ L₂ K : List Piece} (h₁ : SameEdges L₁ (P.arcPieces a k ++ K)) (h₂ : SameEdges L₂ (P.arcPieces (a + ↑k) (m + 3 - k) ++ K)) (q : Plane) : parity u L₁ q + parity u L₂ q = parity u P.pieces q

Parity splitting (Lemma 2.7) for a polygon presented with redundant vertices.

The arcs as sets

def Schoenflies.PrePolygon.arc {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ) : Set Plane

The arc of P that leaves vertex a and runs forward through k edges, as a set.

Equations

• P.arc a k = Schoenflies.cover (P.arcPieces a k)

@[simp]

theorem Schoenflies.PrePolygon.arc_toPre {m : ℕ} (C : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) : C.toPre.arc a k = C.arc a k

theorem Schoenflies.PrePolygon.arc_subset_carrier {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ) : P.arc a k ⊆ P.carrier

theorem Schoenflies.PrePolygon.arc_union {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk : k ≤ m + 3) : P.arc a k ∪ P.arc (a + ↑k) (m + 3 - k) = P.carrier

theorem Schoenflies.PrePolygon.isCompact_arc {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ) : IsCompact (P.arc a k)

An arc is compact: it is a finite union of segments.

theorem Schoenflies.PrePolygon.mem_arc_iff {m : ℕ} {P : PrePolygon m} {a : ZMod (m + 3)} {k : ℕ} {z : Plane} : z ∈ P.arc a k ↔ ∃ t < k, z ∈ P.edge (a + ↑t)

theorem Schoenflies.PrePolygon.vertex_mem_arc {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk : 1 ≤ k) : P.vertex a ∈ P.arc a k

The first vertex of a nonempty arc lies on it.

theorem Schoenflies.PrePolygon.vertex_add_mem_arc {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk : 1 ≤ k) : P.vertex (a + ↑k) ∈ P.arc a k

The last vertex of a nonempty arc lies on it.

theorem Schoenflies.PrePolygon.endpoints_subset_arc {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk : 1 ≤ k) : {P.vertex a, P.vertex (a + ↑k)} ⊆ P.arc a k

The two cut vertices lie on both arcs.

theorem Schoenflies.PrePolygon.endpoints_subset_arc' {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk2 : k ≤ m + 2) : {P.vertex a, P.vertex (a + ↑k)} ⊆ P.arc (a + ↑k) (m + 3 - k)

theorem Schoenflies.PrePolygon.natCast_shift_inj {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) {x z : ℕ} (hx : x < m + 3) (hz : z < m + 3) (he : P.vertex (a + ↑x) = P.vertex (a + ↑z)) : x = z

Distinct index numerals below the modulus name distinct vertices, after any shift.

theorem Schoenflies.PrePolygon.arc_eq_chain {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk : 1 ≤ k) : P.arc a k = (P.rotate a).chain (k - 1)

An arc of P is a chain of the polygon read from its first vertex.

theorem Schoenflies.PrePolygon.isArcBetween_arc {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk1 : 1 ≤ k) (hk2 : k ≤ m + 2) : IsArcBetween (P.arc a k) (P.vertex a) (P.vertex (a + ↑k))

An arc of a splitting is an arc between the two cut vertices.

theorem Schoenflies.PrePolygon.arc_inter {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk1 : 1 ≤ k) (hk2 : k ≤ m + 2) : P.arc a k ∩ P.arc (a + ↑k) (m + 3 - k) = {P.vertex a, P.vertex (a + ↑k)}

The two arcs of a splitting meet exactly at the two cut vertices.

theorem Schoenflies.PrePolygon.arc_not_subset_endpoints {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk1 : 1 ≤ k) (hk2 : k ≤ m + 2) : ¬P.arc a k ⊆ {P.vertex a, P.vertex (a + ↑k)}

An interior point of the first edge of an arc: a point of the arc that is neither cut vertex, which is what says the arc is more than its two ends.

theorem Schoenflies.PrePolygon.parity_ne_iff_mem_farRegion {m : ℕ} (P : PrePolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x y : Plane} (hx : x ∉ P.carrier) (hy : y ∉ P.carrier) : parity u P.pieces x ≠ parity u P.pieces y ↔ x ∈ farRegion P.carrier y

The crossing count separates points exactly as the polygon does (Theorem 2.3, read as a criterion), for a polygon presented with redundant vertices.

An arc as a polyline

arc a k is the carrier of the vertex list v a, v (a+1), …, v (a+k); that is how it is seen to be polygonal, and how it is glued to a crosscut.

def Schoenflies.PrePolygon.arcList {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) : ℕ → List Plane

The vertex list of an arc.

Equations

• P.arcList a 0 = [P.vertex a]
• P.arcList a k.succ = P.vertex a :: P.arcList (a + 1) k

theorem Schoenflies.PrePolygon.arcList_ne_nil {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ) : P.arcList a k ≠ []

theorem Schoenflies.PrePolygon.head_arcList {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ) : (P.arcList a k).head ⋯ = P.vertex a

theorem Schoenflies.PrePolygon.getLast_arcList {m : ℕ} (k : ℕ) (P : PrePolygon m) (a : ZMod (m + 3)) : (P.arcList a k).getLast ⋯ = P.vertex (a + ↑k)

theorem Schoenflies.PrePolygon.arcPieces_succ {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ) : P.arcPieces a (k + 1) = (P.vertex a, P.vertex (a + 1)) :: P.arcPieces (a + 1) k

theorem Schoenflies.PrePolygon.poly_arcList {m : ℕ} (k : ℕ) (P : PrePolygon m) (a : ZMod (m + 3)) : poly (P.arcList a (k + 1)) = P.arc a (k + 1)

theorem Schoenflies.PrePolygon.poly_arcList_of_pos {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk : 1 ≤ k) : poly (P.arcList a k) = P.arc a k

theorem Schoenflies.PrePolygon.isPolygonal_arc {m k : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) (hk : 1 ≤ k) : IsPolygonal (P.arc a k)

Cutting a segment at an interior point, in order

The two halves of a cut segment meet only at the cut, and neither reaches the far end of the other. Both are read off Schoenflies/SegmentOrder.lean: along a nondegenerate segment the distance from one end is a coordinate.

theorem Schoenflies.segment_halves_inter {u v w : Plane} (huv : u ≠ v) (hw : w ∈ openSegment ℝ u v) : segment ℝ u w ∩ segment ℝ w v ⊆ {w}

The two halves of a cut segment meet only at the cut point.

theorem Schoenflies.right_notMem_left_half {u v w : Plane} (huv : u ≠ v) (hw : w ∈ openSegment ℝ u v) : v ∉ segment ℝ u w

The far end of a cut segment is not on the near half.

theorem Schoenflies.left_notMem_right_half {u v w : Plane} (huv : u ≠ v) (hw : w ∈ openSegment ℝ u v) : u ∉ segment ℝ w v

The near end of a cut segment is not on the far half.

Inserting a vertex

Schoenflies.PrePolygon.deleteLast removes a redundant vertex; this is the inverse operation, and it is what makes PrePolygon the right presentation for a consumer that must cut the curve at prescribed points. The vertex is inserted at the end of the list, interior to the last edge; Schoenflies.PrePolygon.rotate brings any edge there.

theorem Schoenflies.PrePolygon.val_neg_one {m : ℕ} : (-1).val = m + 2

The index -1 of a cyclic list of length m + 3, as a numeral.

theorem Schoenflies.PrePolygon.edge_neg_one {m : ℕ} (P : PrePolygon m) : P.edge (-1) = segment ℝ (P.vertex (-1)) (P.vertex 0)

The last edge, with its second endpoint written as vertex 0.

theorem Schoenflies.PrePolygon.vertex_ne_of_mem_openSegment {m : ℕ} {P : PrePolygon m} {i : ZMod (m + 3)} {w : Plane} (hw : w ∈ openSegment ℝ (P.vertex i) (P.vertex (i + 1))) (j : ZMod (m + 3)) : P.vertex j ≠ w

A point interior to an edge is a vertex of no index.

def Schoenflies.PrePolygon.insVertex {m : ℕ} (P : PrePolygon m) (z : Plane) (j : ZMod (m + 1 + 3)) : Plane

The vertex family with z appended at the end: the old numerals name the old vertices, and the one new index names z.

Equations

• P.insVertex z j = if j.val < m + 3 then P.vertex ↑j.val else z

theorem Schoenflies.PrePolygon.insVertex_emb {m : ℕ} (P : PrePolygon m) (z : Plane) (j : ZMod (m + 3)) : P.insVertex z (emb j) = P.vertex j

theorem Schoenflies.PrePolygon.val_neg_one' {m : ℕ} : (-1).val = m + 3

theorem Schoenflies.PrePolygon.insVertex_neg_one {m : ℕ} (P : PrePolygon m) (z : Plane) : P.insVertex z (-1) = z

theorem Schoenflies.PrePolygon.insEdge_of_lt {m : ℕ} {P : PrePolygon m} {z : Plane} {j : ZMod (m + 3)} (h : j.val + 1 < m + 3) : segment ℝ (P.insVertex z (emb j)) (P.insVertex z (emb j + 1)) = P.edge j

Away from the inserted vertex the edges are unchanged.

theorem Schoenflies.PrePolygon.insEdge_pen {m : ℕ} (P : PrePolygon m) (z : Plane) : segment ℝ (P.insVertex z (-1 - 1)) (P.insVertex z (-1 - 1 + 1)) = segment ℝ (P.vertex (-1)) z

The penultimate edge of the lengthened list: the near half of the cut edge.

theorem Schoenflies.PrePolygon.insEdge_last {m : ℕ} (P : PrePolygon m) (z : Plane) : segment ℝ (P.insVertex z (-1)) (P.insVertex z (-1 + 1)) = segment ℝ z (P.vertex 0)

The last edge of the lengthened list: the far half of the cut edge.

theorem Schoenflies.PrePolygon.vertex_neg_one_ne_zero {m : ℕ} (P : PrePolygon m) : P.vertex (-1) ≠ P.vertex 0

theorem Schoenflies.PrePolygon.insEdge_union {m : ℕ} {P : PrePolygon m} {z : Plane} (hz : z ∈ openSegment ℝ (P.vertex (-1)) (P.vertex 0)) : segment ℝ (P.vertex (-1)) z ∪ segment ℝ z (P.vertex 0) = P.edge (-1)

The two new edges cover the edge they replace.

theorem Schoenflies.PrePolygon.insEdge_pen_subset {m : ℕ} {P : PrePolygon m} {z : Plane} (hz : z ∈ openSegment ℝ (P.vertex (-1)) (P.vertex 0)) : segment ℝ (P.vertex (-1)) z ⊆ P.edge (-1)

theorem Schoenflies.PrePolygon.insEdge_last_subset {m : ℕ} {P : PrePolygon m} {z : Plane} (hz : z ∈ openSegment ℝ (P.vertex (-1)) (P.vertex 0)) : segment ℝ z (P.vertex 0) ⊆ P.edge (-1)

def Schoenflies.PrePolygon.insertLast {m : ℕ} {z : Plane} (P : PrePolygon m) (hz : z ∈ openSegment ℝ (P.vertex (-1)) (P.vertex 0)) : PrePolygon (m + 1)

The polygon with one extra vertex, interior to its last edge — equivalently, with the last edge split in two at a prescribed interior point.

Equations

• P.insertLast hz = { vertex := P.insVertex z, vertex_inj := ⋯, edges_meet := ⋯ }

@[simp]

theorem Schoenflies.PrePolygon.insertLast_vertex {m : ℕ} {P : PrePolygon m} {z : Plane} (hz : z ∈ openSegment ℝ (P.vertex (-1)) (P.vertex 0)) : (P.insertLast hz).vertex = P.insVertex z

theorem Schoenflies.PrePolygon.carrier_insertLast {m : ℕ} {P : PrePolygon m} {z : Plane} (hz : z ∈ openSegment ℝ (P.vertex (-1)) (P.vertex 0)) : (P.insertLast hz).carrier = P.carrier

Inserting a vertex does not move the curve.

theorem Schoenflies.PrePolygon.insertLast_mem_vertex {m : ℕ} {P : PrePolygon m} {z : Plane} (hz : z ∈ openSegment ℝ (P.vertex (-1)) (P.vertex 0)) : ∃ (j : ZMod (m + 1 + 3)), (P.insertLast hz).vertex j = z

The inserted vertex is a vertex.

theorem Schoenflies.PrePolygon.insertLast_old_vertex {m : ℕ} {P : PrePolygon m} {z : Plane} (hz : z ∈ openSegment ℝ (P.vertex (-1)) (P.vertex 0)) (i : ZMod (m + 3)) : ∃ (j : ZMod (m + 1 + 3)), (P.insertLast hz).vertex j = P.vertex i

The old vertices are still vertices.

theorem Schoenflies.PrePolygon.exists_prePolygon_insert {m : ℕ} (P : PrePolygon m) {z : Plane} (hz : z ∈ P.carrier) : ∃ (m' : ℕ) (P' : PrePolygon m'), P'.carrier = P.carrier ∧ (∃ (j : ZMod (m' + 3)), P'.vertex j = z) ∧ ∀ (i : ZMod (m + 3)), ∃ (j : ZMod (m' + 3)), P'.vertex j = P.vertex i

A named point of the curve becomes a vertex, and the old vertices stay vertices. Either the point already is a vertex, or it is interior to exactly one edge, and then that edge is brought to the end of the list by Schoenflies.PrePolygon.rotate and cut by Schoenflies.PrePolygon.insertLast.

theorem Schoenflies.PrePolygon.exists_prePolygon_vertices (S : List Plane) {m : ℕ} (P : PrePolygon m) : (∀ z ∈ S, z ∈ P.carrier) → ∃ (m' : ℕ) (P' : PrePolygon m'), P'.carrier = P.carrier ∧ (∀ z ∈ S, ∃ (j : ZMod (m' + 3)), P'.vertex j = z) ∧ ∀ (i : ZMod (m + 3)), ∃ (j : ZMod (m' + 3)), P'.vertex j = P.vertex i

Every point of a finite list on the curve can be made a vertex at once.

theorem Schoenflies.PrePolygon.arc_one {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) : P.arc a 1 = P.edge a

A one-edge arc is that edge.

theorem Schoenflies.PrePolygon.vertex_mem_edge_elim {m : ℕ} {P : PrePolygon m} {c i : ZMod (m + 3)} (hc : P.vertex c ∈ P.edge i) : P.vertex c ∈ {P.vertex i, P.vertex (i + 1)}

A vertex on an edge is one of that edge's own two ends.

The realization theorem, with the cut points anywhere on the curve

Schoenflies.exists_closedPolygon_split requires the two cut points to be corners, and by Schoenflies.ClosedPolygon.isCornerAt_vertex that requirement cannot be dropped while the realization is a ClosedPolygon. For a PrePolygon there is no such obstruction: a point of the curve is either already a vertex or interior to an edge, and an edge may be cut.

theorem Schoenflies.exists_prePolygon_points {C : Set Plane} (hJ : IsJordanCurve C) (hP : IsPolygonal C) (S : List Plane) (hS : ∀ p ∈ S, p ∈ C) : ∃ (m : ℕ) (P : PrePolygon m), P.carrier = C ∧ ∀ p ∈ S, ∃ (i : ZMod (m + 3)), P.vertex i = p

The realization theorem for PrePolygon, with named points. Any finite list of points of the curve — corners or not — can be required to be among the vertices.

theorem Schoenflies.exists_prePolygon_split {C : Set Plane} (hJ : IsJordanCurve C) (hP : IsPolygonal C) {p q : Plane} (hp : p ∈ C) (hq : q ∈ C) (hpq : p ≠ q) : ∃ (m : ℕ) (P : PrePolygon m) (a : ZMod (m + 3)) (k : ℕ), P.carrier = C ∧ P.vertex a = p ∧ P.vertex (a + ↑k) = q ∧ 1 ≤ k ∧ k ≤ m + 2

The realization theorem tracking two named points, for a presentation that may carry redundant vertices. Unlike Schoenflies.exists_closedPolygon_split this asks nothing of the two points but that they lie on the curve: a PrePolygon has no corner field to obstruct a vertex where the curve runs straight.