Realizing a polygonal Jordan curve as a ClosedPolygon

The blueprint's "simple closed polygonal curve" is set-theoretic: an IsJordanCurve that is also IsPolygonal, with no condition on vertices at all. The development works instead with Schoenflies.ClosedPolygon, a cyclic vertex list carrying a corner field — no three consecutive vertices collinear. That field is a presentation condition, strictly stronger than the blueprint's notion, and until now nothing said that a set-level polygonal Jordan curve admits such a presentation. This module proves it.

How the vertex list is found

The curve is not read off the vertex list IsPolygonal hands over: that list may retrace itself, cross itself, and repeat segments, and it carries no order along the curve. Two structures are laid over the point set instead and then matched.

• From the plane side, the overlay of Schoenflies/OverlayGraph.lean, with the graph discarded: Schoenflies.IsClean is a finite list of nondegenerate segments occupying the curve, with pairwise disjoint interiors and no end interior to any of them. Around an interior point of a piece the curve is that piece (IsClean.exists_ball_subset_seg), so the piece interiors are separated by honest open sets of the plane (Schoenflies.nearPiece) and a connected subset of the curve away from the ends lies inside a single piece.
• From the curve side, the loop's parameters at which it reaches an end of a piece. They form a finite subset of [0, 1) containing 0 — 0 because the loop's start is put on the cut list, so that the last gap is the one that closes the curve — and, listed in increasing order, they cut [0, 1) into gaps.

The two match: a gap image is connected and misses the ends, so it lies in one piece interior; and the interior is connected and covered by the closed gap images, so it lies in that one gap. Gaps and pieces therefore correspond one to one, the ends of a gap are the ends of its piece, and the ends listed in the loop's order are a cyclic vertex list whose edges are the pieces. That list satisfies vertex_inj and edges_meet but not corner, which is what Schoenflies.PrePolygon is for; corner is then arranged by deleting redundant vertices.

Blueprint

• Schoenflies.PrePolygon — a ClosedPolygon less the corner field: the blueprint's simple closed polygonal curve presented by a vertex list, redundant vertices allowed.
• Schoenflies.PrePolygon.deleteLast, Schoenflies.PrePolygon.exists_closedPolygon_of_prePolygon — the blueprint's opening move in Lemma 1.8, "delete redundant vertices at which two consecutive edges are collinear", as an operation rather than an invariant.
• Schoenflies.IsClean, Schoenflies.exists_isClean — Lemma 3.7 (polygonal overlay) with the combinatorics dropped: what the overlay says about the point set alone.
• Schoenflies.par, Schoenflies.parNext, Schoenflies.exists_mem_gap — the parameters in increasing order, and that their gaps tile [0, 1).
• Schoenflies.exists_prePolygon_of_isJordanCurve, Schoenflies.exists_closedPolygon — §1: every simple closed polygonal curve, in the blueprint's set-level sense, is the carrier of a ClosedPolygon.
• Schoenflies.IsStraightAt, Schoenflies.IsCornerAt, Schoenflies.ClosedPolygon.exists_vertex_eq_of_isCornerAt, Schoenflies.ClosedPolygon.isCornerAt_vertex — the vertex set of a realization is exactly the set of points at which the curve does not run straight. So a named point can be required to be a vertex precisely when it is a corner, and no realization has any choice about it.
• Schoenflies.ClosedPolygon.rotate, …isArcBetween_arc, …arc_inter — the two arcs of a splitting, as arcs between the two cut vertices meeting exactly there.
• Schoenflies.two_arcs_unique — two points cut a Jordan curve into two arcs in only one way.
• Schoenflies.exists_closedPolygon_corners, Schoenflies.exists_closedPolygon_split, Schoenflies.exists_closedPolygon_arcs, Schoenflies.exists_closedPolygon_arcs_ordered — the realization with named corners, with the splitting indices, and with the two arcs identified. The last is the shape Graph.IsHexRealization asks for.

The corner hypothesis is not an artefact

exists_closedPolygon_arcs requires the two cut points to be corners. ClosedPolygon.isCornerAt_vertex shows that this cannot be dropped: every vertex of every realization is a corner, so a cut point at which the curve runs straight is a vertex of no realization, and no ClosedPolygon with that carrier has an arc ending there. A consumer that needs to cut at a straight point has to change the curve — bend it there — which is a different theorem, and is exactly the freedom Graph.IsK33Config.not_isDrawing reserves for itself.

Polygons before normalization

PrePolygon is ClosedPolygon with the corner field removed. Everything the curve bridge of Schoenflies/PolygonBridge.lean proves about a ClosedPolygon — that its carrier is a Jordan curve, that it is polygonal — uses only vertex_inj and edges_meet, so it is already true here; what corner buys is the germ argument of the strip lemma, and nothing else.

