The subdivided boundary of a square is a cycle

Schoenflies.SquaresTwoConnected, the last hypothesis between this library and thm:jordan, discharged.

What has to be built

Schoenflies.squareGraph pieces points c r is the part of a polygonal overlay lying on the boundary of the axis-parallel square of ℓ^∞-radius r about c, when the four sides of that square are among the overlay's source segments. It is the subdivided boundary of the square, so it is a cycle, and Graph.IsLongCycle.isTwoConnected finishes. What is missing on main is the cyclic order of the cut points: the graph is presented as a set of edges, with nothing saying which edge follows which.

The route

One real-valued coordinate does the whole of it. Schoenflies.sqCoord c r is the perimeter coordinate: the distance travelled from the north-east corner going counterclockwise round the boundary, a number in [0, 8r). It is affine on each side, and it is the ordering tool of Schoenflies/SegmentOrder.lean — distance from the side's first corner — with an offset.

• Graph.IsIncWalk is a walk along which a chosen real function strictly increases. Such a walk is automatically a path (Graph.IsIncWalk.isPath): the freshness clause of Graph.IsPath says the vertex a step departs from is not visited later, and a vertex visited later has a strictly larger value. This is the only place where "the cut points are in order" is turned into a combinatorial statement, and it replaces every argument about distinctness of vertices.
• Schoenflies.exists_incWalk_of_chain is the one-dimensional heart: a finite family of nondegenerate segments inside one ambient segment [a, b], with pairwise disjoint interiors, with every end of every one of them interior to none of them, and covering [a, b], is a chain from a to b — an IsIncWalk for the coordinate dist a · whose edge list is exactly the family. The induction is on the number of segments, and the step is Schoenflies.exists_next_piece: the piece leaving the current point is the one covering a point just beyond it, "just" being measured by the least end-coordinate strictly ahead.
• The four sides are chained separately and concatenated. The concatenation is a closed walk at the north-east corner, so its last edge is split off (Graph.IsIncWalk.split_last) and becomes the distinguished edge of Graph.IsCycleThrough.

Blueprint

• Schoenflies.squaresTwoConnected — the hypothesis Schoenflies.SquaresTwoConnected of thm:arc-complement, discharged. In the blueprint this is the unstated step of "it follows inductively from lem:union-two-connected that Γ_i is 2-connected": the induction starts from one subdivided square boundary, and that it is a cycle is taken for granted there.
• Schoenflies.exists_isLongCycle_squareGraph — the cycle itself, with the clause that makes it usable: the cycle graph is squareGraph, not merely a subgraph of it. A consumer wanting the boundary cycle of a square as an object, rather than 2-connectedness, takes it from here.
• Schoenflies.exists_incWalk_insideEdges — the subdivision of one source segment of a polygonal overlay, as a path. Schoenflies/SquareMeshConnected.lean names exactly this as the theorem missing from main that blocks prop:anchored-square-mesh from being carried over to Schoenflies.squareMesh. Its own ground is Schoenflies.exists_incWalk_of_chain, which knows nothing about overlays either.
• Graph.IsIncWalk — no blueprint statement; it is the device that makes lem:polygonal-overlay's cut points into an ordered cycle.

Part 1: a walk along which a real function increases

inductive Graph.IsIncWalk {α : Type u_1} {β : Type u_2} (G : Graph α β) (f : α → ℝ) : α → List β → α → Prop

A walk along which f strictly increases. The point of the definition is Graph.IsIncWalk.isPath: a walk that cannot come back is a path, and no argument about the distinctness of the vertices has to be made anywhere else.

• nil {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → ℝ} {x : α} (hx : x ∈ G.vertexSet) : G.IsIncWalk f x [] x

  The empty walk, at a vertex of the graph.

• cons {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → ℝ} {u w v : α} {e : β} {W : List β} (hl : G.IsLink e u w) (hf : f u < f w) (hW : G.IsIncWalk f w W v) : G.IsIncWalk f u (e :: W) v

  A step to a vertex of strictly larger value, followed by an increasing walk.

theorem Graph.IsIncWalk.isWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → ℝ} {u v : α} {W : List β} (h : G.IsIncWalk f u W v) : G.IsWalk u W v

