Scaffolding for the arc-complement theorem

thm:arc-complement — a simple arc does not separate the plane — is proved by covering the arc with a chain of small axis-parallel squares, overlaying their boundaries into one plane graph G, and showing that the two given points lie in the outer face of G, which is then disjoint from the arc. This module builds everything in that proof that does not need the outer-chain lemma (lem:outer-chain), so that the theorem itself becomes a short assembly.

What is here

1. The square boundary as a polygon. Schoenflies.squarePolygon c hr : ClosedPolygon 1 is the axis-parallel square of ℓ^∞-radius r about c, presented the way the parity and overlay machinery consume a polygon — as a ClosedPolygon, not as a set. Its carrier is frontier (Plane.closedSquare c r) (carrier_squarePolygon), and the polygonal Jordan curve theorem then hands over that this frontier is a Jordan curve, is polygonal, and is separating, with inside the open square and outside the complement of the closed one.

   Schoenflies.modelCurve is the case c = 0, r = 1 as a set; nothing there is a ClosedPolygon, so nothing there could be fed to the overlay.

2. Two nearby congruent squares meet twice. The route taken is the coordinate one, not the blueprint's topological one, because the meeting points can be written down: a vertical side of one square crosses a horizontal side of the other, transversally, in a single point. That "single point" is exactly what Schoenflies.MeetsAreCut needs to turn a meeting point into a vertex of the overlay graph, which is what Graph.IsTwoConnected.union consumes. See exists_two_common_vertices and the discussion before it.

3. The uniform-continuity partition. Schoenflies.sample n i = i / n is the even partition of [0,1]; exists_mesh says that for n large enough — and n may be asked to be a multiple of any prescribed k, which is what makes the fine partition refine the coarse one — every point of α '' [t i, t (i+1)] is within ε of α (t i).

4. Nonadjacent subarcs are at positive distance. exists_pos_dist_nonadjacent.

5. The covering clause. image_subset_iUnion_closedSquare: the closed squares of radius ε about the samples cover the arc.

Blueprint

• squarePolygon, carrier_squarePolygon — the square boundary of the proof of thm:arc-complement ("around every sample draw the boundary of the axis-parallel square of ℓ^∞-radius δ/4"), as a polygon.
• isJordanCurve_frontier_closedSquare, isPolygonal_frontier_closedSquare, isSeparating_frontier_closedSquare, inside_frontier_closedSquare, outside_frontier_closedSquare — thm:polygonal-jordan specialised to the square.
• exists_two_meets, exists_two_frontier_inter — "their boundary cycles therefore meet in at least two points", thm:arc-complement; exists_two_meets is the sharp form, in which each meeting point is a transversal crossing of two sides.
• exists_two_common_vertices, exists_two_cut_points, exists_overlayPiece_end_subset — the bridge from "two common points" to the two common vertices that lem:union-two-connected (Graph.IsTwoConnected.union) consumes.
• sample, exists_mesh — "By uniform continuity, choose a partition …", used twice in thm:arc-complement and again in prop:anchored-square-mesh.
• exists_pos_dist_nonadjacent — "Nonadjacent compact subarcs are disjoint, hence at positive distance by lem:compact-separation(b)".
• image_subset_iUnion_closedSquare — "Every point of A lies in or on one of the small squares".

Part 1: the boundary of a square, as a polygon

Everything is done in coordinates. The four corners are named, the four sides are the four segments between consecutive corners, and the two lemmas Plane.mem_seg_horiz and Plane.mem_seg_vert of Schoenflies/ModelCurve.lean reduce membership of a side to a pair of scalar conditions.

theorem Schoenflies.Plane.supDist_eq_max (z c : Plane) : z.supDist c = max |z.ofLp 0 - c.ofLp 0| |z.ofLp 1 - c.ofLp 1|

The sup distance in coordinates.

theorem Schoenflies.Plane.mem_frontier_closedSquare {c z : Plane} {r : ℝ} : z ∈ frontier (c.closedSquare r) ↔ max |z.ofLp 0 - c.ofLp 0| |z.ofLp 1 - c.ofLp 1| = r

