The inner grid of the anchored square mesh: 2-connectivity and the outer cycle

Schoenflies/SquareMesh.lean delivers the geometry of prop:anchored-square-mesh — the diameter bound, the anchors, the inward edges at the fresh points, and connectedness of |T| ∖ S — and leaves two clauses open, both of them combinatorial:

• clause 5, the skeleton of T is 2-connected, is absent;
• clause 3 is proved only as a point-set equation, never as a cycle of the graph.

This module supplies both for the object the blueprint's own proof of the proposition is about: the rectangular grid. See "What this does and does not close" below for exactly what the integrator still has to do.

The grid, concretely

Two coordinate functions xc yc : ℕ → ℝ and two sizes m n : ℕ fix a grid: the vertices are the (m+1)(n+1) points gridPt xc yc i j = (xc i, yc j), the edges are the m(n+1) horizontal steps gridHEdge and the (m+1)n vertical steps gridVEdge. Everything is a def — an existentially quantified grid could not be refined against a second one, which is what Part II does.

The hypotheses on the coordinates are exactly as strong as each statement needs, and no stronger: 2-connectivity needs only that consecutive coordinates differ, the outer cycle needs the coordinates distinct (Set.InjOn xc (Set.Iic m)), and only the drawing — the clause that makes the grid a plane graph — needs them increasing (StrictMonoOn xc (Set.Iic m)).

The graph is pieceListGraph (gridEdges xc yc m n), where pieceListGraph is the general "a list of straight segments, read as a graph" constructor: an edge is a Piece, and it links exactly its two ends. pieceListGraph is overlayGraph without the subdivision — the vertices are the ends of the listed segments and nothing is cut — and its point is that pieceListGraph l₁ ∪ pieceListGraph l₂ = pieceListGraph (l₁ ++ l₂) on the nose (pieceListGraph_union), so that the blueprint's "add these finitely many cycles one at a time" is list concatenation and every union is an equation rather than an inclusion.

2-connectivity: two nested chains of lem:union-two-connected

The blueprint says "the inner grid is 2-connected by the same ear construction used for K". The ear construction is replaced here by two applications of Graph.IsTwoConnected.union, which is shorter and needs no ear at all:

• one cell — the boundary of a single rectangle of the grid — is a quadrilateral, and Graph.isTwoConnected_of_quad proves any quadrilateral 2-connected directly from the definition (delete a vertex; the other three are still a path);
• a strip (one column of cells) is the union of its cells, consecutive cells sharing the horizontal edge between them, hence two vertices;
• the grid is the union of its strips, consecutive strips sharing the whole vertical line between them, hence again two vertices.

Both chains need at least two vertices in common at every step, so both need 1 ≤ m and 1 ≤ n: a grid with a single row of points is a path and is not 2-connected. That is the degenerate case, and it is a hypothesis, not an oversight.

The outer cycle

The boundary walk goes once round the four sides, gridBoundaryEdge and gridBoundaryPt naming the 2m + 2n edges and vertices in order by a four-way if on the index. Everything about the walk is then arithmetic in ℕ, which omega decides. gridGraph_isCycleThrough_boundary is a Graph.IsCycleThrough of the grid graph — the distinguished outer cycle — and edgesCover_gridBoundary computes what it occupies: for increasing coordinates it is exactly the frame of the bounding rectangle, and for the grid on [-1,1]² that frame is modelCurve, i.e. S (edgesCover_gridBoundary_modelCurve, gridGraph_outer_cycle). That is the cycle thm:finite-transfer(b) asks for, in the form it asks for it.

The grid is also shown to be a plane graph (gridGraph_isDrawing), so the outer cycle is a Jordan curve (gridBoundary_isJordanCurve) and the whole face machinery applies to it.

What this does and does not close

Closed. Both clauses, for the rectangular grid, from an explicit construction, together with the drawing that makes the grid a plane graph.

Not closed. Neither clause is transported to Schoenflies.squareMesh, and the reason is structural, not a matter of effort: squareMesh is overlayGraph applied to a list of segments and an unspecified list of cut points obtained from exists_cut_points by choice. Its edges are therefore the pieces of a subdivision nobody can enumerate, so neither "the edges on S form a cycle" nor "the rings are cycles glued along the spokes" is available without first proving that the subdivision of a segment at a finite point set is a path — a theorem no module on main has. The honest statement of the missing collar step is Graph.IsTwoConnected.attach_cycles below: it takes a 2-connected hub K and finitely many 2-connected pieces each meeting K in two distinct vertices, and concludes for the union. Instantiating it at squareMesh needs the collar rectangles of the mesh as cycles, which is exactly the enumeration that is missing.

A degenerate case that would have to be excluded. squareMesh δ fresh anchors is not 2-connected when fresh has fewer than two distinct points, so the missing theorem cannot be stated without a hypothesis. With fresh = [] the mesh is meshCount δ pairwise disjoint concentric ring frames and is not even connected. With one fresh point z the spoke at z is the only thing joining the rings, so every vertex of that spoke is a cut vertex: deleting the one at radius k/N separates the rings inside it from the rings outside. Two fresh points are what make the rings and the two spokes a chain of quadrilaterals, which is the same picture the grid presents here. The corresponding hypothesis for the grid is 1 ≤ m and 1 ≤ n, and it is carried explicitly by every theorem below that needs it.