structure Schoenflies.PrePolygon (m : ℕ) : Type

A simple closed polygonal curve presented by its cyclic vertex list, with redundant vertices allowed: ClosedPolygon less its corner field.

• vertex : ZMod (m + 3) → Plane

  The vertices, in cyclic order.

• vertex_inj : Function.Injective self.vertex

  The vertices are distinct.

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

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

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

The edge leaving vertex i.

Equations

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

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

The carrier: the union of the edges.

Equations

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

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

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

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

def Schoenflies.ClosedPolygon.toPre {m : ℕ} (P : ClosedPolygon m) : PrePolygon m

A ClosedPolygon read as a PrePolygon: forget the corner field.

Equations

• P.toPre = { vertex := P.vertex, vertex_inj := ⋯, edges_meet := ⋯ }

@[simp]

theorem Schoenflies.ClosedPolygon.carrier_toPre {m : ℕ} (P : ClosedPolygon m) : P.toPre.carrier = P.carrier

Small facts about the cyclic index

ZMod (m + 3) has at least three elements; 0, 1 and 2 are distinct, which is what makes a vertex, its successor and its predecessor three different vertices.

theorem Schoenflies.PrePolygon.two_ne_zero' {m : ℕ} : 2 ≠ 0

theorem Schoenflies.PrePolygon.pred_ne_succ {m : ℕ} (i : ZMod (m + 3)) : i - 1 ≠ i + 1

theorem Schoenflies.PrePolygon.val_one_eq {m : ℕ} : ZMod.val 1 = 1

theorem Schoenflies.PrePolygon.val_succ_of_lt {m : ℕ} {j : ZMod (m + 3)} (h : j.val + 1 < m + 3) : (j + 1).val = j.val + 1

The successor of a non-final index is the next one.

theorem Schoenflies.PrePolygon.val_succ_last {m : ℕ} {j : ZMod (m + 3)} (h : j.val + 1 = m + 3) : (j + 1).val = 0

The successor of the final index wraps to 0.

Rotation

Reading the same cyclic list from a different starting vertex. It is used once, to bring the vertex that is about to be deleted to the end of the list.

def Schoenflies.PrePolygon.rotate {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) : PrePolygon m

The same closed polygon, read from vertex a onwards.

Equations

• P.rotate a = { vertex := fun (j : ZMod (m + 3)) => P.vertex (a + j), vertex_inj := ⋯, edges_meet := ⋯ }

@[simp]

theorem Schoenflies.PrePolygon.rotate_vertex {m : ℕ} (P : PrePolygon m) (a j : ZMod (m + 3)) : (P.rotate a).vertex j = P.vertex (a + j)

theorem Schoenflies.PrePolygon.carrier_rotate {m : ℕ} (P : PrePolygon m) (a : ZMod (m + 3)) : (P.rotate a).carrier = P.carrier

Rotating does not move the curve: the edges are the same, listed from elsewhere.

Deleting the last vertex

The blueprint's opening move in the strip lemma. The vertex to be deleted is brought to the end of the list by rotate, so only that one case has to be treated. emb is the inclusion of the shortened index set into the old one: the same numeral, one modulus smaller.

def Schoenflies.PrePolygon.emb {m : ℕ} (j : ZMod (m + 3)) : ZMod (m + 1 + 3)

An index of the shortened list, read in the original one: the same numeral.

Equations

• Schoenflies.PrePolygon.emb j = ↑j.val

theorem Schoenflies.PrePolygon.neg_one_eq_cast {m : ℕ} : -1 = ↑(m + 3)

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

theorem Schoenflies.PrePolygon.emb_injective {m : ℕ} : Function.Injective emb

theorem Schoenflies.PrePolygon.emb_succ_of_lt {m : ℕ} {j : ZMod (m + 3)} (h : j.val + 1 < m + 3) : emb (j + 1) = emb j + 1

theorem Schoenflies.PrePolygon.emb_succ_last {m : ℕ} {j : ZMod (m + 3)} (h : j.val + 1 = m + 3) : emb (j + 1) = 0

theorem Schoenflies.PrePolygon.emb_eq_last {m : ℕ} {j : ZMod (m + 3)} (h : j.val + 1 = m + 3) : emb j = -1 - 1

theorem Schoenflies.PrePolygon.emb_ne_of_lt {m : ℕ} {j : ZMod (m + 3)} (h : j.val + 1 < m + 3) : emb j ≠ -1 ∧ emb j ≠ -1 - 1

Below the last index, emb misses both the deleted vertex and its predecessor.