theorem Schoenflies.Plane.mem_frontier_closedSquare_of_fst {c z : Plane} {r : ℝ} (h0 : |z.ofLp 0 - c.ofLp 0| = r) (h1 : |z.ofLp 1 - c.ofLp 1| ≤ r) : z ∈ frontier (c.closedSquare r)

A point whose first coordinate is extreme and whose second is dominated is on the boundary.

theorem Schoenflies.Plane.mem_frontier_closedSquare_of_snd {c z : Plane} {r : ℝ} (h1 : |z.ofLp 1 - c.ofLp 1| = r) (h0 : |z.ofLp 0 - c.ofLp 0| ≤ r) : z ∈ frontier (c.closedSquare r)

The same with the roles of the two coordinates exchanged.

def Schoenflies.Plane.sqNE (c : Plane) (r : ℝ) : Plane

The north-east corner of the square of radius r about c.

Equations

• c.sqNE r = Schoenflies.Plane.mk (c.ofLp 0 + r) (c.ofLp 1 + r)

def Schoenflies.Plane.sqNW (c : Plane) (r : ℝ) : Plane

The north-west corner.

Equations

• c.sqNW r = Schoenflies.Plane.mk (c.ofLp 0 - r) (c.ofLp 1 + r)

def Schoenflies.Plane.sqSW (c : Plane) (r : ℝ) : Plane

The south-west corner.

Equations

• c.sqSW r = Schoenflies.Plane.mk (c.ofLp 0 - r) (c.ofLp 1 - r)

def Schoenflies.Plane.sqSE (c : Plane) (r : ℝ) : Plane

The south-east corner.

Equations

• c.sqSE r = Schoenflies.Plane.mk (c.ofLp 0 + r) (c.ofLp 1 - r)

@[simp]

theorem Schoenflies.Plane.sqNE_zero {c : Plane} {r : ℝ} : (c.sqNE r).ofLp 0 = c.ofLp 0 + r

@[simp]

theorem Schoenflies.Plane.sqNE_one {c : Plane} {r : ℝ} : (c.sqNE r).ofLp 1 = c.ofLp 1 + r

@[simp]

theorem Schoenflies.Plane.sqNW_zero {c : Plane} {r : ℝ} : (c.sqNW r).ofLp 0 = c.ofLp 0 - r

@[simp]

theorem Schoenflies.Plane.sqNW_one {c : Plane} {r : ℝ} : (c.sqNW r).ofLp 1 = c.ofLp 1 + r

@[simp]

theorem Schoenflies.Plane.sqSW_zero {c : Plane} {r : ℝ} : (c.sqSW r).ofLp 0 = c.ofLp 0 - r

@[simp]

theorem Schoenflies.Plane.sqSW_one {c : Plane} {r : ℝ} : (c.sqSW r).ofLp 1 = c.ofLp 1 - r

@[simp]

theorem Schoenflies.Plane.sqSE_zero {c : Plane} {r : ℝ} : (c.sqSE r).ofLp 0 = c.ofLp 0 + r

@[simp]

theorem Schoenflies.Plane.sqSE_one {c : Plane} {r : ℝ} : (c.sqSE r).ofLp 1 = c.ofLp 1 - r

theorem Schoenflies.Plane.mem_segment_abs {a r x : ℝ} (hr : 0 ≤ r) : x ∈ segment ℝ (a - r) (a + r) ↔ |x - a| ≤ r

A real number is within r of a exactly when it lies on the segment from a - r to a + r, in either order. Stated through uIcc so that the two orders are one lemma.

theorem Schoenflies.Plane.mem_segment_abs' {a r x : ℝ} (hr : 0 ≤ r) : x ∈ segment ℝ (a + r) (a - r) ↔ |x - a| ≤ r

theorem Schoenflies.Plane.mem_seg_top {c z : Plane} {r : ℝ} (hr : 0 ≤ r) : z ∈ segment ℝ (c.sqNE r) (c.sqNW r) ↔ z.ofLp 1 = c.ofLp 1 + r ∧ |z.ofLp 0 - c.ofLp 0| ≤ r

The top side.

theorem Schoenflies.Plane.mem_seg_left {c z : Plane} {r : ℝ} (hr : 0 ≤ r) : z ∈ segment ℝ (c.sqNW r) (c.sqSW r) ↔ z.ofLp 0 = c.ofLp 0 - r ∧ |z.ofLp 1 - c.ofLp 1| ≤ r