Blueprint

• prop:anchored-square-mesh, clause 5, for the inner grid — gridGraph_isTwoConnected.
• prop:anchored-square-mesh, clause 3, as a cycle — gridGraph_isCycleThrough_boundary together with edgesCover_gridBoundary, edgesCover_gridBoundary_modelCurve and the packaged gridGraph_outer_cycle.
• lem:polygonal-overlay, the drawing clause, for the grid — gridGraph_isDrawing.
• lem:union-two-connected — used through Graph.IsTwoConnected.union; iterated here as Graph.IsTwoConnected.attach_cycles, which is the blueprint's "adding these finitely many cycles one at a time".
• pieceListGraph, pieceListGraph_union — the list-of-segments graph, and the fact that its unions are concatenations.

A quadrilateral is 2-connected

The base case of both chains below. The blueprint reaches it through the ear decomposition (lem:subdivision-ear-preserve applied to a cycle); here it is read straight off the definition of Graph.IsTwoConnected, because a four-vertex graph is small enough that "delete one vertex and the rest is still connected" is four applications of one lemma.

theorem Graph.isTwoConnected_of_quad {α : Type u_1} {β : Type u_2} {G : Graph α β} {e₁ e₂ e₃ e₄ : β} {a b c d : α} (h₁ : G.IsLink e₁ a b) (h₂ : G.IsLink e₂ b c) (h₃ : G.IsLink e₃ c d) (h₄ : G.IsLink e₄ d a) (hV : ∀ v ∈ G.vertexSet, v = a ∨ v = b ∨ v = c ∨ v = d) (hab : a ≠ b) (hbc : b ≠ c) (hcd : c ≠ d) (hda : d ≠ a) (hac : a ≠ c) (hbd : b ≠ d) : G.IsTwoConnected

A four-cycle is 2-connected. No hypothesis on G beyond the four edges, the four distinct vertices, and the fact that there are no other vertices.

Attaching finitely many pieces to a 2-connected hub

prop:anchored-square-mesh: "The boundary of every collar rectangle is a cycle sharing with the inner grid at least the two endpoints of its inner boundary arc. Adding these finitely many cycles one at a time and applying lem:union-two-connected proves that the full mesh is 2-connected."

Graph.chainUnion_isTwoConnected (Schoenflies/OuterChain.lean) iterates the same lemma along a chain in which consecutive members meet. Here every piece meets the hub, which is what the collar rectangles do — each meets the inner grid, but two collar rectangles on opposite sides of the square meet nothing of each other. The two statements are independent; the integrator may want them beside each other.

def Graph.attachUnion {α : Type u_1} {β : Type u_2} (K : Graph α β) (Γ : ℕ → Graph α β) : ℕ → Graph α β

The hub K with the pieces Γ 0, …, Γ (m-1) glued on, one at a time.

Equations

• K.attachUnion Γ 0 = K
• K.attachUnion Γ m.succ = (K.attachUnion Γ m).union (Γ m)

@[simp]

theorem Graph.attachUnion_zero {α : Type u_1} {β : Type u_2} (K : Graph α β) (Γ : ℕ → Graph α β) : K.attachUnion Γ 0 = K

@[simp]

theorem Graph.attachUnion_succ {α : Type u_1} {β : Type u_2} (K : Graph α β) (Γ : ℕ → Graph α β) (m : ℕ) : K.attachUnion Γ (m + 1) = (K.attachUnion Γ m).union (Γ m)

theorem Graph.le_attachUnion {α : Type u_1} {β : Type u_2} (K : Graph α β) (Γ : ℕ → Graph α β) (m : ℕ) : K ≤ K.attachUnion Γ m

theorem Graph.attachUnion_le {α : Type u_1} {β : Type u_2} {G K : Graph α β} {Γ : ℕ → Graph α β} {m : ℕ} (hK : K ≤ G) (hΓ : ∀ q < m, Γ q ≤ G) : K.attachUnion Γ m ≤ G

theorem Graph.piece_le_attachUnion {α : Type u_1} {β : Type u_2} {G K : Graph α β} {Γ : ℕ → Graph α β} {m q : ℕ} (hK : K ≤ G) (hΓ : ∀ r < m, Γ r ≤ G) (hq : q < m) : Γ q ≤ K.attachUnion Γ m

theorem Graph.IsTwoConnected.attach_cycles {α : Type u_1} {β : Type u_2} {G K : Graph α β} {Γ : ℕ → Graph α β} {m : ℕ} (hK : K.IsTwoConnected) (hKG : K ≤ G) (hΓG : ∀ q < m, Γ q ≤ G) (hΓ : ∀ q < m, (Γ q).IsTwoConnected) (hmeet : ∀ q < m, ∃ (a : α) (b : α), a ≠ b ∧ a ∈ K.vertexSet ∧ a ∈ (Γ q).vertexSet ∧ b ∈ K.vertexSet ∧ b ∈ (Γ q).vertexSet) : (K.attachUnion Γ m).IsTwoConnected

lem:union-two-connected, iterated at a hub. A 2-connected K and finitely many 2-connected pieces, each meeting K in two distinct vertices, have 2-connected union.