theorem Schoenflies.PrePolygon.exists_emb_eq {m : ℕ} {i : ZMod (m + 1 + 3)} (h1 : i ≠ -1) (h2 : i ≠ -1 - 1) : ∃ (j : ZMod (m + 3)), j.val + 1 < m + 3 ∧ emb j = i

Every index other than the deleted vertex and its predecessor is hit by emb.

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

The vertex list with its last entry dropped.

Equations

• P.dropVertex j = P.vertex (Schoenflies.PrePolygon.emb j)

theorem Schoenflies.PrePolygon.dropVertex_injective {m : ℕ} {P : PrePolygon (m + 1)} : Function.Injective P.dropVertex

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

Away from the deleted vertex the edges are unchanged.

theorem Schoenflies.PrePolygon.dropVertex_edge_last {m : ℕ} {P : PrePolygon (m + 1)} (hcol : P.vertex (-1) ∈ openSegment ℝ (P.vertex (-1 - 1)) (P.vertex 0)) {j : ZMod (m + 3)} (h : j.val + 1 = m + 3) : segment ℝ (P.dropVertex j) (P.dropVertex (j + 1)) = P.edge (-1 - 1) ∪ P.edge (-1)

The final edge of the shortened list is the union of the two edges at the deleted vertex — which is a segment precisely because the deleted vertex is interior to it.

theorem Schoenflies.PrePolygon.vertex_last_notMem_edge {m : ℕ} {P : PrePolygon (m + 1)} {i : ZMod (m + 1 + 3)} (h1 : i ≠ -1) (h2 : i ≠ -1 - 1) : P.vertex (-1) ∉ P.edge i

The deleted vertex lies on no edge but its own two: edges_meet puts a meeting point at an end of the other edge, and the deleted vertex is an end only of the two edges at it.

theorem Schoenflies.PrePolygon.dropVertex_edges_meet {m : ℕ} {P : PrePolygon (m + 1)} (hcol : P.vertex (-1) ∈ openSegment ℝ (P.vertex (-1 - 1)) (P.vertex 0)) (j k : ZMod (m + 3)) (hjk : j ≠ k) : segment ℝ (P.dropVertex j) (P.dropVertex (j + 1)) ∩ segment ℝ (P.dropVertex k) (P.dropVertex (k + 1)) ⊆ {P.dropVertex j, P.dropVertex (j + 1)}

Simplicity survives the deletion. The only new edge is the merged one, and the point that has to be kept out of it — the deleted vertex — lies on no other edge at all.

def Schoenflies.PrePolygon.deleteLast {m : ℕ} (P : PrePolygon (m + 1)) (hcol : P.vertex (-1) ∈ openSegment ℝ (P.vertex (-1 - 1)) (P.vertex 0)) : PrePolygon m

The polygon with a redundant vertex deleted.

Equations

• P.deleteLast hcol = { vertex := P.dropVertex, vertex_inj := ⋯, edges_meet := ⋯ }

theorem Schoenflies.PrePolygon.carrier_deleteLast {m : ℕ} {P : PrePolygon (m + 1)} (hcol : P.vertex (-1) ∈ openSegment ℝ (P.vertex (-1 - 1)) (P.vertex 0)) : (P.deleteLast hcol).carrier = P.carrier

Deleting a redundant vertex does not move the curve.

Recognising a redundant vertex

The corner field is det ≠ 0 at every vertex. Where it fails the vertex is interior to the segment joining its two neighbours, never an endpoint of it. That is the geometric content of edges_meet: two edges leaving a vertex in the same direction would overlap in a nondegenerate segment, and edges_meet would then put a whole segment inside a two-point set.

theorem Schoenflies.PrePolygon.exists_mem_segment_ne {a b : Plane} (hab : a ≠ b) : ∃ p ∈ segment ℝ a b, p ≠ a ∧ p ≠ b

A nondegenerate segment is not contained in the pair of its own endpoints.

theorem Schoenflies.PrePolygon.mem_openSegment_of_det_eq_zero' {a b c : Plane} (hab : a ≠ b) (hcb : c ≠ b) (hmeet : segment ℝ a b ∩ segment ℝ b c ⊆ {a, b}) (h : (a - b).det (c - b) = 0) : b ∈ openSegment ℝ a c

Three collinear points meeting only at the shared one are in the order that makes the middle one interior. The alternative — the two segments running the same way out of b — makes them overlap in a nondegenerate segment, which the meeting hypothesis forbids.

theorem Schoenflies.PrePolygon.mem_openSegment_of_det_eq_zero {m : ℕ} {P : PrePolygon m} (i : ZMod (m + 3)) (h : (P.vertex (i - 1) - P.vertex i).det (P.vertex (i + 1) - P.vertex i) = 0) : P.vertex i ∈ openSegment ℝ (P.vertex (i - 1)) (P.vertex (i + 1))