The left side.

theorem Schoenflies.Plane.mem_seg_bottom {c z : Plane} {r : ℝ} (hr : 0 ≤ r) : z ∈ segment ℝ (c.sqSW r) (c.sqSE r) ↔ z.ofLp 1 = c.ofLp 1 - r ∧ |z.ofLp 0 - c.ofLp 0| ≤ r

The bottom side.

theorem Schoenflies.Plane.mem_seg_right {c z : Plane} {r : ℝ} (hr : 0 ≤ r) : z ∈ segment ℝ (c.sqSE r) (c.sqNE r) ↔ z.ofLp 0 = c.ofLp 0 + r ∧ |z.ofLp 1 - c.ofLp 1| ≤ r

The right side.

theorem Schoenflies.Plane.mem_frontier_closedSquare_iff_sides {c z : Plane} {r : ℝ} (hr : 0 ≤ r) : z ∈ frontier (c.closedSquare r) ↔ z ∈ segment ℝ (c.sqNE r) (c.sqNW r) ∨ z ∈ segment ℝ (c.sqNW r) (c.sqSW r) ∨ z ∈ segment ℝ (c.sqSW r) (c.sqSE r) ∨ z ∈ segment ℝ (c.sqSE r) (c.sqNE r)

The boundary of a square is the union of its four sides.

The square as a ClosedPolygon

Four corners in counterclockwise order. edges_meet splits into the four adjacent pairs, where segment_inter_shared applies because consecutive sides are perpendicular, and the two opposite pairs, which are disjoint because opposite sides are pinned to different values of one coordinate.

def Schoenflies.squarePolygon (c : Plane) {r : ℝ} (hr : 0 < r) : ClosedPolygon 1

**The boundary of the axis-parallel square of ℓ^∞-radius r about c, as a closed polygon.**This is the presentation the overlay and parity machinery consume; Schoenflies.modelCurve is the case c = 0, r = 1 but only as a set.

Equations

• Schoenflies.squarePolygon c hr = { vertex := ![c.sqNE r, c.sqNW r, c.sqSW r, c.sqSE r], vertex_inj := ⋯, edges_meet := ⋯, corner := ⋯ }

@[simp]

theorem Schoenflies.squarePolygon_vertex_zero {c : Plane} {r : ℝ} (hr : 0 < r) : (squarePolygon c hr).vertex 0 = c.sqNE r

@[simp]

theorem Schoenflies.squarePolygon_vertex_one {c : Plane} {r : ℝ} (hr : 0 < r) : (squarePolygon c hr).vertex 1 = c.sqNW r

@[simp]

theorem Schoenflies.squarePolygon_vertex_two {c : Plane} {r : ℝ} (hr : 0 < r) : (squarePolygon c hr).vertex 2 = c.sqSW r

@[simp]

theorem Schoenflies.squarePolygon_vertex_three {c : Plane} {r : ℝ} (hr : 0 < r) : (squarePolygon c hr).vertex 3 = c.sqSE r

theorem Schoenflies.edge_squarePolygon_zero {c : Plane} {r : ℝ} (hr : 0 < r) : (squarePolygon c hr).edge 0 = segment ℝ (c.sqNE r) (c.sqNW r)

theorem Schoenflies.edge_squarePolygon_one {c : Plane} {r : ℝ} (hr : 0 < r) : (squarePolygon c hr).edge 1 = segment ℝ (c.sqNW r) (c.sqSW r)

theorem Schoenflies.edge_squarePolygon_two {c : Plane} {r : ℝ} (hr : 0 < r) : (squarePolygon c hr).edge 2 = segment ℝ (c.sqSW r) (c.sqSE r)

theorem Schoenflies.edge_squarePolygon_three {c : Plane} {r : ℝ} (hr : 0 < r) : (squarePolygon c hr).edge 3 = segment ℝ (c.sqSE r) (c.sqNE r)

theorem Schoenflies.carrier_squarePolygon {c : Plane} {r : ℝ} (hr : 0 < r) : (squarePolygon c hr).carrier = frontier (c.closedSquare r)

The polygon carries the boundary of the square. This is the identification that lets the polygonal Jordan curve theorem be read as a statement about frontier (closedSquare c r), and it is what the overlay consumes.