theorem Graph.IsIncWalk.source_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → ℝ} {u v : α} {W : List β} (h : G.IsIncWalk f u W v) (x : α) : x ∈ G.walkVertices u W → f u ≤ f x

Every vertex the walk visits has value at least the source's.

theorem Graph.IsIncWalk.le_target {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → ℝ} {u v : α} {W : List β} (h : G.IsIncWalk f u W v) (x : α) : x ∈ G.walkVertices u W → f x ≤ f v

And at most the target's.

theorem Graph.IsIncWalk.isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → ℝ} {u v : α} {W : List β} (h : G.IsIncWalk f u W v) : G.IsPath u W v

An increasing walk is a path. The vertex a step departs from has a strictly smaller value than everything the rest of the walk visits, so it is not among them.

theorem Graph.IsIncWalk.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} {f : α → ℝ} {u v : α} {W : List β} (hHG : H ≤ G) (h : H.IsIncWalk f u W v) : G.IsIncWalk f u W v

theorem Graph.IsIncWalk.append {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → ℝ} {u v w : α} {W₁ W₂ : List β} (h₁ : G.IsIncWalk f u W₁ w) (h₂ : G.IsIncWalk f w W₂ v) : G.IsIncWalk f u (W₁ ++ W₂) v

theorem Graph.IsIncWalk.congr_walkVertices {α : Type u_1} {β : Type u_2} {G : Graph α β} {f g : α → ℝ} {u v : α} {W : List β} (h : G.IsIncWalk f u W v) (hfg : ∀ x ∈ G.walkVertices u W, f x = g x) : G.IsIncWalk g u W v

The function may be replaced by any function agreeing with it on the visited vertices.

theorem Graph.IsIncWalk.const_add {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → ℝ} {u v : α} {W : List β} (h : G.IsIncWalk f u W v) (t : ℝ) : G.IsIncWalk (fun (x : α) => t + f x) u W v

Shifting the function by a constant changes nothing. Each side of the square carries the distance from its own first corner; the shifts are what glue the four into one coordinate.

theorem Graph.IsIncWalk.eq_nil_of_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → ℝ} {u : α} {W : List β} (h : G.IsIncWalk f u W u) : W = []

An increasing walk from a vertex to itself is empty.

theorem Graph.IsIncWalk.split_last {α : Type u_1} {β : Type u_2} {G : Graph α β} {f : α → ℝ} {u v : α} {W : List β} (h : G.IsIncWalk f u W v) (huv : u ≠ v) : ∃ (W' : List β) (e : β) (z : α), W = W' ++ [e] ∧ G.IsIncWalk f u W' z ∧ G.IsLink e z v ∧ f z < f v

Splitting off the last step. An increasing walk between distinct vertices has a last edge, and what precedes it is again an increasing walk. This is what turns the closed walk round the square into the edge plus detour that Graph.IsCycleThrough asks for.

Part 2: a tiling of one segment is a chain

Everything here happens along a single ambient segment [a, b], and the coordinate is the one Schoenflies/SegmentOrder.lean supplies: the distance from a. A finite family of nondegenerate pieces inside [a, b], with disjoint interiors, no end interior to any of them, and covering the part of [a, b] ahead of the current point, is walked through from the current point to b, one piece at a time, in increasing distance from a.

theorem Schoenflies.exists_mem_segment_dist {a b : Plane} (hab : a ≠ b) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ dist a b) : ∃ x ∈ segment ℝ a b, dist a x = t

Every point of [a, b] at a prescribed distance from a — the surjectivity of the coordinate, which is what lets an argument name a point "just ahead" of another.

theorem Schoenflies.dist_le_dist_of_mem_segment {a b x : Plane} (hab : a ≠ b) (hx : x ∈ segment ℝ a b) : dist a x ≤ dist a b

The coordinate of a point of [a, b] lies between 0 and the segment's length.