A redundant vertex is interior to the segment joining its neighbours.

Normalization

Delete redundant vertices until none is left. Each deletion shortens the list by one, and the list can never shrink below three vertices: a triangle with a redundant vertex would have one edge inside another, which edges_meet forbids.

theorem Schoenflies.PrePolygon.not_collinear_triangle (P : PrePolygon 0) : P.vertex (-1) ∉ openSegment ℝ (P.vertex (-1 - 1)) (P.vertex 0)

A three-vertex polygon has no redundant vertex: were the last one interior to the segment joining the other two, the edge before it would lie inside the edge opposite it.

theorem Schoenflies.PrePolygon.exists_closedPolygon_of_prePolygon (m : ℕ) (P : PrePolygon m) : ∃ (m' : ℕ) (P' : ClosedPolygon m'), P'.carrier = P.carrier

Every PrePolygon normalizes to a ClosedPolygon with the same carrier. This is the blueprint's "delete redundant vertices at which two consecutive edges are collinear", run to completion; the induction is on the number of vertices, which each deletion lowers by one.

theorem Schoenflies.PrePolygon.exists_prePolygon {n : ℕ} (hn : 3 ≤ n) (w : ZMod n → Plane) (hinj : Function.Injective w) (hmeet : ∀ (i j : ZMod n), i ≠ j → segment ℝ (w i) (w (i + 1)) ∩ segment ℝ (w j) (w (j + 1)) ⊆ {w i, w (i + 1)}) : ∃ (m : ℕ) (P : PrePolygon m), P.carrier = ⋃ (i : ZMod n), segment ℝ (w i) (w (i + 1))

Assembling a cyclic vertex family into a PrePolygon. The index type is ZMod n for an n known only to be at least three, which is what PrePolygon asks for after n is written m + 3.

Clean pieces

The overlay of Schoenflies/OverlayGraph.lean, stripped of the graph. All that is wanted from it is a finite list of segments occupying the curve whose interiors are pairwise disjoint and none of whose ends is interior to any of them — the geometric content of lem:polygonal-overlay with the combinatorics left out.

structure Schoenflies.IsClean (Q : List Piece) (C : Set Plane) : Prop

A finite list of segments presenting a polygonal set as a plane graph would: occupying it, nondegenerate, with pairwise disjoint interiors, and with no end interior to any piece.

• cover_eq : cover Q = C

  The pieces occupy the set.

• nondeg (R : Piece) : R ∈ Q → R.Nondeg

  No piece is a point.

• ends (R : Piece) : R ∈ Q → ∀ S ∈ Q, ∀ (z : Plane), z = R.1 ∨ z = R.2 → z ∉ S.interior

  No end of any piece is interior to any piece.

• interiors (R : Piece) : R ∈ Q → ∀ S ∈ Q, R ≠ S → ∀ x ∈ R.interior, x ∉ S.interior

  Distinct pieces have disjoint interiors.

theorem Schoenflies.exists_isClean {C : Set Plane} (hC : IsPolygonal C) {a b : Plane} (ha : a ∈ C) (hb : b ∈ C) (hab : a ≠ b) (extra : List Plane) : ∃ (Q : List Piece), IsClean Q C ∧ ∀ p ∈ extra, p ∈ C → ∃ R ∈ Q, p = R.1 ∨ p = R.2

Every polygonal set with two points in it has a clean presentation, and any finite list of points of it may be required to be among the ends. Lengthening the cut list is free: both EndsAreCut and MeetsAreCut only ask that certain points occur in it.

theorem Schoenflies.mem_interior_or_end {R : Piece} {x : Plane} (hx : x ∈ R.seg) : x ∈ R.interior ∨ x = R.1 ∨ x = R.2

A point of a piece is interior to it or one of its ends.

def Schoenflies.nearPiece (C : Set Plane) (R : Piece) : Set Plane

The open set that isolates one piece from the others: the union of the balls in which the curve is that piece alone.

Equations

• Schoenflies.nearPiece C R = {y : Schoenflies.Plane | ∃ x ∈ R.interior, ∃ r > 0, y ∈ Metric.ball x r ∧ Metric.ball x r ∩ C ⊆ R.seg}

theorem Schoenflies.isOpen_nearPiece {C : Set Plane} {R : Piece} : IsOpen (nearPiece C R)

theorem Schoenflies.IsClean.seg_inter_subset {Q : List Piece} {C : Set Plane} {R S : Piece} (h : IsClean Q C) (hR : R ∈ Q) (hS : S ∈ Q) (hRS : R ≠ S) : R.seg ∩ S.seg ⊆ {R.1, R.2}

Two distinct clean pieces meet only at ends of the first. This is edges_meet, before the pieces have been put in cyclic order.

theorem Schoenflies.IsClean.seg_subset {Q : List Piece} {C : Set Plane} {R : Piece} (h : IsClean Q C) (hR : R ∈ Q) : R.seg ⊆ C

theorem Schoenflies.IsClean.endSet_subset {Q : List Piece} {C : Set Plane} (h : IsClean Q C) : endSet Q ⊆ C

theorem Schoenflies.IsClean.mem_cover_of_mem {Q : List Piece} {C : Set Plane} {x : Plane} (h : IsClean Q C) (hz : x ∈ C) : x ∈ cover Q

theorem Schoenflies.IsClean.diff_endSet_eq {Q : List Piece} {C : Set Plane} (h : IsClean Q C) : C \ endSet Q = ⋃ R ∈ Q, R.interior

The curve minus the ends is the disjoint union of the piece interiors.

theorem Schoenflies.IsClean.exists_ball_subset_seg {Q : List Piece} {C : Set Plane} {R : Piece} {x : Plane} (h : IsClean Q C) (hR : R ∈ Q) (hx : x ∈ R.interior) : ∃ r > 0, Metric.ball x r ∩ C ⊆ R.seg

Near an interior point the curve is that piece alone. The other pieces are finitely many closed sets missing the point: interior points are not shared, and an end of another piece cannot be interior to this one.

theorem Schoenflies.IsClean.interior_subset_nearPiece {Q : List Piece} {C : Set Plane} {R : Piece} (h : IsClean Q C) (hR : R ∈ Q) : R.interior ⊆ nearPiece C R

theorem Schoenflies.IsClean.nearPiece_inter_diff {Q : List Piece} {C : Set Plane} {R : Piece} (hR : R ∈ Q) : nearPiece C R ∩ (C \ endSet Q) ⊆ R.interior

theorem Schoenflies.IsClean.preconnected_subset_interior {Q : List Piece} {C : Set Plane} (h : IsClean Q C) {A : Set Plane} (hA : IsPreconnected A) (hA0 : A.Nonempty) (hAsub : A ⊆ C \ endSet Q) : ∃ R ∈ Q, A ⊆ R.interior

A connected piece of the curve away from the ends lies inside a single piece. The nearPiece sets are honest open sets of the plane that trace out the pieces on the curve, so IsPreconnected can be applied to them directly.

The gaps between the parameters

The loop's parameters at which it visits an end of a piece form a finite subset of [0, 1) containing 0. Listed in increasing order they cut [0, 1) into gaps, one per piece; the last gap runs to 1, where the loop closes. This section is pure order theory on ℝ.

noncomputable def Schoenflies.par {n : ℕ} (T : Finset ℝ) (hcard : T.card = n) (i : Fin n) : ℝ

The i-th parameter, in increasing order.

Equations

• Schoenflies.par T hcard i = (T.orderEmbOfFin hcard) i

noncomputable def Schoenflies.parNext {n : ℕ} (T : Finset ℝ) (hcard : T.card = n) (i : Fin n) : ℝ

The right end of the i-th gap: the next parameter, or 1 for the last gap.

Equations

• Schoenflies.parNext T hcard i = if h : ↑i + 1 < n then (T.orderEmbOfFin hcard) ⟨↑i + 1, h⟩ else 1

theorem Schoenflies.par_mem {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) (i : Fin n) : par T hcard i ∈ T

theorem Schoenflies.par_lt_par {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) {i j : Fin n} (h : i < j) : par T hcard i < par T hcard j

theorem Schoenflies.par_lt_iff {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) {i j : Fin n} : par T hcard i < par T hcard j ↔ i < j

theorem Schoenflies.par_le_par {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) {i j : Fin n} (h : i ≤ j) : par T hcard i ≤ par T hcard j

theorem Schoenflies.exists_par_eq {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) {s : ℝ} (hs : s ∈ T) : ∃ (i : Fin n), par T hcard i = s

theorem Schoenflies.par_card_pos {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) (h0 : 0 ∈ T) : 0 < n

theorem Schoenflies.par_zero {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) (hT : ∀ s ∈ T, s ∈ Set.Ico 0 1) (h0 : 0 ∈ T) : par T hcard ⟨0, ⋯⟩ = 0

The first parameter is 0: the loop is at a vertex when it starts.

theorem Schoenflies.parNext_le_one {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) (hT : ∀ s ∈ T, s ∈ Set.Ico 0 1) (i : Fin n) : parNext T hcard i ≤ 1

theorem Schoenflies.par_lt_parNext {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) (hT : ∀ s ∈ T, s ∈ Set.Ico 0 1) (i : Fin n) : par T hcard i < parNext T hcard i

theorem Schoenflies.notMem_of_mem_gap {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) {i : Fin n} {s : ℝ} (hs : s ∈ Set.Ioo (par T hcard i) (parNext T hcard i)) : s ∉ T

No parameter lies strictly inside a gap.

theorem Schoenflies.gap_disjoint {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) {i j : Fin n} (hij : i ≠ j) : Disjoint (Set.Ioo (par T hcard i) (parNext T hcard i)) (Set.Ioo (par T hcard j) (parNext T hcard j))

Distinct gaps are disjoint.

theorem Schoenflies.gap_subset_Ico {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) (hT : ∀ s ∈ T, s ∈ Set.Ico 0 1) (i : Fin n) : Set.Ioo (par T hcard i) (parNext T hcard i) ⊆ Set.Ico 0 1

theorem Schoenflies.gapClosure_subset_I {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) (hT : ∀ s ∈ T, s ∈ Set.Ico 0 1) (i : Fin n) : Set.Icc (par T hcard i) (parNext T hcard i) ⊆ unitInterval

theorem Schoenflies.exists_mem_gap {n : ℕ} {T : Finset ℝ} (hcard : T.card = n) (hT : ∀ s ∈ T, s ∈ Set.Ico 0 1) (h0 : 0 ∈ T) {s : ℝ} (hs : s ∈ Set.Ico 0 1) (hsT : s ∉ T) : ∃ (i : Fin n), s ∈ Set.Ioo (par T hcard i) (parNext T hcard i)

The gaps cover [0, 1) minus the parameters. The gap containing s starts at the largest parameter below s.

theorem Schoenflies.Icc_eq_Ioo_union_ends {a b : ℝ} (hab : a ≤ b) : Set.Icc a b = Set.Ioo a b ∪ {a, b}

A closed interval is its interior together with its two ends.

theorem Schoenflies.pair_eq_of_mem_pair {a b p q : Plane} (hab : a ≠ b) (ha : a = p ∨ a = q) (hb : b = p ∨ b = q) : a = p ∧ b = q ∨ a = q ∧ b = p

Two points of a nondegenerate pair, each known to be one of two given points, exhaust them.

theorem Schoenflies.zmod_val_succ {n : ℕ} (hn : 1 < n) (j : ZMod n) : (j + 1).val = if j.val + 1 < n then j.val + 1 else 0

The successor in ZMod n, read as a numeral below n.

From a clean presentation to a cyclic vertex list

The loop 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 loop reaches them, are the cyclic vertex list of a PrePolygon whose edges are the pieces.

theorem Schoenflies.eq_of_preconnected_finite_partition {ι : Type u_1} {X : Type u_2} [Finite ι] [TopologicalSpace X] {A D : Set X} {G Z : ι → Set X} (i : ι) (hA : IsPreconnected A) (hAD : A ⊆ D) (hGi : (G i).Nonempty) (hGA : G i ⊆ A) (hZclosed : ∀ (j : ι), IsClosed (Z j)) (hZdiff : ∀ (j : ι), Z j ∩ D = G j) (hdisjoint : ∀ (j k : ι), j ≠ k → G j ∩ G k = ∅) (hcover : ⋃ (j : ι), G j = D) : A = G i

A connected set in a finite relatively closed partition lies in the member it meets. This is shared by the arc and closed-curve realization arguments.

theorem Schoenflies.Piece.ends_of_closed_gap {R : Piece} {Z G : Set Plane} {a b : Plane} (hnd : R.1 ≠ R.2) (hclosed : IsClosed Z) (hinterior : R.interior = G) (hZ : Z = G ∪ {a, b}) : R.1 = a ∧ R.2 = b ∨ R.1 = b ∧ R.2 = a

The endpoints of a nondegenerate piece are the two boundary points of a closed gap.

theorem Schoenflies.IsClean.exists_piece_index {Q : List Piece} {C : Set Plane} (hQ : IsClean Q C) {ι : Type u_1} {pc : ι → Piece} (hpcQ : ∀ (i : ι), pc i ∈ Q) (hcover : ⋃ (i : ι), (pc i).interior = C \ endSet Q) (R : Piece) : R ∈ Q → ∃ (i : ι), pc i = R

A family whose interiors cover a clean presentation contains every piece.

theorem Schoenflies.exists_prePolygon_of_isJordanCurve {C : Set Plane} (hJ : IsJordanCurve C) (hP : IsPolygonal C) : ∃ (m : ℕ) (P : PrePolygon m), P.carrier = C

A polygonal Jordan curve is the carrier of a cyclic vertex list.

The realization theorem

theorem Schoenflies.exists_closedPolygon {C : Set Plane} (hJ : IsJordanCurve C) (hP : IsPolygonal C) : ∃ (m : ℕ) (P : ClosedPolygon m), P.carrier = C

Every simple closed polygonal curve is the carrier of a ClosedPolygon. This is the blueprint's set-level notion — IsJordanCurve together with IsPolygonal, no condition on vertices — matched with the presentation the development works with.

Corners

A realization cannot put a vertex wherever it likes: corner forbids a vertex at which the curve runs straight through. The points that must be vertices are exactly the ones at which it does not, and this is what a consumer needing a named point to be a vertex has to check.

def Schoenflies.IsStraightAt (C : Set Plane) (p : Plane) : Prop

C runs straight through p when, near p, it lies inside a segment having p in its interior.

Equations

• Schoenflies.IsStraightAt C p = ∃ (a : Schoenflies.Plane) (b : Schoenflies.Plane), p ∈ openSegment ℝ a b ∧ ∃ r > 0, Metric.ball p r ∩ C ⊆ segment ℝ a b

def Schoenflies.IsCornerAt (C : Set Plane) (p : Plane) : Prop

A corner of C: a point of it at which it does not run straight.

Equations

• Schoenflies.IsCornerAt C p = (p ∈ C ∧ ¬Schoenflies.IsStraightAt C p)

theorem Schoenflies.ClosedPolygon.exists_vertex_eq_of_isCornerAt {m : ℕ} (P : ClosedPolygon m) {p : Plane} (hp : IsCornerAt P.carrier p) : ∃ (i : ZMod (m + 3)), P.vertex i = p

Every corner is a vertex. A point interior to an edge lies on no other edge, so a small ball meets the curve only in that edge — and then the curve runs straight through it.

theorem Schoenflies.sub_eq_smul_of_mem_segment {a b x y : Plane} (hx : x ∈ segment ℝ a b) (hy : y ∈ segment ℝ a b) : ∃ (c : ℝ), x - y = c • (a - b)

Two points of a segment differ by a multiple of its direction.

theorem Schoenflies.det_eq_zero_of_mem_segment {a b x y z : Plane} (hx : x ∈ segment ℝ a b) (hy : y ∈ segment ℝ a b) (hz : z ∈ segment ℝ a b) : (x - z).det (y - z) = 0

Three points of one segment are collinear.

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

Every vertex is a corner. With ClosedPolygon.exists_vertex_eq_of_isCornerAt this says that the vertex set of a realization is exactly the corner set of the curve — so any two realizations of one curve have the same vertices, and a point can be required to be a vertex precisely when it is a corner.

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

The realization theorem, with named corners. Any finite list of corners of the curve can be required to be among the vertices — and by ClosedPolygon.exists_vertex_eq_of_isCornerAt, being a corner is exactly what a point must be for that to be possible.

theorem Schoenflies.exists_closedPolygon_split {C : Set Plane} (hJ : IsJordanCurve C) (hP : IsPolygonal C) {p q : Plane} (hp : IsCornerAt C p) (hq : IsCornerAt C q) (hpq : p ≠ q) : ∃ (m : ℕ) (P : ClosedPolygon 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 a splitting. Two distinct corners of the curve become two vertices a and a + k of the realization, which is what names the two arcs P.arc a k and P.arc (a + k) (m + 3 - k) that they cut it into.

The corner hypothesis is not an artefact: ClosedPolygon.corner forbids a vertex where the curve runs straight through, so a splitting point that is not a corner cannot be a vertex of any realization.

The two arcs of a splitting

ClosedPolygon.arc a k and ClosedPolygon.arc (a + k) (m + 3 - k) are what a consumer tracking a decomposition of the curve has to be handed. This section says what they are: two arcs between the two cut vertices, covering the curve and meeting exactly there.

def Schoenflies.ClosedPolygon.rotate {m : ℕ} (P : ClosedPolygon m) (a : ZMod (m + 3)) : ClosedPolygon m

The same closed polygon, read from vertex a onwards.

Equations

• P.rotate a = { vertex := fun (j : ZMod (m + 3)) => P.vertex (a + j), vertex_inj := ⋯, edges_meet := ⋯, corner := ⋯ }

@[simp]

theorem Schoenflies.ClosedPolygon.rotate_vertex {m : ℕ} (P : ClosedPolygon m) (a j : ZMod (m + 3)) : (P.rotate a).vertex j = P.vertex (a + j)

theorem Schoenflies.ClosedPolygon.rotate_edge {m : ℕ} (P : ClosedPolygon m) (a j : ZMod (m + 3)) : (P.rotate a).edge j = P.edge (a + j)

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

An arc is the union of the k edges leaving vertices a, a + 1, ….

theorem Schoenflies.ClosedPolygon.arc_eq_chain {m k : ℕ} (P : ClosedPolygon 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.ClosedPolygon.isArcBetween_arc {m k : ℕ} (P : ClosedPolygon 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.ClosedPolygon.natCast_shift_inj {m : ℕ} (P : ClosedPolygon m) (a : ZMod (m + 3)) {x y : ℕ} (hx : x < m + 3) (hy : y < m + 3) (he : P.vertex (a + ↑x) = P.vertex (a + ↑y)) : x = y

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

theorem Schoenflies.ClosedPolygon.arc_inter {m k : ℕ} (P : ClosedPolygon 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. A point on both lies on an edge of each; edges_meet, read in both directions, puts it at a vertex shared by the two edges, and the only shared vertices are the two ends of the split.

The two-arc decomposition is unique

Two points cut a Jordan curve into two arcs, and only into those two: the interior of any arc of the curve between them is connected and misses both, so it lies on one side of any other such splitting. Without this a realization could name two arcs and still not be known to name the two arcs a consumer started from.

theorem Schoenflies.IsArcBetween.preconnected_diff {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : IsPreconnected (A \ {p, q}) ∧ (A \ {p, q}).Nonempty

The interior of an arc — the arc less its two endpoints — is connected and nonempty. The paired form the uniqueness argument below destructures; both halves are in Schoenflies/Subarc.lean, which is where the shared set identity A ∖ {p, q} = f '' Ioo 0 1 lives.

theorem Schoenflies.two_arcs_unique {C A₁ A₂ D₁ D₂ : Set Plane} {p q : Plane} (hA : A₁ ∪ A₂ = C) (hAi : A₁ ∩ A₂ = {p, q}) (hD : D₁ ∪ D₂ = C) (hDi : D₁ ∩ D₂ = {p, q}) (hA1 : IsArcBetween A₁ p q) (hA2 : IsArcBetween A₂ p q) (hD1 : IsArcBetween D₁ p q) (hD2 : IsArcBetween D₂ p q) : A₁ = D₁ ∧ A₂ = D₂ ∨ A₁ = D₂ ∧ A₂ = D₁

The two arcs a pair of points cuts a curve into are determined.

theorem Schoenflies.exists_closedPolygon_arcs {C A₁ A₂ : Set Plane} (hJ : IsJordanCurve C) (hP : IsPolygonal C) {p q : Plane} (hp : IsCornerAt C p) (hq : IsCornerAt C q) (hpq : p ≠ q) (hA1 : IsArcBetween A₁ p q) (hA2 : IsArcBetween A₂ p q) (hunion : A₁ ∪ A₂ = C) (hinter : A₁ ∩ A₂ = {p, q}) : ∃ (m : ℕ) (P : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ), P.carrier = C ∧ 1 ≤ k ∧ k ≤ m + 2 ∧ P.vertex a = p ∧ P.vertex (a + ↑k) = q ∧ (P.arc a k = A₁ ∧ P.arc (a + ↑k) (m + 3 - k) = A₂ ∨ P.arc a k = A₂ ∧ P.arc (a + ↑k) (m + 3 - k) = A₁)

The realization theorem, tracking a splitting. A polygonal Jordan curve decomposed into two arcs meeting at two of its corners is the carrier of a ClosedPolygon whose two arcs at the corresponding vertices are those two arcs.

This is the form the plane-graph layer wants — compare Graph.IsHexRealization. The corner hypothesis on the two cut points is not an artefact of the proof: ClosedPolygon.isCornerAt_vertex says every vertex of a realization is a corner, so a cut point that is not one cannot be a vertex of any realization at all.

theorem Schoenflies.exists_closedPolygon_arcs_ordered {C A₁ A₂ : Set Plane} (hJ : IsJordanCurve C) (hP : IsPolygonal C) {p q : Plane} (hp : IsCornerAt C p) (hq : IsCornerAt C q) (hpq : p ≠ q) (hA1 : IsArcBetween A₁ p q) (hA2 : IsArcBetween A₂ p q) (hunion : A₁ ∪ A₂ = C) (hinter : A₁ ∩ A₂ = {p, q}) : ∃ (m : ℕ) (P : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ), P.carrier = C ∧ 1 ≤ k ∧ k ≤ m + 2 ∧ P.arc a k = A₁ ∧ P.arc (a + ↑k) (m + 3 - k) = A₂ ∧ (P.vertex a = p ∧ P.vertex (a + ↑k) = q ∨ P.vertex a = q ∧ P.vertex (a + ↑k) = p)

The realization theorem, with the two arcs in the order they were given. The same as Schoenflies.exists_closedPolygon_arcs with the disjunction moved off the arcs and onto the two cut vertices: reading the polygon from the other cut point exchanges the two arcs, so exactly one of the two starting vertices makes P.arc a k the first arc. This is the shape Graph.IsHexRealization asks for.