What the polygonal Jordan curve theorem says about a square

All four clauses come from main; only the identification of the two regions is new, and it is Plane.connectedComponentIn_eq_of_frontier_disjoint twice: once for the open square and once for its complement.

theorem Schoenflies.isJordanCurve_frontier_closedSquare {r : ℝ} (c : Plane) (hr : 0 < r) : IsJordanCurve (frontier (c.closedSquare r))

theorem Schoenflies.isPolygonal_frontier_closedSquare {r : ℝ} (c : Plane) (hr : 0 < r) : IsPolygonal (frontier (c.closedSquare r))

theorem Schoenflies.isSeparating_frontier_closedSquare {r : ℝ} (c : Plane) (hr : 0 < r) : IsSeparating (frontier (c.closedSquare r))

theorem Schoenflies.Plane.isBounded_closedSquare (c : Plane) (r : ℝ) : Bornology.IsBounded (c.closedSquare r)

A closed square is bounded — the statement for an arbitrary centre. Graph.isBounded_closedSquare is the same fact for the centre 0 only.

theorem Schoenflies.Plane.beyondSquare_subset_compl_closedSquare (c : Plane) (r : ℝ) : beyondSquare (r + c.supNorm) ⊆ (c.closedSquare r)ᶜ

The outside of a square about c contains the outside of a large square about the origin, hence is unbounded.

theorem Schoenflies.Plane.not_isBounded_compl_closedSquare (c : Plane) (r : ℝ) : ¬Bornology.IsBounded (c.closedSquare r)ᶜ

theorem Schoenflies.Plane.mem_compl_closedSquare_iff (c : Plane) (r : ℝ) (x : Plane) : x ∈ (c.closedSquare r)ᶜ ↔ x - c ∈ beyondSquare r

Membership in the outside of a square, as membership in a translate of beyondSquare.

theorem Schoenflies.Plane.compl_closedSquare_eq_image (c : Plane) (r : ℝ) : (c.closedSquare r)ᶜ = (fun (x : Plane) => x + c) '' beyondSquare r

theorem Schoenflies.Plane.isConnected_compl_closedSquare (c : Plane) (r : ℝ) : IsConnected (c.closedSquare r)ᶜ

The plane outside a closed square is connected: a translate of beyondSquare.

theorem Schoenflies.Plane.compl_frontier_closedSquare (c : Plane) (r : ℝ) : (frontier (c.closedSquare r))ᶜ = c.openSquare r ∪ (c.closedSquare r)ᶜ

The complement of the boundary is the open square together with the outside.

theorem Schoenflies.Plane.frontier_openSquare_subset (c : Plane) (r : ℝ) : frontier (c.openSquare r) ⊆ frontier (c.closedSquare r)

The frontier of the open square lies in the frontier of the closed one. That inclusion is all lem:recognizing-a-component needs.

theorem Schoenflies.inside_frontier_closedSquare (c : Plane) (r : ℝ) : inside (frontier (c.closedSquare r)) = c.openSquare r

The inside of a square boundary is the open square.

theorem Schoenflies.outside_frontier_closedSquare (c : Plane) (r : ℝ) : outside (frontier (c.closedSquare r)) = (c.closedSquare r)ᶜ

The outside of a square boundary is the complement of the closed square.

Part 2: two nearby congruent squares meet twice

The blueprint (thm:arc-complement) argues topologically: neither congruent square contains the other, so each boundary has nonempty relatively open parts inside the other open square and outside the other closed square, and a single intersection point could not disconnect a connected boundary curve.

The route taken here is the coordinate one, and it proves more than the blueprint asks. Write the two centres as c₁ and c₂ = c₁ + (a, b) with |a|, |b| < r. Then

• the vertical side of S₁ on the side of c₂ crosses the horizontal side of S₂ away from c₁, in the single point (c₁₀ ± r, c₂₁ ∓ r);
• the horizontal side of S₁ away from c₂ crosses the vertical side of S₂ on the side of c₁, in the single point (c₂₀ ∓ r, c₁₁ ± r);