theorem Schoenflies.exists_ordered_ends (a : Plane) (Q : Piece) : ∃ (u : Plane) (v : Plane), (u = Q.1 ∧ v = Q.2 ∨ u = Q.2 ∧ v = Q.1) ∧ dist a u ≤ dist a v ∧ segment ℝ u v = Q.seg ∧ openSegment ℝ u v = Q.interior

The two ends of a piece, near end first. Every one-dimensional citation wants them in that order, and which of the two names is the near one is none of the caller's business.

theorem Schoenflies.ne_of_ordered_ends {Q : Piece} {u v : Plane} (hQ : Q.Nondeg) (h : u = Q.1 ∧ v = Q.2 ∨ u = Q.2 ∧ v = Q.1) : u ≠ v

Ordered ends of a nondegenerate piece are distinct.

structure Schoenflies.IsPieceChain (a b p : Plane) (E : Set Piece) : Prop

The data of the induction: a finite family of pieces filling the part of [a, b] from p onwards.

cover asks nothing at b itself, and cannot: at p = b the family is empty, and an empty family covers nothing.

• finite : E.Finite

  Finitely many pieces.

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

  None of them a point.

• sub (Q : Piece) : Q ∈ E → Q.seg ⊆ segment ℝ p b

  All of them ahead of p.

• memP : p ∈ segment ℝ a b

  The current point is on the ambient segment.

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

  Every end of every piece is interior to none of them — the cut-point condition.

• disj (Q : Piece) : Q ∈ E → ∀ Q' ∈ E, Q ≠ Q' → ∀ x ∈ Q.interior, x ∉ Q'.interior

  Distinct pieces have disjoint interiors.

• cover (x : Plane) : x ∈ segment ℝ p b → x ≠ b → ∃ Q ∈ E, x ∈ Q.seg

  Every point ahead of p, short of b, is on a piece.

theorem Schoenflies.IsPieceChain.segment_subset {a b p : Plane} {E : Set Piece} (hC : IsPieceChain a b p E) : segment ℝ p b ⊆ segment ℝ a b

theorem Schoenflies.IsPieceChain.sub_ab {a b p : Plane} {E : Set Piece} (hC : IsPieceChain a b p E) (Q : Piece) : Q ∈ E → Q.seg ⊆ segment ℝ a b

theorem Schoenflies.IsPieceChain.notMem_interior {a b p : Plane} {E : Set Piece} (hC : IsPieceChain a b p E) (hab : a ≠ b) (Q : Piece) : Q ∈ E → p ∉ Q.interior

The current point is not interior to any piece: every piece lies ahead of it, so its near end is already at or beyond p.

theorem Schoenflies.exists_next_piece {a b p : Plane} {E : Set Piece} (hab : a ≠ b) (hfin : E.Finite) (hsub : ∀ Q ∈ E, Q.seg ⊆ segment ℝ a b) (hp : p ∈ segment ℝ a b) (hpnot : ∀ Q ∈ E, p ∉ Q.interior) (hcover : ∀ x ∈ segment ℝ p b, x ≠ b → ∃ Q ∈ E, x ∈ Q.seg) (hpb : p ≠ b) : ∃ Q ∈ E, ∃ (w : Plane), (p = Q.1 ∧ w = Q.2 ∨ p = Q.2 ∧ w = Q.1) ∧ dist a p < dist a w

The piece leaving the current point.

Let m be the least coordinate of an end of a piece strictly ahead of p (the far end b being counted, so that there is one). A point x strictly between p and m is covered by some piece; that piece's near end is at or before p, because it is at most x's coordinate, which is short of m; and it is at or after p, because p is interior to no piece and the far end is beyond p. So the near end is p.

Stated with explicit hypotheses rather than with Schoenflies.IsPieceChain, because it is applied once at the current point and once at the point one step ahead, and at the latter the family is no longer confined to what lies beyond.

theorem Schoenflies.mem_seg_of_end {Q : Piece} {z : Plane} (h : z = Q.1 ∨ z = Q.2) : z ∈ Q.seg

An end of a piece lies on it.