A march along indices is a path

The boundary walk of the grid is a march: vertices p s, p (s+1), … joined by edges q s, q (s+1), …. The freshness clause of Graph.IsPath is then exactly the injectivity of p on the index range, because an edge of the chain is incident with nothing but its own two ends (Graph.Inc.eq_or_eq_of_isLink).

theorem Graph.isPath_range' {α : Type u_1} {β : Type u_2} {G : Graph α β} {p : ℕ → α} {q : ℕ → β} (k s : ℕ) : (∀ (i : ℕ), s ≤ i → i < s + k → G.IsLink (q i) (p i) (p (i + 1))) → (∀ (i j : ℕ), s ≤ i → i ≤ s + k → s ≤ j → j ≤ s + k → p i = p j → i = j) → p (s + k) ∈ G.vertexSet → G.IsPath (p s) (List.map q (List.range' s k)) (p (s + k))

A chain of edges through pairwise distinct vertices is a path.

The graph carried by a list of segments

overlayGraph subdivides; this does not. When the segments are already in general position — which for a grid they are, by construction — no subdivision is wanted, and what is gained is that unions are concatenations.

Schoenflies/ArcComplement.lean has the same construction indexed by a Set Piece, under the name segGraph, and pieceListGraph l is segGraph {P | P ∈ l}. The two were written in parallel and collided at merge; they are kept apart for now because this module's proofs run on the list and the other's on the set. If a third consumer appears, hoist the set version into Schoenflies/OverlayGraph.lean beside endSet and derive this one from it.

def Schoenflies.pieceListGraph (edges : List Piece) : Graph Plane Piece

The graph whose edges are the listed segments and whose vertices are their ends.

Equations

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

@[simp]

theorem Schoenflies.pieceListGraph_vertexSet (l : List Piece) : (pieceListGraph l).vertexSet = endSet l

@[simp]

theorem Schoenflies.pieceListGraph_mem_edgeSet {l : List Piece} {P : Piece} : P ∈ (pieceListGraph l).edgeSet ↔ P ∈ l

@[simp]

theorem Schoenflies.pieceListGraph_isLink {l : List Piece} {P : Piece} {x y : Plane} : (pieceListGraph l).IsLink P x y ↔ P ∈ l ∧ (x = P.1 ∧ y = P.2 ∨ x = P.2 ∧ y = P.1)

theorem Schoenflies.pieceListGraph_mem_vertexSet {l : List Piece} {v : Plane} : v ∈ (pieceListGraph l).vertexSet ↔ ∃ P ∈ l, v = P.1 ∨ v = P.2

theorem Schoenflies.pieceListGraph_isLink_self {l : List Piece} {P : Piece} (h : P ∈ l) : (pieceListGraph l).IsLink P P.1 P.2

The canonical link of a listed segment: it joins its own two ends.

theorem Schoenflies.mem_vertexSet_pieceListGraph_left {l : List Piece} {P : Piece} (h : P ∈ l) : P.1 ∈ (pieceListGraph l).vertexSet

theorem Schoenflies.mem_vertexSet_pieceListGraph_right {l : List Piece} {P : Piece} (h : P ∈ l) : P.2 ∈ (pieceListGraph l).vertexSet

theorem Schoenflies.pieceListGraph_inc {l : List Piece} {P : Piece} {v : Plane} (hP : P ∈ l) (h : v = P.1 ∨ v = P.2) : (pieceListGraph l).Inc P v

An end of a listed segment is incident with it.

theorem Schoenflies.plane_eq_of_coords {z w : Plane} (h0 : z.ofLp 0 = w.ofLp 0) (h1 : z.ofLp 1 = w.ofLp 1) : z = w

Two plane points with the same coordinates are equal.

Schoenflies.Plane.coord_ext in Schoenflies/JordanSeparates.lean is the same fact in a more general form; that module is not on this one's import path, and the integrator should collapse the two if it ever is.

theorem Schoenflies.endSet_append (l l' : List Piece) : endSet (l ++ l') = endSet l ∪ endSet l'

instance Schoenflies.pieceListGraph_finite (l : List Piece) : (pieceListGraph l).Finite

theorem Schoenflies.pieceListGraph_pointSet (l : List Piece) : (pieceListGraph l).pointSet segmentDrawing = cover l

What a segment graph occupies is what its segments occupy: every vertex is an end of a listed segment, so the vertices add nothing.

theorem Schoenflies.pieceListGraph_mono {l l' : List Piece} (h : l ⊆ l') : pieceListGraph l ≤ pieceListGraph l'

theorem Schoenflies.pieceListGraph_compatible (l l' : List Piece) : (pieceListGraph l).Compatible (pieceListGraph l')

Two segment graphs never disagree about a shared edge: an edge is its own pair of ends.