and the two points differ because their first coordinates differ by 2r - |a| ≠ 0. Each is a transversal crossing — the meet of the two sides is a singleton, not a segment — which is exactly what MeetsAreCut turns into a cut point and hence into a vertex of the overlay graph. Two common points would not be enough for Graph.IsTwoConnected.union, which wants two common vertices; see exists_two_common_vertices.

def Schoenflies.squarePieces (c : Plane) (r : ℝ) : List Piece

The four sides of the square of ℓ^∞-radius r about c, as Pieces, in the same cyclic order as squarePolygon.

Equations

• Schoenflies.squarePieces c r = [(c.sqNE r, c.sqNW r), (c.sqNW r, c.sqSW r), (c.sqSW r, c.sqSE r), (c.sqSE r, c.sqNE r)]

theorem Schoenflies.cover_squarePieces {r : ℝ} (c : Plane) (hr : 0 ≤ r) : cover (squarePieces c r) = frontier (c.closedSquare r)

theorem Schoenflies.squarePieces_nondeg {r : ℝ} (c : Plane) (hr : 0 < r) (P : Piece) : P ∈ squarePieces c r → P.Nondeg

A vertical side crosses a horizontal side in one point

theorem Schoenflies.mem_segment_of_bounds {u v y : ℝ} (h : u ≤ y ∧ y ≤ v ∨ v ≤ y ∧ y ≤ u) : y ∈ segment ℝ u v

Membership in a real segment from two inequalities, in whichever order the ends come.

theorem Schoenflies.meetOf_vert_horiz {x₀ y₀ u v s t : ℝ} (hy : y₀ ∈ segment ℝ u v) (hx : x₀ ∈ segment ℝ s t) : meetOf (Plane.mk x₀ u, Plane.mk x₀ v) (Plane.mk s y₀, Plane.mk t y₀) = {Plane.mk x₀ y₀}

A vertical segment and a horizontal segment that reach each other meet in exactly one point. Both coordinates are pinned, one by each segment.

theorem Schoenflies.meetOf_horiz_vert {x₀ y₀ u v s t : ℝ} (hx : x₀ ∈ segment ℝ s t) (hy : y₀ ∈ segment ℝ u v) : meetOf (Plane.mk s y₀, Plane.mk t y₀) (Plane.mk x₀ u, Plane.mk x₀ v) = {Plane.mk x₀ y₀}

The same crossing with the two pieces in the other order.

theorem Schoenflies.exists_two_meets {c₁ c₂ : Plane} {r : ℝ} (hr : 0 < r) (hd : c₁.supDist c₂ < r) : ∃ (p : Plane) (q : Plane), p ≠ q ∧ (∃ P ∈ squarePieces c₁ r, ∃ Q ∈ squarePieces c₂ r, meetOf P Q = {p}) ∧ ∃ P ∈ squarePieces c₁ r, ∃ Q ∈ squarePieces c₂ r, meetOf P Q = {q}

Two congruent axis-parallel squares whose centres are less than one radius apart have boundaries meeting in at least two points, and each meeting point is a transversal crossing: the two sides that produce it meet in a singleton.

The two centres are not required to be distinct — for equal centres the two squares coincide and the two points produced are two of the four corners, which is what the blueprint's "or coincide" allows.

From a meeting point to a vertex of the overlay

Graph.IsTwoConnected.union needs two common vertices, not two common points. The overlay's cut-point condition MeetsAreCut says that both ends of the meet of two source pieces are cut points; when the meet is a singleton both ends are that one point, so the crossing point is a cut point, and overlayGraph_mem_vertexSet_of_mem_cover promotes a cut point on the union to a vertex. This is the whole bridge, and it is why exists_two_meets is stated with singleton meets rather than with mere common points.

theorem Schoenflies.overlayGraph_mem_vertexSet_of_meetOf_eq_singleton {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hMeets : MeetsAreCut pieces points) {P Q : Piece} (hP : P ∈ pieces) (hQ : Q ∈ pieces) {p : Plane} (hmeet : meetOf P Q = {p}) : p ∈ (overlayGraph pieces points).vertexSet

A transversal crossing of two source pieces is a cut point of any overlay built on them, hence a vertex of the overlay graph.