theorem Schoenflies.exists_incWalk_of_chain {a b : Plane} {G : Graph Plane Piece} (hab : a ≠ b) (hbG : b ∈ G.vertexSet) (n : ℕ) (p : Plane) (E : Set Piece) : E.ncard = n → IsPieceChain a b p E → (∀ Q ∈ E, G.IsLink Q Q.1 Q.2) → ∃ (W : List Piece), (∀ (Q : Piece), Q ∈ W ↔ Q ∈ E) ∧ G.IsIncWalk (fun (z : Plane) => dist a z) p W b

A tiling of a segment is a chain. The pieces are walked through from p to b, one at a time, in increasing distance from a; the walk's edge list is exactly the family.

The induction is on the number of pieces, and the step removes the piece leaving p. Three of the seven clauses of Schoenflies.IsPieceChain are inherited verbatim by the smaller family; the work is in re-establishing the other two — that everything left lies beyond the new point, and that it still covers.

Part 3: the perimeter coordinate of a square boundary

The four sides of the square are axis-parallel, so on each of them the Euclidean distance from the side's first corner is the difference of one coordinate. Schoenflies.sqCoord glues the four into one function on the plane: the distance travelled from the north-east corner going counterclockwise. It is dist from the side's first corner plus a multiple of 2r, and that is the only property of it that is ever used.

theorem Schoenflies.dist_eq_abs_fst {z w : Plane} (h : z.ofLp 1 = w.ofLp 1) : dist z w = |z.ofLp 0 - w.ofLp 0|

The distance between two points at the same height.

theorem Schoenflies.dist_eq_abs_snd {z w : Plane} (h : z.ofLp 0 = w.ofLp 0) : dist z w = |z.ofLp 1 - w.ofLp 1|

The distance between two points on the same vertical.

theorem Schoenflies.dist_sqNE_sqNW {r : ℝ} (c : Plane) (hr : 0 ≤ r) : dist (c.sqNE r) (c.sqNW r) = 2 * r

theorem Schoenflies.dist_sqNW_sqSW {r : ℝ} (c : Plane) (hr : 0 ≤ r) : dist (c.sqNW r) (c.sqSW r) = 2 * r

theorem Schoenflies.dist_sqSW_sqSE {r : ℝ} (c : Plane) (hr : 0 ≤ r) : dist (c.sqSW r) (c.sqSE r) = 2 * r

theorem Schoenflies.dist_sqSE_sqNE {r : ℝ} (c : Plane) (hr : 0 ≤ r) : dist (c.sqSE r) (c.sqNE r) = 2 * r

The distance from a side's first corner, in coordinates

theorem Schoenflies.dist_sqNE_of_mem_top {c z : Plane} {r : ℝ} (hr : 0 ≤ r) (hz : z ∈ segment ℝ (c.sqNE r) (c.sqNW r)) : dist (c.sqNE r) z = c.ofLp 0 + r - z.ofLp 0

theorem Schoenflies.dist_sqNW_of_mem_left {c z : Plane} {r : ℝ} (hr : 0 ≤ r) (hz : z ∈ segment ℝ (c.sqNW r) (c.sqSW r)) : dist (c.sqNW r) z = c.ofLp 1 + r - z.ofLp 1

theorem Schoenflies.dist_sqSW_of_mem_bottom {c z : Plane} {r : ℝ} (hr : 0 ≤ r) (hz : z ∈ segment ℝ (c.sqSW r) (c.sqSE r)) : dist (c.sqSW r) z = z.ofLp 0 - (c.ofLp 0 - r)

theorem Schoenflies.dist_sqSE_of_mem_right {c z : Plane} {r : ℝ} (hr : 0 ≤ r) (hz : z ∈ segment ℝ (c.sqSE r) (c.sqNE r)) : dist (c.sqSE r) z = z.ofLp 1 - (c.ofLp 1 - r)

Where two sides meet

theorem Schoenflies.eq_sqNW_of_mem_top_left {c z : Plane} {r : ℝ} (hr : 0 ≤ r) (h₁ : z ∈ segment ℝ (c.sqNE r) (c.sqNW r)) (h₂ : z ∈ segment ℝ (c.sqNW r) (c.sqSW r)) : z = c.sqNW r