theorem Schoenflies.pieceListGraph_union (l l' : List Piece) : (pieceListGraph l).union (pieceListGraph l') = pieceListGraph (l ++ l')

The union of two segment graphs is the segment graph of the concatenation. This is the whole reason for pieceListGraph: it turns "glue one more cycle on" into an equation.

The rectangular grid

Two coordinate functions and two sizes. Nothing here asks the coordinates to be sorted: the combinatorics needs only that consecutive coordinates differ, which is exactly what makes each cell a genuine quadrilateral. Sortedness enters only with the geometry of the outer cycle.

def Schoenflies.gridPt (xc yc : ℕ → ℝ) (i j : ℕ) : Plane

The grid point with coordinate indices (i, j).

Equations

• Schoenflies.gridPt xc yc i j = Schoenflies.Plane.mk (xc i) (yc j)

def Schoenflies.gridHEdge (xc yc : ℕ → ℝ) (i j : ℕ) : Piece

The horizontal grid edge from (i, j) to (i+1, j).

Equations

• Schoenflies.gridHEdge xc yc i j = (Schoenflies.gridPt xc yc i j, Schoenflies.gridPt xc yc (i + 1) j)

def Schoenflies.gridVEdge (xc yc : ℕ → ℝ) (i j : ℕ) : Piece

The vertical grid edge from (i, j) to (i, j+1).

Equations

• Schoenflies.gridVEdge xc yc i j = (Schoenflies.gridPt xc yc i j, Schoenflies.gridPt xc yc i (j + 1))

theorem Schoenflies.gridPt_ne_of_fst {xc yc : ℕ → ℝ} {i i' j j' : ℕ} (h : xc i ≠ xc i') : gridPt xc yc i j ≠ gridPt xc yc i' j'

theorem Schoenflies.gridPt_ne_of_snd {xc yc : ℕ → ℝ} {i i' j j' : ℕ} (h : yc j ≠ yc j') : gridPt xc yc i j ≠ gridPt xc yc i' j'

def Schoenflies.cellEdges (xc yc : ℕ → ℝ) (i j : ℕ) : List Piece

The four sides of the cell whose lower-left corner is (i, j), listed bottom, right, top, left.

Equations

• Schoenflies.cellEdges xc yc i j = [Schoenflies.gridHEdge xc yc i j, Schoenflies.gridVEdge xc yc (i + 1) j, Schoenflies.gridHEdge xc yc i (j + 1), Schoenflies.gridVEdge xc yc i j]

def Schoenflies.stripEdges (xc yc : ℕ → ℝ) (i n : ℕ) : List Piece

One column of n cells, the cells (i, 0), …, (i, n-1).

Equations

• Schoenflies.stripEdges xc yc i n = List.flatMap (Schoenflies.cellEdges xc yc i) (List.range n)

def Schoenflies.gridEdges (xc yc : ℕ → ℝ) (m n : ℕ) : List Piece

The m × n grid: m columns of n cells.

Equations

• Schoenflies.gridEdges xc yc m n = List.flatMap (fun (i : ℕ) => Schoenflies.stripEdges xc yc i n) (List.range m)

def Schoenflies.gridGraph (xc yc : ℕ → ℝ) (m n : ℕ) : Graph Plane Piece

The grid graph: the m × n rectangular grid on the coordinates xc, yc, as a plane graph with straight edges.

Equations

• Schoenflies.gridGraph xc yc m n = Schoenflies.pieceListGraph (Schoenflies.gridEdges xc yc m n)

theorem Schoenflies.stripEdges_succ (xc yc : ℕ → ℝ) (i n : ℕ) : stripEdges xc yc i (n + 1) = stripEdges xc yc i n ++ cellEdges xc yc i n

theorem Schoenflies.stripEdges_one (xc yc : ℕ → ℝ) (i : ℕ) : stripEdges xc yc i 1 = cellEdges xc yc i 0

theorem Schoenflies.cellEdges_subset_stripEdges {xc yc : ℕ → ℝ} {i j n : ℕ} (h : j < n) : cellEdges xc yc i j ⊆ stripEdges xc yc i n

theorem Schoenflies.gridEdges_succ (xc yc : ℕ → ℝ) (m n : ℕ) : gridEdges xc yc (m + 1) n = gridEdges xc yc m n ++ stripEdges xc yc m n

theorem Schoenflies.gridEdges_one (xc yc : ℕ → ℝ) (n : ℕ) : gridEdges xc yc 1 n = stripEdges xc yc 0 n

theorem Schoenflies.stripEdges_subset_gridEdges {xc yc : ℕ → ℝ} {i m n : ℕ} (h : i < m) : stripEdges xc yc i n ⊆ gridEdges xc yc m n

The cell

theorem Schoenflies.cellGraph_isTwoConnected {xc yc : ℕ → ℝ} {i j : ℕ} (hx : xc i ≠ xc (i + 1)) (hy : yc j ≠ yc (j + 1)) : (pieceListGraph (cellEdges xc yc i j)).IsTwoConnected

One cell of the grid is 2-connected. Its boundary is a quadrilateral, so this is Graph.isTwoConnected_of_quad with the four corners named. Only the two consecutive-coordinate inequalities are used.

The strip, then the grid

Two chains of Graph.IsTwoConnected.union, and the two shared vertices are in each case the two ends of one edge that both parts contain.

theorem Schoenflies.stripGraph_isTwoConnected {xc yc : ℕ → ℝ} {i : ℕ} (hx : xc i ≠ xc (i + 1)) (k : ℕ) : (∀ j ≤ k, yc j ≠ yc (j + 1)) → (pieceListGraph (stripEdges xc yc i (k + 1))).IsTwoConnected

A column of cells is 2-connected. Consecutive cells share the horizontal edge between them, hence its two ends.

theorem Schoenflies.gridGraph_isTwoConnected_aux {xc yc : ℕ → ℝ} {n : ℕ} (hy : ∀ j ≤ n, yc j ≠ yc (j + 1)) (k : ℕ) : (∀ i ≤ k, xc i ≠ xc (i + 1)) → (pieceListGraph (gridEdges xc yc (k + 1) (n + 1))).IsTwoConnected

The grid is 2-connected. Each new column shares with what is already there the whole vertical line between them — in particular the two ends of its lowest edge.

The two size hypotheses are not decoration: a grid one point wide is a path, and a path is not 2-connected.

theorem Schoenflies.gridGraph_isTwoConnected {xc yc : ℕ → ℝ} {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (hx : ∀ i < m, xc i ≠ xc (i + 1)) (hy : ∀ j < n, yc j ≠ yc (j + 1)) : (gridGraph xc yc m n).IsTwoConnected

prop:anchored-square-mesh, clause 5, for the inner grid.

Which grid edges exist

Two membership lemmas, both by the same trick: a horizontal edge at height n is the top of a cell rather than the bottom of one, and a vertical edge on the line i = m is the right side of a cell rather than the left.

theorem Schoenflies.gridHEdge_mem_gridEdges {xc yc : ℕ → ℝ} {i j m n : ℕ} (hi : i < m) (hj : j ≤ n) (hn : 1 ≤ n) : gridHEdge xc yc i j ∈ gridEdges xc yc m n

theorem Schoenflies.gridVEdge_mem_gridEdges {xc yc : ℕ → ℝ} {i j m n : ℕ} (hi : i ≤ m) (hj : j < n) (hm : 1 ≤ m) : gridVEdge xc yc i j ∈ gridEdges xc yc m n

theorem Schoenflies.mem_gridEdges_iff {xc yc : ℕ → ℝ} {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) {P : Piece} : P ∈ gridEdges xc yc m n ↔ (∃ i < m, ∃ j ≤ n, P = gridHEdge xc yc i j) ∨ ∃ i ≤ m, ∃ j < n, P = gridVEdge xc yc i j

The edges of the grid, classified. A grid edge is a horizontal step in a row, or a vertical step in a column, and nothing else.

theorem Schoenflies.mem_vertexSet_gridGraph_iff {xc yc : ℕ → ℝ} {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) {v : Plane} : v ∈ (gridGraph xc yc m n).vertexSet ↔ ∃ i ≤ m, ∃ j ≤ n, v = gridPt xc yc i j

The vertices of the grid are exactly the grid points.

The outer cycle

The boundary of the grid, walked once anticlockwise from the corner (0,0): m steps right along the bottom, n up the right side, m back along the top, n down the left side. The walk is parametrised by an index t < 2m + 2n, and both the vertex and the edge at index t are given by a four-way if. Everything about the walk then reduces to arithmetic in ℕ, which omega decides; the geometry enters only in edgesCover_gridBoundary at the end.

def Schoenflies.bIdx (m n t : ℕ) : ℕ

The x-index of the t-th vertex of the boundary walk.

Equations

• Schoenflies.bIdx m n t = if t ≤ m then t else if t ≤ m + n then m else if t ≤ 2 * m + n then 2 * m + n - t else 0

def Schoenflies.bIdy (m n t : ℕ) : ℕ

The y-index of the t-th vertex of the boundary walk.

Equations

• Schoenflies.bIdy m n t = if t ≤ m then 0 else if t ≤ m + n then t - m else if t ≤ 2 * m + n then n else 2 * m + 2 * n - t

theorem Schoenflies.bIdx_le (m n t : ℕ) : bIdx m n t ≤ m

theorem Schoenflies.bIdy_le {m n t : ℕ} (h : t ≤ 2 * m + 2 * n) : bIdy m n t ≤ n

theorem Schoenflies.bIdx_bottom {m n t : ℕ} (h : t ≤ m) : bIdx m n t = t

theorem Schoenflies.bIdy_bottom {m n t : ℕ} (h : t ≤ m) : bIdy m n t = 0

theorem Schoenflies.bIdx_right {m n t : ℕ} (h₁ : m ≤ t) (h₂ : t ≤ m + n) : bIdx m n t = m

theorem Schoenflies.bIdy_right {m n t : ℕ} (h₁ : m ≤ t) (h₂ : t ≤ m + n) : bIdy m n t = t - m

theorem Schoenflies.bIdx_top {m n t : ℕ} (h₁ : m + n ≤ t) (h₂ : t ≤ 2 * m + n) : bIdx m n t = 2 * m + n - t

theorem Schoenflies.bIdy_top {m n t : ℕ} (h₁ : m + n ≤ t) (h₂ : t ≤ 2 * m + n) : bIdy m n t = n

theorem Schoenflies.bIdx_left {m n t : ℕ} (h₁ : 2 * m + n ≤ t) (_h₂ : t ≤ 2 * m + 2 * n) : bIdx m n t = 0

theorem Schoenflies.bIdy_left {m n t : ℕ} (h₁ : 2 * m + n ≤ t) (h₂ : t ≤ 2 * m + 2 * n) : bIdy m n t = 2 * m + 2 * n - t

theorem Schoenflies.bIdx_bIdy_inj {m n t s : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (ht : t < 2 * m + 2 * n) (hs : s < 2 * m + 2 * n) (h₁ : bIdx m n t = bIdx m n s) (h₂ : bIdy m n t = bIdy m n s) : t = s

The index pair determines the position on the walk. Pure arithmetic: the four sides overlap only at the corners, and there the two descriptions agree.

1 ≤ m and 1 ≤ n are needed and are not slack. With n = 0 the walk goes out along the bottom and comes back along the same row, so index t and index 2m - t name one point; this is the degenerate case in which the grid is a path rather than a cycle.

def Schoenflies.gridBoundaryPt (xc yc : ℕ → ℝ) (m n t : ℕ) : Plane

The t-th vertex of the boundary walk.

Equations

• Schoenflies.gridBoundaryPt xc yc m n t = Schoenflies.gridPt xc yc (Schoenflies.bIdx m n t) (Schoenflies.bIdy m n t)

def Schoenflies.gridBoundaryEdge (xc yc : ℕ → ℝ) (m n t : ℕ) : Piece

The t-th edge of the boundary walk.

Equations

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

theorem Schoenflies.gridBoundaryPt_wrap (xc yc : ℕ → ℝ) (m n : ℕ) : gridBoundaryPt xc yc m n (2 * m + 2 * n) = gridBoundaryPt xc yc m n 0

The walk closes up: index 2m + 2n is the corner it started from.

theorem Schoenflies.gridBoundaryPt_inj {xc yc : ℕ → ℝ} {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (hx : Set.InjOn xc (Set.Iic m)) (hy : Set.InjOn yc (Set.Iic n)) {t s : ℕ} (ht : t < 2 * m + 2 * n) (hs : s < 2 * m + 2 * n) (h : gridBoundaryPt xc yc m n t = gridBoundaryPt xc yc m n s) : t = s

The vertices of the boundary walk are pairwise distinct.

theorem Schoenflies.gridBoundary_isLink {xc yc : ℕ → ℝ} {m n t : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (ht : t < 2 * m + 2 * n) : (gridGraph xc yc m n).IsLink (gridBoundaryEdge xc yc m n t) (gridBoundaryPt xc yc m n t) (gridBoundaryPt xc yc m n (t + 1))

Each step of the boundary walk is an edge of the grid, joining the two vertices it should.

def Schoenflies.gridBoundaryDetour (xc yc : ℕ → ℝ) (m n : ℕ) : List Piece

The detour: all the boundary edges but the last.

Equations

• Schoenflies.gridBoundaryDetour xc yc m n = List.map (Schoenflies.gridBoundaryEdge xc yc m n) (List.range' 0 (2 * m + 2 * n - 1))

def Schoenflies.gridBoundaryLast (xc yc : ℕ → ℝ) (m n : ℕ) : Piece

The last boundary edge, which closes the cycle.

Equations

• Schoenflies.gridBoundaryLast xc yc m n = Schoenflies.gridBoundaryEdge xc yc m n (2 * m + 2 * n - 1)

theorem Schoenflies.gridGraph_isCycleThrough_boundary {xc yc : ℕ → ℝ} {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (hx : Set.InjOn xc (Set.Iic m)) (hy : Set.InjOn yc (Set.Iic n)) : (gridGraph xc yc m n).IsCycleThrough (gridBoundaryLast xc yc m n) (gridBoundaryPt xc yc m n 0) (gridBoundaryPt xc yc m n (2 * m + 2 * n - 1)) (gridBoundaryDetour xc yc m n)

prop:anchored-square-mesh, clause 3, as a cycle. The boundary of the grid is a cycle of the grid graph — not merely a point set.

What the outer cycle occupies

Up to here nothing has been asked of the order of the coordinates. It is asked now: the union of the boundary edges is the frame of the bounding rectangle only if the coordinates increase, and the proof is the one-dimensional fact Set.Icc_union_Icc_eq_Icc transported along Schoenflies.mem_segment_horiz / mem_segment_vert.

theorem Schoenflies.gridBoundaryEdge_bottom {xc yc : ℕ → ℝ} {m n i : ℕ} (h : i < m) : gridBoundaryEdge xc yc m n i = gridHEdge xc yc i 0

theorem Schoenflies.gridBoundaryEdge_right {xc yc : ℕ → ℝ} {m n j : ℕ} (h : j < n) : gridBoundaryEdge xc yc m n (m + j) = gridVEdge xc yc m j

theorem Schoenflies.gridBoundaryEdge_top {xc yc : ℕ → ℝ} {m n i : ℕ} (hn : 1 ≤ n) (h : i < m) : gridBoundaryEdge xc yc m n (2 * m + n - 1 - i) = gridHEdge xc yc i n

theorem Schoenflies.gridBoundaryEdge_left {xc yc : ℕ → ℝ} {m n j : ℕ} (h : j < n) : gridBoundaryEdge xc yc m n (2 * m + 2 * n - 1 - j) = gridVEdge xc yc 0 j

theorem Schoenflies.edgesCover_gridBoundary_eq_iUnion (xc yc : ℕ → ℝ) {m n : ℕ} (hL : 1 ≤ 2 * m + 2 * n) : Graph.edgesCover segmentDrawing (gridBoundaryLast xc yc m n :: gridBoundaryDetour xc yc m n) = ⋃ t ∈ Set.Iio (2 * m + 2 * n), (gridBoundaryEdge xc yc m n t).seg

The realisation of the cycle is the union of the boundary edges, indexed by position on the walk.

theorem Schoenflies.iUnion_gridBoundaryEdge (xc yc : ℕ → ℝ) {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) : ⋃ t ∈ Set.Iio (2 * m + 2 * n), (gridBoundaryEdge xc yc m n t).seg = ((⋃ i ∈ Set.Iio m, (gridHEdge xc yc i 0).seg) ∪ ⋃ j ∈ Set.Iio n, (gridVEdge xc yc m j).seg) ∪ ((⋃ i ∈ Set.Iio m, (gridHEdge xc yc i n).seg) ∪ ⋃ j ∈ Set.Iio n, (gridVEdge xc yc 0 j).seg)

The boundary edges, sorted into the four sides.

Consecutive intervals

theorem Schoenflies.chain_le_of_le {f : ℕ → ℝ} {m : ℕ} (h : ∀ i < m, f i ≤ f (i + 1)) (a b : ℕ) : a ≤ b → b ≤ m → f a ≤ f b

theorem Schoenflies.iUnion_Icc_chain {f : ℕ → ℝ} (m : ℕ) : 1 ≤ m → (∀ i < m, f i ≤ f (i + 1)) → ⋃ i ∈ Set.Iio m, Set.Icc (f i) (f (i + 1)) = Set.Icc (f 0) (f m)

theorem Schoenflies.iUnion_gridHEdge_seg {xc yc : ℕ → ℝ} {m : ℕ} (hm : 1 ≤ m) (hmono : ∀ i < m, xc i ≤ xc (i + 1)) (j : ℕ) : ⋃ i ∈ Set.Iio m, (gridHEdge xc yc i j).seg = segment ℝ (gridPt xc yc 0 j) (gridPt xc yc m j)

A run of horizontal grid edges occupies the whole horizontal segment.

theorem Schoenflies.iUnion_gridVEdge_seg {xc yc : ℕ → ℝ} {n : ℕ} (hn : 1 ≤ n) (hmono : ∀ j < n, yc j ≤ yc (j + 1)) (i : ℕ) : ⋃ j ∈ Set.Iio n, (gridVEdge xc yc i j).seg = segment ℝ (gridPt xc yc i 0) (gridPt xc yc i n)

A run of vertical grid edges occupies the whole vertical segment.

theorem Schoenflies.edgesCover_gridBoundary {xc yc : ℕ → ℝ} {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (hxmono : ∀ i < m, xc i ≤ xc (i + 1)) (hymono : ∀ j < n, yc j ≤ yc (j + 1)) : Graph.edgesCover segmentDrawing (gridBoundaryLast xc yc m n :: gridBoundaryDetour xc yc m n) = segment ℝ (gridPt xc yc 0 0) (gridPt xc yc m 0) ∪ segment ℝ (gridPt xc yc m 0) (gridPt xc yc m n) ∪ (segment ℝ (gridPt xc yc 0 n) (gridPt xc yc m n) ∪ segment ℝ (gridPt xc yc 0 0) (gridPt xc yc 0 n))

What the outer cycle occupies: the frame of the bounding rectangle, as the union of its four sides.

theorem Schoenflies.edgesCover_gridBoundary_modelCurve {xc yc : ℕ → ℝ} {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (hxmono : ∀ i < m, xc i ≤ xc (i + 1)) (hymono : ∀ j < n, yc j ≤ yc (j + 1)) (hx0 : xc 0 = -1) (hxm : xc m = 1) (hy0 : yc 0 = -1) (hyn : yc n = 1) : Graph.edgesCover segmentDrawing (gridBoundaryLast xc yc m n :: gridBoundaryDetour xc yc m n) = modelCurve

The outer cycle of a grid on [-1,1]² occupies exactly S. This is the missing half of prop:anchored-square-mesh clause 3: not "the edges lying on S cover S", but "S is the realisation of a distinguished cycle of the graph", which is the form thm:finite-transfer(b) consumes.

theorem Schoenflies.gridGraph_outer_cycle {xc yc : ℕ → ℝ} {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (hx : Set.InjOn xc (Set.Iic m)) (hy : Set.InjOn yc (Set.Iic n)) (hxmono : ∀ i < m, xc i ≤ xc (i + 1)) (hymono : ∀ j < n, yc j ≤ yc (j + 1)) (hx0 : xc 0 = -1) (hxm : xc m = 1) (hy0 : yc 0 = -1) (hyn : yc n = 1) : (gridGraph xc yc m n).IsCycleThrough (gridBoundaryLast xc yc m n) (gridBoundaryPt xc yc m n 0) (gridBoundaryPt xc yc m n (2 * m + 2 * n - 1)) (gridBoundaryDetour xc yc m n) ∧ Graph.edgesCover segmentDrawing (gridBoundaryLast xc yc m n :: gridBoundaryDetour xc yc m n) = modelCurve

The distinguished outer cycle of the grid on [-1,1]², both halves at once: it is a cycle of the grid graph, and what it occupies is S.

The grid is a plane graph

Sorted coordinates make the drawing clause a coordinate computation. A point of a horizontal grid edge has the row's y-coordinate and an x-coordinate in one closed coordinate interval; strict monotonicity turns "xc a lies in [xc i, xc (i+1)]" into "a = i or a = i+1", and that single step settles both remaining clauses of Graph.IsDrawing.

theorem Schoenflies.coord_le_of_idx_le {f : ℕ → ℝ} {N : ℕ} (hf : StrictMonoOn f (Set.Iic N)) {a b : ℕ} (ha : a ≤ N) (hb : b ≤ N) (h : a ≤ b) : f a ≤ f b

theorem Schoenflies.idx_le_of_coord_le {f : ℕ → ℝ} {N : ℕ} (hf : StrictMonoOn f (Set.Iic N)) {a b : ℕ} (ha : a ≤ N) (hb : b ≤ N) (h : f a ≤ f b) : a ≤ b

theorem Schoenflies.idx_of_coord_mem {f : ℕ → ℝ} {N : ℕ} (hf : StrictMonoOn f (Set.Iic N)) {a i : ℕ} (ha : a ≤ N) (hi : i + 1 ≤ N) (h₁ : f i ≤ f a) (h₂ : f a ≤ f (i + 1)) : a = i ∨ a = i + 1

Reading an index off a coordinate.

theorem Schoenflies.mem_gridHEdge_seg_iff {xc yc : ℕ → ℝ} {i j : ℕ} {z : Plane} : z ∈ (gridHEdge xc yc i j).seg ↔ z.ofLp 1 = yc j ∧ z.ofLp 0 ∈ segment ℝ (xc i) (xc (i + 1))

theorem Schoenflies.mem_gridVEdge_seg_iff {xc yc : ℕ → ℝ} {i j : ℕ} {z : Plane} : z ∈ (gridVEdge xc yc i j).seg ↔ z.ofLp 0 = xc i ∧ z.ofLp 1 ∈ segment ℝ (yc j) (yc (j + 1))

theorem Schoenflies.gridEdges_nondeg {xc yc : ℕ → ℝ} {m n : ℕ} (hxs : StrictMonoOn xc (Set.Iic m)) (hys : StrictMonoOn yc (Set.Iic n)) (hm : 1 ≤ m) (hn : 1 ≤ n) {P : Piece} (hP : P ∈ gridEdges xc yc m n) : P.Nondeg

A grid edge is nondegenerate: its two ends differ in one coordinate.

theorem Schoenflies.end_of_gridPt_mem_seg {xc yc : ℕ → ℝ} {m n : ℕ} (hxs : StrictMonoOn xc (Set.Iic m)) (hys : StrictMonoOn yc (Set.Iic n)) (hm : 1 ≤ m) (hn : 1 ≤ n) {P : Piece} (hP : P ∈ gridEdges xc yc m n) {a b : ℕ} (ha : a ≤ m) (hb : b ≤ n) (hmem : gridPt xc yc a b ∈ P.seg) : gridPt xc yc a b = P.1 ∨ gridPt xc yc a b = P.2

A grid point on a grid edge is one of that edge's two ends.

theorem Schoenflies.gridPt_of_mem_two_edges {xc yc : ℕ → ℝ} {m n : ℕ} (hxs : StrictMonoOn xc (Set.Iic m)) (hys : StrictMonoOn yc (Set.Iic n)) (hm : 1 ≤ m) (hn : 1 ≤ n) {P Q : Piece} (hP : P ∈ gridEdges xc yc m n) (hQ : Q ∈ gridEdges xc yc m n) (hPQ : P ≠ Q) {z : Plane} (hzP : z ∈ P.seg) (hzQ : z ∈ Q.seg) : ∃ a ≤ m, ∃ b ≤ n, z = gridPt xc yc a b

A point on two grid edges is a grid point on both. The heart of the drawing clause: two grid segments cross only where a coordinate of one is pinned by the other.

theorem Schoenflies.gridGraph_isDrawing {xc yc : ℕ → ℝ} {m n : ℕ} (hxs : StrictMonoOn xc (Set.Iic m)) (hys : StrictMonoOn yc (Set.Iic n)) (hm : 1 ≤ m) (hn : 1 ≤ n) : (gridGraph xc yc m n).IsDrawing segmentDrawing

The grid is a plane graph, drawn with straight edges.

theorem Schoenflies.gridBoundary_isJordanCurve {xc yc : ℕ → ℝ} {m n : ℕ} (hxs : StrictMonoOn xc (Set.Iic m)) (hys : StrictMonoOn yc (Set.Iic n)) (hm : 1 ≤ m) (hn : 1 ≤ n) : IsJordanCurve (Graph.edgesCover segmentDrawing (gridBoundaryLast xc yc m n :: gridBoundaryDetour xc yc m n))

The outer cycle is a Jordan curve. Now that the grid is a plane graph this is Graph.IsDrawing.cycle_isJordanCurve applied to the boundary cycle.