theorem Schoenflies.mem_frontier_of_meetOf_eq_singleton {c₁ c₂ : Plane} {r : ℝ} (hr : 0 ≤ r) {P Q : Piece} {p : Plane} (hP : P ∈ squarePieces c₁ r) (hQ : Q ∈ squarePieces c₂ r) (h : meetOf P Q = {p}) : p ∈ frontier (c₁.closedSquare r) ∧ p ∈ frontier (c₂.closedSquare r)

The crossing point lies on both square boundaries.

theorem Schoenflies.exists_two_frontier_inter {c₁ c₂ : Plane} {r : ℝ} (hr : 0 < r) (hd : c₁.supDist c₂ < r) : ∃ (p : Plane) (q : Plane), p ≠ q ∧ p ∈ frontier (c₁.closedSquare r) ∩ frontier (c₂.closedSquare r) ∧ q ∈ frontier (c₁.closedSquare r) ∩ frontier (c₂.closedSquare r)

The blueprint's statement: the two boundaries meet in at least two points.

theorem Schoenflies.exists_two_common_vertices {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hMeets : MeetsAreCut pieces points) {c₁ c₂ : Plane} {r : ℝ} (hr : 0 < r) (hd : c₁.supDist c₂ < r) (h₁ : ∀ P ∈ squarePieces c₁ r, P ∈ pieces) (h₂ : ∀ P ∈ squarePieces c₂ r, P ∈ pieces) : ∃ (p : Plane) (q : Plane), p ≠ q ∧ p ∈ (overlayGraph pieces points).vertexSet ∧ q ∈ (overlayGraph pieces points).vertexSet

Two nearby squares contribute two common vertices to any overlay containing both.

This is the form Graph.IsTwoConnected.union consumes: a ≠ b, with both a and b vertices of the graphs being joined. What is not proved here — because it depends on how the next wave splits one overlay into the pieces it unions — is that p and q are vertices of the two subgraphs Γ and Γ' separately. The extra fact needed for that is recorded by exists_two_cut_points below: p and q are cut points lying on each of the two boundaries, so overlayGraph_mem_vertexSet_of_mem_cover places them in the vertex set of whichever sub-overlay covers the boundary in question.

Localizing a cut point to one source piece

overlayGraph_mem_vertexSet_of_mem_cover says a cut point on the union is a vertex, but it says nothing about which edge it is an end of. The next wave has to place the two common points of two neighbouring squares in the vertex sets of the two graphs being unioned, and for that the edge must be pinned inside the boundary it came from. The three lemmas below do that; the first two are general facts about subdivide whose home is Schoenflies/Subdivide.lean.

theorem Schoenflies.subdivide_mono (points : List Plane) {l pieces : List Piece} : (∀ P ∈ l, P ∈ pieces) → ∀ Q ∈ subdivide l points, Q ∈ subdivide pieces points

Subdividing is monotone in the piece list.

theorem Schoenflies.exists_overlayPiece_end_subset {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) {x : Plane} (hxp : x ∈ points) {P₀ : Piece} (hP₀ : P₀ ∈ pieces) (hx : x ∈ P₀.seg) : ∃ Q ∈ overlayPieces pieces points, (x = Q.1 ∨ x = Q.2) ∧ Q.seg ⊆ P₀.seg

A cut point on a source piece is an end of an overlay edge inside that source piece. This is overlayGraph_mem_vertexSet_of_mem_cover with the witnessing edge named and pinned: the edge lies inside the prescribed source segment, so a subgraph spanned by the edges inside that segment has the point among its vertices.

theorem Schoenflies.exists_two_cut_points {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hMeets : MeetsAreCut pieces points) {c₁ c₂ : Plane} {r : ℝ} (hr : 0 < r) (hd : c₁.supDist c₂ < r) (h₁ : ∀ P ∈ squarePieces c₁ r, P ∈ pieces) (h₂ : ∀ P ∈ squarePieces c₂ r, P ∈ pieces) : ∃ (p : Plane) (q : Plane), p ≠ q ∧ p ∈ points ∧ q ∈ points ∧ p ∈ frontier (c₁.closedSquare r) ∩ frontier (c₂.closedSquare r) ∧ q ∈ frontier (c₁.closedSquare r) ∩ frontier (c₂.closedSquare r)

The localizable form: two distinct cut points, each lying on both square boundaries. Feed a cut point together with "it lies on the union carried by Γ" to overlayGraph_mem_vertexSet_of_mem_cover to get a vertex of Γ.