theorem Schoenflies.notMem_top_of_mem_bottom {c z : Plane} {r : ℝ} (hr : 0 < r) (h₁ : z ∈ segment ℝ (c.sqSW r) (c.sqSE r)) : z ∉ segment ℝ (c.sqNE r) (c.sqNW r)

theorem Schoenflies.eq_sqNE_of_mem_top_right {c z : Plane} {r : ℝ} (hr : 0 ≤ r) (h₁ : z ∈ segment ℝ (c.sqNE r) (c.sqNW r)) (h₂ : z ∈ segment ℝ (c.sqSE r) (c.sqNE r)) : z = c.sqNE r

theorem Schoenflies.eq_sqSW_of_mem_left_bottom {c z : Plane} {r : ℝ} (hr : 0 ≤ r) (h₁ : z ∈ segment ℝ (c.sqNW r) (c.sqSW r)) (h₂ : z ∈ segment ℝ (c.sqSW r) (c.sqSE r)) : z = c.sqSW r

theorem Schoenflies.notMem_left_of_mem_right {c z : Plane} {r : ℝ} (hr : 0 < r) (h₁ : z ∈ segment ℝ (c.sqSE r) (c.sqNE r)) : z ∉ segment ℝ (c.sqNW r) (c.sqSW r)

theorem Schoenflies.eq_sqSE_of_mem_bottom_right {c z : Plane} {r : ℝ} (hr : 0 ≤ r) (h₁ : z ∈ segment ℝ (c.sqSW r) (c.sqSE r)) (h₂ : z ∈ segment ℝ (c.sqSE r) (c.sqNE r)) : z = c.sqSE r

The perimeter coordinate

noncomputable def Schoenflies.sqCoord (c : Plane) (r : ℝ) (z : Plane) : ℝ

The perimeter coordinate: the distance travelled from the north-east corner going counterclockwise round the boundary of the square. Junk away from the boundary.

The four branches agree at the three corners where consecutive sides meet, so the value is the geometric one on all four sides at once — with the single exception of the north-east corner itself, where the walk both starts and would end. That exception is the whole reason the closing edge of the cycle has to be split off.

Equations

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

theorem Schoenflies.sqCoord_top {c z : Plane} {r : ℝ} (hz : z ∈ segment ℝ (c.sqNE r) (c.sqNW r)) : sqCoord c r z = dist (c.sqNE r) z

theorem Schoenflies.sqCoord_left {c z : Plane} {r : ℝ} (hr : 0 ≤ r) (hz : z ∈ segment ℝ (c.sqNW r) (c.sqSW r)) : sqCoord c r z = 2 * r + dist (c.sqNW r) z

theorem Schoenflies.sqCoord_bottom {c z : Plane} {r : ℝ} (hr : 0 < r) (hz : z ∈ segment ℝ (c.sqSW r) (c.sqSE r)) : sqCoord c r z = 4 * r + dist (c.sqSW r) z

theorem Schoenflies.sqCoord_right {c z : Plane} {r : ℝ} (hr : 0 < r) (hz : z ∈ segment ℝ (c.sqSE r) (c.sqNE r)) (hne : z ≠ c.sqNE r) : sqCoord c r z = 6 * r + dist (c.sqSE r) z

Part 4: the overlay edges on one side

A nondegenerate straight segment inside the boundary of a square lies inside one side: its midpoint is on the boundary, so one of the two coordinates is extreme there, and an average of two numbers at most c i + r can only equal c i + r when both are. That is Schoenflies.exists_side_of_mem_squareEdges, and it is the only genuinely two-dimensional step in the file.

def Schoenflies.sideEdges (pieces : List Piece) (points : List Plane) (c : Plane) (r : ℝ) (S : Piece) : Set Piece

The edges of the overlay lying on one prescribed side of the square.

Equations

• Schoenflies.sideEdges pieces points c r S = {Q : Schoenflies.Piece | Q ∈ Schoenflies.squareEdges pieces points c r ∧ Q.seg ⊆ S.seg}

theorem Schoenflies.coord_mem_segment {y u v : Plane} (i : Fin 2) (h : y ∈ segment ℝ u v) : y.ofLp i ∈ segment ℝ (u.ofLp i) (v.ofLp i)