Part 3: the uniform-continuity partition

The blueprint asks for "a partition 0 = t₀ < t₁ < ⋯ < t_k = 1, with k ≥ 3, such that every point of α([t_{i-1}, t_i]) is at distance less than ε from α(t_{i-1})", and separately for a refinement of it inside each piece. Both are served by the even partition: nothing in the proof uses anything about the partition beyond the mesh bound, and taking t_i = i/n makes "the fine partition refines the coarse one" the arithmetic identity sample (k*m) (i*m) = sample k i rather than a bookkeeping argument. The number of pieces can be forced to be a multiple of any prescribed k and hence as large as one likes, which covers the k ≥ 3 clause.

noncomputable def Schoenflies.sample (n i : ℕ) : ℝ

The i-th point of the even partition of [0,1] into n pieces.

Equations

• Schoenflies.sample n i = ↑i / ↑n

@[simp]

theorem Schoenflies.sample_zero (n : ℕ) : sample n 0 = 0

theorem Schoenflies.sample_last {n : ℕ} (hn : 0 < n) : sample n n = 1

theorem Schoenflies.sample_nonneg (n i : ℕ) : 0 ≤ sample n i

theorem Schoenflies.sample_mono {n i j : ℕ} (h : i ≤ j) : sample n i ≤ sample n j

theorem Schoenflies.sample_strictMono {n i j : ℕ} (hn : 0 < n) (h : i < j) : sample n i < sample n j

theorem Schoenflies.sample_le_one {n i : ℕ} (h : i ≤ n) : sample n i ≤ 1

theorem Schoenflies.sample_mem_I {n i : ℕ} (h : i ≤ n) : sample n i ∈ unitInterval

theorem Schoenflies.sample_succ_sub (n i : ℕ) : sample n (i + 1) - sample n i = 1 / ↑n

Consecutive samples are 1/n apart.

theorem Schoenflies.sample_mul {k m i : ℕ} (hm : 0 < m) : sample (k * m) (i * m) = sample k i

The fine partition refines the coarse one: the multiples of m among the k*m samples are the k samples.

theorem Schoenflies.Icc_sample_subset_I {n i : ℕ} (h : i + 1 ≤ n) : Set.Icc (sample n i) (sample n (i + 1)) ⊆ unitInterval

theorem Schoenflies.exists_mem_Icc_sample {n : ℕ} (hn : 0 < n) {s : ℝ} (hs : s ∈ unitInterval) : ∃ i < n, s ∈ Set.Icc (sample n i) (sample n (i + 1))

Every parameter lies in one of the n closed cells of the even partition.

theorem Schoenflies.exists_mesh {α : ℝ → Plane} (hα : ContinuousOn α unitInterval) {ε : ℝ} (hε : 0 < ε) (k : ℕ) (hk : 0 < k) : ∃ (m : ℕ), 0 < m ∧ ∀ i < k * m, ∀ s ∈ Set.Icc (sample (k * m) i) (sample (k * m) (i + 1)), dist (α s) (α (sample (k * m) i)) < ε

The uniform-continuity partition. For every ε > 0 and every prescribed k > 0 there is a multiple k * m of k such that on each cell of the even partition into k * m pieces the map moves by less than ε. Taking k = 1 gives the plain statement; taking k to be the size of a coarser partition makes this one a refinement of it, by sample_mul.

Part 4: nonadjacent subarcs are at positive distance

def Schoenflies.subarcCell (α : ℝ → Plane) (n i : ℕ) : Set Plane

The i-th subarc of the even partition of an arc into n pieces.

Equations

• Schoenflies.subarcCell α n i = α '' Set.Icc (Schoenflies.sample n i) (Schoenflies.sample n (i + 1))

theorem Schoenflies.isCompact_subarcCell {α : ℝ → Plane} (hα : ContinuousOn α unitInterval) {n i : ℕ} (h : i + 1 ≤ n) : IsCompact (subarcCell α n i)

theorem Schoenflies.subarcCell_nonempty {α : ℝ → Plane} {n i : ℕ} : (subarcCell α n i).Nonempty