A coordinate of a point of a segment lies on the segment of the coordinates: the coordinate map is linear.

theorem Schoenflies.abs_le_of_mem_frontier {c : Plane} {r : ℝ} {y : Plane} (hy : y ∈ frontier (c.closedSquare r)) : |y.ofLp 0 - c.ofLp 0| ≤ r ∧ |y.ofLp 1 - c.ofLp 1| ≤ r

A point of the boundary of a square has both coordinates within r of the centre's.

theorem Schoenflies.exists_side_of_mem_squareEdges {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} (hr : 0 < r) {Q : Piece} (hQ : Q ∈ squareEdges pieces points c r) : ∃ S ∈ squarePieces c r, Q ∈ sideEdges pieces points c r S

Every edge of the overlay on a square lies on one of the four sides.

Part 5: the four sides, chained

Each side of the square is a source segment of the overlay, so the edges lying on it tile it, and Part 2 walks through them. The four walks are then glued at the corners.

theorem Schoenflies.mem_vertexSet_squareGraph_iff {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} {y : Plane} : y ∈ (squareGraph pieces points c r).vertexSet ↔ ∃ Q ∈ squareEdges pieces points c r, y = Q.1 ∨ y = Q.2

theorem Schoenflies.mem_edgeSet_squareGraph_iff {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} {Q : Piece} : Q ∈ (squareGraph pieces points c r).edgeSet ↔ Q ∈ squareEdges pieces points c r

theorem Schoenflies.inc_of_mem_squareEdges {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} {Q : Piece} {y : Plane} (hQ : Q ∈ squareEdges pieces points c r) (hy : y = Q.1 ∨ y = Q.2) : (squareGraph pieces points c r).Inc Q y

An end of an edge is incident with it.

theorem Schoenflies.isLink_of_mem_squareEdges {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} {Q : Piece} (hQ : Q ∈ squareEdges pieces points c r) : (squareGraph pieces points c r).IsLink Q Q.1 Q.2

Every edge of the graph is drawn where its own name says.

theorem Schoenflies.side_subset_frontier {c : Plane} {r : ℝ} (hr : 0 ≤ r) {S : Piece} (hS : S ∈ squarePieces c r) : S.seg ⊆ frontier (c.closedSquare r)

A side of the square lies on its boundary.

The subdivision of one source segment

Nothing about squares enters here. Schoenflies/SquareMeshConnected.lean records this as the theorem missing from main — "the subdivision of a segment at a finite point set is a path" — that blocks prop:anchored-square-mesh from being carried over to Schoenflies.squareMesh.

def Schoenflies.insideEdges (pieces : List Piece) (points : List Plane) (P₀ : Piece) : Set Piece

The edges of an overlay lying inside one of its source segments.

Equations

• Schoenflies.insideEdges pieces points P₀ = {Q : Schoenflies.Piece | Q ∈ Schoenflies.overlayPieces pieces points ∧ Q.seg ⊆ P₀.seg}

theorem Schoenflies.isPieceChain_insideEdges {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) {P₀ : Piece} (hP₀ : P₀ ∈ pieces) : IsPieceChain P₀.1 P₀.2 P₀.1 (insideEdges pieces points P₀)

The edges inside one source segment tile it. Every clause is a property of the polygonal overlay already on main; the covering clause is the one that needs P₀ to be a source segment.

theorem Schoenflies.exists_incWalk_insideEdges {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) {P₀ : Piece} (hP₀ : P₀ ∈ pieces) (hP₀nd : P₀.Nondeg) : ∃ (W : List Piece), (∀ (Q : Piece), Q ∈ W ↔ Q ∈ insideEdges pieces points P₀) ∧ (overlayGraph pieces points).IsIncWalk (fun (z : Plane) => dist P₀.1 z) P₀.1 W P₀.2

The subdivision of one source segment of an overlay is a path, from one end of the segment to the other, taking every overlay edge inside it exactly once, in increasing distance from the first end.

theorem Schoenflies.sideEdges_eq_insideEdges {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} (hr : 0 ≤ r) {S : Piece} (hS : S ∈ squarePieces c r) : sideEdges pieces points c r S = insideEdges pieces points S

On a side of the square, "inside the boundary" is automatic.

theorem Schoenflies.isPieceChain_sideEdges {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) (hr : 0 < r) (hsub : ∀ P ∈ squarePieces c r, P ∈ pieces) {S : Piece} (hS : S ∈ squarePieces c r) : IsPieceChain S.1 S.2 S.1 (sideEdges pieces points c r S)

The edges on one side tile it.

theorem Schoenflies.corner_mem_vertexSet {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hr : 0 < r) (hsub : ∀ P ∈ squarePieces c r, P ∈ pieces) {S : Piece} (hS : S ∈ squarePieces c r) : S.2 ∈ (squareGraph pieces points c r).vertexSet

The far corner of a side is a vertex: it is an end of a source segment, hence a cut point, and it lies on the boundary.

theorem Schoenflies.exists_side_walk {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) (hr : 0 < r) (hsub : ∀ P ∈ squarePieces c r, P ∈ pieces) {u v : Plane} (hS : (u, v) ∈ squarePieces c r) : ∃ (W : List Piece), (∀ (Q : Piece), Q ∈ W ↔ Q ∈ sideEdges pieces points c r (u, v)) ∧ (squareGraph pieces points c r).IsIncWalk (fun (z : Plane) => dist u z) u W v

The walk along one side, from its first corner to its second, taking every edge of the overlay that lies on it exactly once, in increasing distance from the first corner.

theorem Schoenflies.walkVertices_squareGraph_subset {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} {u : Plane} {W : List Piece} {T : Set Plane} (hu : u ∈ T) (hW : ∀ Q ∈ W, Q.seg ⊆ T) : (squareGraph pieces points c r).walkVertices u W ⊆ T

What a walk of the square graph visits stays inside anything its edges stay inside.

theorem Schoenflies.not_nondeg_of_seg_subset_singleton {Q : Piece} {t : Plane} (h : ∀ y ∈ Q.seg, y = t) : ¬Q.Nondeg

A piece all of whose points are one point is degenerate.

Part 6: the cycle, and SquaresTwoConnected

The four walks are concatenated into a closed walk at the north-east corner. The perimeter coordinate increases along the first three sides and along all of the fourth but its last step, which returns to the corner where the coordinate is 0; so that step is split off and becomes the distinguished edge of Graph.IsCycleThrough.

theorem Schoenflies.sqNW_ne_sqNE {r : ℝ} (c : Plane) (hr : 0 < r) : c.sqNW r ≠ c.sqNE r

theorem Schoenflies.sqSE_ne_sqNE {r : ℝ} (c : Plane) (hr : 0 < r) : c.sqSE r ≠ c.sqNE r

theorem Schoenflies.exists_isLongCycle_squareGraph {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) (hr : 0 < r) (hsub : ∀ P ∈ squarePieces c r, P ∈ pieces) : ∃ (e : Piece) (u : Plane) (v : Plane) (D : List Piece) (w : Plane), (squareGraph pieces points c r).IsLongCycle e u v D w ∧ (squareGraph pieces points c r).cycleGraph u e D = squareGraph pieces points c r

The boundary cycle of a subdivided square. The whole of squareGraph is a cycle: an edge e, a detour D running the other way round, and a third vertex. The second clause is what makes the first usable — Graph.IsLongCycle.isTwoConnected proves the cycle graph 2-connected, and here the cycle graph is the graph itself.

theorem Schoenflies.squareGraph_isTwoConnected {c : Plane} {r : ℝ} {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) (hr : 0 < r) (hsub : ∀ P ∈ squarePieces c r, P ∈ pieces) : (squareGraph pieces points c r).IsTwoConnected

The part of a polygonal overlay on the boundary of one of its squares is 2-connected. It is a cycle through at least four vertices — the corners — so Graph.IsLongCycle.isTwoConnected finishes.

theorem Schoenflies.squaresTwoConnected : SquaresTwoConnected

Schoenflies.SquaresTwoConnected, discharged. Substituting this into Schoenflies.exists_face_of_notMem_arc makes thm:arc-complement, lem:accessible-dense and thm:jordan without an auxiliary separation hypothesis.