theorem Schoenflies.disjoint_subarcCell {α : ℝ → Plane} (hinj : Set.InjOn α unitInterval) {n i j : ℕ} (hi : i + 1 ≤ n) (hj : j + 1 ≤ n) (hij : i + 2 ≤ j) : Disjoint (subarcCell α n i) (subarcCell α n j)

Nonadjacent cells of an injective parametrisation are disjoint: their parameter intervals are, and injectivity carries that to the images.

theorem Schoenflies.exists_pos_dist_nonadjacent {α : ℝ → Plane} (hα : ContinuousOn α unitInterval) (hinj : Set.InjOn α unitInterval) {n : ℕ} : ∃ ρ > 0, ∀ i < n, ∀ j < n, i + 2 ≤ j → ∀ x ∈ subarcCell α n i, ∀ y ∈ subarcCell α n j, ρ ≤ dist x y

Nonadjacent subarcs are at positive distance — the blueprint's δ'. A finite family of positive separations, merged by exists_pos_forall_of_finite.

Part 5: the covering clause

theorem Schoenflies.image_subset_iUnion_closedSquare {α : ℝ → Plane} {n : ℕ} (hn : 0 < n) {ε : ℝ} (hmesh : ∀ i < n, ∀ s ∈ Set.Icc (sample n i) (sample n (i + 1)), dist (α s) (α (sample n i)) < ε) : α '' unitInterval ⊆ ⋃ i ∈ Finset.range n, (α (sample n i)).closedSquare ε

Every point of the arc lies in or on one of the small squares. This is what makes the outer face of the assembled graph disjoint from the arc: a point of the arc is either inside one of the squares — and then separated from the outer face by that square's boundary cycle — or on one, and then it is a point of the graph.

The shape of lem:outer-chain this module expects to be handed

This is a note to the integrator, not a declaration. thm:arc-complement consumes the outer-chain lemma exactly once, and the form that makes the assembly short is the following. Γ : ℕ → Graph Plane Piece are the chain graphs, all subgraphs of one overlay graph G built from the concatenation of the squarePieces of every sample — so that "after subdividing common points into vertices" is discharged by construction rather than assumed, and so that all the Γ i are Graph.Compatible with each other for free (they share edge names because they share the ambient edge type Piece).

theorem outer_chain {k : ℕ} (hk : 3 ≤ k) (Γ : ℕ → Graph Plane Piece)
    (drawing : Piece → ℝ → Plane)
    (hfin : ∀ i < k, (Γ i).Finite)
    (hdraw : ∀ i < k, Graph.IsDrawing (Γ i) drawing)
    (h2c : ∀ i < k, (Γ i).IsTwoConnected)
    (hshare : ∀ i, i + 1 < k → ∃ a b : Plane, a ≠ b ∧
      a ∈ V(Γ i) ∧ a ∈ V(Γ (i+1)) ∧ b ∈ V(Γ i) ∧ b ∈ V(Γ (i+1)))
    (hfar : ∀ i j, i < k → j < k → i + 2 ≤ j →
      Disjoint (Graph.pointSet (Γ i) drawing) (Graph.pointSet (Γ j) drawing))
    {x : Plane}
    (houter : ∀ i, i + 1 < k → ¬ Bornology.IsBounded
      (Graph.face ((Γ i).union (Γ (i+1))) drawing x)) :
    ¬ Bornology.IsBounded (Graph.face (chainUnion Γ k) drawing x)

with chainUnion Γ k the fold of Graph.union over i < k, exported as a def with vertexSet / edgeSet / IsLink lemmas. Three things matter for the join:

• "outer face" must be stated as ¬ IsBounded (face …), not as face … = face … base for some chosen base point. Graph.exists_unbounded_face and Graph.unbounded_face_unique make the two equivalent, but the arc-complement proof gets its hypothesis from Graph.beyondSquare_subset_face applied to a containing square, which is naturally an unboundedness statement about x's own face.
• hshare must be about vertices, which is what exists_two_common_vertices and exists_two_cut_points + exists_overlayPiece_end_subset above deliver. Two common points would not compose with Graph.IsTwoConnected.union.
• hfar is about point sets, not vertex sets. The arc-complement proof gets it from exists_pos_dist_nonadjacent: nonadjacent samples are at distance ≥ δ while the squares have radius δ/4, so the two point sets are δ/2 apart.