The anchored square mesh: the three gaps an audit found

Schoenflies/SquareMesh.lean and Schoenflies/SquareMeshConnected.lean deliver prop:anchored-square-mesh between them. An adversarial audit of the second found three real gaps; this module closes what can be closed and states, as explicit hypotheses, what cannot.

Gap 3 — the dropped subdivision step

The blueprint proves the inner grid 2-connected "by the same ear construction used for K, together with lem:subdivision-ear-preserve". SquareMeshConnected.gridGraph_isTwoConnected supplies the ear half (as a chain of Graph.IsTwoConnected.unions) and drops the subdivision half entirely — yet the mesh subdivides the grid, at the four corners of the inner square, at every point λ zᵢ, and at every crossing the overlay finds. A grid that is 2-connected before subdivision and unproved after it is of no use to the proposition.

pieceListGraph_subdivide_isTwoConnected is the missing half, in the vocabulary of Schoenflies/Subdivide.lean: subdividing a list of segments whose graph is 2-connected, at any list of points that cut it cleanly (CleanCut: each point interior to at most one segment, and interior to none once it is an end of one), leaves the graph 2-connected. It is Graph.IsTwoConnected.replace_edge_by_path — lem:subdivision-ear-preserve (a) — iterated, with the two-edge replacement path built by isPathGraph_pair.

For a grid the cleanliness hypothesis is free: two distinct grid edges meet only at a grid point, and a grid point interior to a grid edge does not exist. So gridGraph_subdivide_isTwoConnected has no hypothesis on the points at all.

Gap 2 — the outer cycle was instantiated at the wrong square

SquareMeshConnected.edgesCover_gridBoundary_modelCurve pins the grid to xc 0 = -1, xc m = 1, yc 0 = -1, yc n = 1: a grid spanning all of Q, whose boundary cycle is S. The audit says such a grid cannot be the mesh, and it is right. The obstruction is gridGraph_full_square_aligned_ends below: for 0 < i < m the two grid points (xc i, -1) and (xc i, 1) both lie on S and both carry an internal edge — the vertical edges at the bottom and top of the column i — neither of which lies on S. Clause 3 of the proposition then demands that both be fresh points of u(𝒜), and clause 2 demands a grid line through every old boundary vertex, which manufactures such a pair on the opposite side. Nothing about u(𝒜) supplies pairs of points with a common coordinate: it is merely dense. The theorem is true; the instantiation is wrong.

The blueprint's grid fills the inner square λQ, λ < 1, which touches S nowhere; edgesCover_gridBoundary_ringSet is the corrected statement — the boundary cycle of a grid on [-r, r]² occupies ringSet r — and gridGraph_inner_cycle packages it with the disjointness from S that makes the freshness clauses vacuous for the grid.

Gap 1 — nothing was proved about squareMesh itself

squareMesh δ fresh anchors is overlayGraph applied to the mesh segments and to a list of cut points obtained from exists_cut_points by choice. Its edges are the pieces of a subdivision nobody can enumerate, so no clause about its combinatorics follows from the grid results, which are about a different graph.

One general fact about overlayGraph is missing, and it is stated here as the explicit hypothesis SubdividesToPath: the overlay edges lying inside a source segment are exactly the edges of a path of the overlay from one end of that segment to the other. That is a statement about Schoenflies.overlayGraph and Schoenflies.subdivide alone — believed, and dischargeable, since the pieces of the subdivision of a segment have pairwise disjoint interiors and cover it, so the distance from one end orders them into a chain. It is not a restatement of any goal here: the whole content below is the assembly, which the hypothesis does not contain.

From it:

• meshGraph_outer_cycle / squareMesh_outer_cycle_of_subdividesToPath — clause 3 as a cycle, for the mesh itself. The four sides of the outer ring are four overlay paths; three concatenations (Graph.IsPath.append_of_disjoint) glue them into one path once round S, and the first step of the reversed fourth side is peeled off to close the cycle. The result is a Graph.IsLongCycle of the mesh whose edges occupy exactly modelCurve.
• squareMesh_outer_cycleGraph_isTwoConnected_of_subdividesToPath — hence the outer ring is a 2-connected subgraph of the mesh, which is the first step of the blueprint's assembly of clause 5.

Full 2-connectivity of squareMesh is NOT proved here, and is not assumed either. What remains is the rest of that assembly: the inner rings as cycles (the same argument, with ringPieces r in place of ringPieces 1), the crossing points r • z as vertices (which needs the MeetsAreCut clause of meshPoints), and then each spoke segment between consecutive rings attached as an ear — for which one also needs the two arcs of an already-built cycle between two of its vertices. None of that is short.

The degeneracy the audit asked about is settled, with a proof rather than an assertion: not_isTwoConnected_squareMesh_of_fresh_nil. With no fresh point the mesh is meshCount δ ≥ 2 disjoint concentric frames and is not even connected, so clause 5 is false as stated for squareMesh δ [] anchors. With exactly one fresh point it is connected but every interior vertex of the single spoke is a cut vertex; that case is discussed in the section docstring and not formalised. Every statement of clause 5 for the mesh must therefore carry a hypothesis giving two distinct fresh points.

Blueprint

• lem:subdivision-ear-preserve — isPathGraph_pair, pieceListGraph_splitAllAt_eq, pieceListGraph_splitAllAt_isTwoConnected, pieceListGraph_subdivide_isTwoConnected.
• prop:anchored-square-mesh, clause 5 for the inner grid, after subdivision — gridGraph_subdivide_isTwoConnected.
• prop:anchored-square-mesh, clause 3 for the inner grid at the right radius — edgesCover_gridBoundary_ringSet, gridGraph_inner_cycle.
• prop:anchored-square-mesh, clauses 3 and 4, the obstruction to a grid on all of Q — gridGraph_full_square_aligned_ends.
• prop:anchored-square-mesh, clause 3 as a cycle, for the mesh — SubdividesToPath, meshGraph_outer_cycle, squareMesh_outer_cycle_of_subdividesToPath.
• prop:anchored-square-mesh, clause 5, the first step for the mesh and the degenerate case — squareMesh_outer_cycleGraph_isTwoConnected_of_subdividesToPath, not_isTwoConnected_squareMesh_of_fresh_nil.
• lem:union-two-connected is not used here; the assembly that would use it is the part left open.

A two-edge path graph

The replacement path of a single subdivision: one new vertex q between the two ends of the segment being cut. Graph.IsTwoConnected.replace_edge_by_path takes a path of any length, so this is the only shape needed.

theorem Schoenflies.pieceListGraph_inc_iff {l : List Piece} {P : Piece} {v : Plane} : (pieceListGraph l).Inc P v ↔ P ∈ l ∧ (v = P.1 ∨ v = P.2)

theorem Schoenflies.endSet_pair (a q b : Plane) : endSet [(a, q), (q, b)] = {a, q, b}

theorem Schoenflies.coveredVertices_pair (a q b : Plane) : (pieceListGraph [(a, q), (q, b)]).coveredVertices [(a, q), (q, b)] = {a, q, b}

theorem Schoenflies.isPathGraph_pair {a q b : Plane} (haq : a ≠ q) (hqb : q ≠ b) (hab : a ≠ b) : (pieceListGraph [(a, q), (q, b)]).IsPathGraph a [(a, q), (q, b)] b

The two halves of a cut segment form a path graph.

Cutting a list of segments cleanly

splitAllAt q l cuts every piece of l that has q in its interior. To read the result as one subdivision of one edge — which is what lem:subdivision-ear-preserve is about — the point must be interior to at most one piece; and to keep the replacement path's middle vertex new, the point must not already be an end. A point that is interior to no piece cuts nothing at all, and is harmless.

def Schoenflies.CleanCut (l : List Piece) (q : Plane) : Prop

q cuts the list l cleanly: it is interior to at most one piece, and either it is interior to none or it is an end of none.

Both branches of the disjunction occur in the intended use: a point of the cut list that has already been cut out is interior to nothing, and a point not yet used is an end of nothing.

Equations

• Schoenflies.CleanCut l q = ((∀ R ∈ l, ∀ S ∈ l, q ∈ R.interior → q ∈ S.interior → R = S) ∧ ((∀ R ∈ l, q ∉ R.interior) ∨ q ∉ Schoenflies.endSet l))

theorem Schoenflies.CleanCut.of_no_interior {l : List Piece} {q : Plane} (h : ∀ R ∈ l, q ∉ R.interior) : CleanCut l q

theorem Schoenflies.openSegment_halves_disjoint {a b p x : Plane} (hab : a ≠ b) (hp : p ∈ openSegment ℝ a b) (h₁ : x ∈ openSegment ℝ a p) (h₂ : x ∈ openSegment ℝ p b) : False

The two halves of a cut segment have disjoint interiors. The distance from the left end is a faithful coordinate along the segment (Schoenflies/SegmentOrder.lean), and it is < dist a p on one half and > dist a p on the other.

theorem Schoenflies.splitAllAt_eq_self {l : List Piece} {q : Plane} (h : ∀ R ∈ l, q ∉ R.interior) : splitAllAt q l = l

Splitting at a point that is interior to nothing changes the list not at all.

theorem Schoenflies.mem_splitAllAt_iff {l : List Piece} {P R : Piece} {q : Plane} (hP : P ∈ l) (hq : q ∈ P.interior) (huniq : ∀ S ∈ l, q ∈ S.interior → S = P) : R ∈ splitAllAt q l ↔ R ∈ l ∧ R ≠ P ∨ R ∈ [(P.1, q), (q, P.2)]

The members of a split list: everything but the cut piece, and the cut piece's two halves.

theorem Schoenflies.endSet_splitAllAt {l : List Piece} {P : Piece} {q : Plane} (hP : P ∈ l) (hq : q ∈ P.interior) (huniq : ∀ S ∈ l, q ∈ S.interior → S = P) : endSet (splitAllAt q l) = endSet l ∪ {q}

The ends of a split list: the old ends and the cut point.

theorem Schoenflies.pieceListGraph_splitAllAt_eq {l : List Piece} {P : Piece} {q : Plane} (hP : P ∈ l) (hq : q ∈ P.interior) (huniq : ∀ S ∈ l, q ∈ S.interior → S = P) : pieceListGraph (splitAllAt q l) = ((pieceListGraph l).deleteEdges {P}).union (pieceListGraph [(P.1, q), (q, P.2)])

One cut, as a replacement of one edge by a two-edge path.

theorem Schoenflies.pieceListGraph_splitAllAt_isTwoConnected {l : List Piece} {P : Piece} {q : Plane} (hP : P ∈ l) (hnd : P.Nondeg) (hq : q ∈ P.interior) (huniq : ∀ S ∈ l, q ∈ S.interior → S = P) (hnew : q ∉ endSet l) (h2 : (pieceListGraph l).IsTwoConnected) : (pieceListGraph (splitAllAt q l)).IsTwoConnected

lem:subdivision-ear-preserve, one cut. Cutting one segment of a 2-connected list of segments at an interior point that is interior to no other segment and is an end of none leaves the graph 2-connected.

theorem Schoenflies.CleanCut.splitAllAt {l : List Piece} {q q' : Plane} (hnd : ∀ R ∈ l, R.Nondeg) (hq : CleanCut l q) (hq' : CleanCut l q') : CleanCut (Schoenflies.splitAllAt q' l) q

Cleanliness survives a cut: interiors only shrink, and the only new end is the cut point — which, after its own cut, is interior to nothing.

theorem Schoenflies.pieceListGraph_subdivide_isTwoConnected (points : List Plane) (l : List Piece) : (∀ P ∈ l, P.Nondeg) → (∀ q ∈ points, CleanCut l q) → (pieceListGraph l).IsTwoConnected → (pieceListGraph (subdivide l points)).IsTwoConnected

lem:subdivision-ear-preserve, the whole subdivision. A list of segments whose graph is 2-connected, subdivided at any list of points that cut it cleanly, still has a 2-connected graph.

This is the half of the blueprint's inner-grid argument that Schoenflies/SquareMeshConnected.lean dropped.

The inner grid, subdivided

For a grid the cleanliness hypothesis costs nothing. Two distinct grid edges meet only at a grid point (gridPt_of_mem_two_edges), a grid point on a grid edge is an end of it (end_of_gridPt_mem_seg), and an end of a nondegenerate segment is not interior to it. So every point cuts the grid cleanly, and the subdivision theorem applies with no hypothesis on the cut points at all.

theorem Schoenflies.notMem_interior_of_end {R : Piece} (hnd : R.Nondeg) {q : Plane} (h : q = R.1 ∨ q = R.2) : q ∉ R.interior

An end of a nondegenerate segment is not interior to it.

theorem Schoenflies.cleanCut_gridEdges {xc yc : ℕ → ℝ} {m n : ℕ} (hxs : StrictMonoOn xc (Set.Iic m)) (hys : StrictMonoOn yc (Set.Iic n)) (hm : 1 ≤ m) (hn : 1 ≤ n) (q : Plane) : CleanCut (gridEdges xc yc m n) q

Every point cuts the grid cleanly.

theorem Schoenflies.gridGraph_subdivide_isTwoConnected {xc yc : ℕ → ℝ} {m n : ℕ} (hxs : StrictMonoOn xc (Set.Iic m)) (hys : StrictMonoOn yc (Set.Iic n)) (hm : 1 ≤ m) (hn : 1 ≤ n) (points : List Plane) : (pieceListGraph (subdivide (gridEdges xc yc m n) points)).IsTwoConnected

prop:anchored-square-mesh, clause 5 for the inner grid, after subdivision. This is the half of the blueprint's argument — lem:subdivision-ear-preserve — that Schoenflies/SquareMeshConnected.lean dropped. It needs nothing of the cut points: the grid is in general position with itself, so any list of points cuts it cleanly.

The outer cycle of the inner grid, at the right radius

SquareMeshConnected.edgesCover_gridBoundary_modelCurve is the r = 1 case of the theorem below, and r = 1 is exactly the case the mesh cannot use. See the module docstring, and gridGraph_full_square_aligned_ends for the obstruction made explicit.

theorem Schoenflies.edgesCover_gridBoundary_ringSet {xc yc : ℕ → ℝ} {m n : ℕ} {r : ℝ} (hr : 0 ≤ r) (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 = -r) (hxm : xc m = r) (hy0 : yc 0 = -r) (hyn : yc n = r) : Graph.edgesCover segmentDrawing (gridBoundaryLast xc yc m n :: gridBoundaryDetour xc yc m n) = ringSet r

What the grid's outer cycle occupies, at any radius. For a grid on [-r, r]² the boundary cycle occupies the frame ringSet r. The blueprint's inner grid is the case r = λ < 1, and then the cycle misses S entirely.

theorem Schoenflies.gridGraph_inner_cycle {xc yc : ℕ → ℝ} {m n : ℕ} {r : ℝ} (hr : 0 ≤ r) (hr1 : r ≠ 1) (hm : 1 ≤ m) (hn : 1 ≤ n) (hxs : StrictMonoOn xc (Set.Iic m)) (hys : StrictMonoOn yc (Set.Iic n)) (hx0 : xc 0 = -r) (hxm : xc m = r) (hy0 : yc 0 = -r) (hyn : yc n = r) : (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) = ringSet r ∧ Graph.edgesCover segmentDrawing (gridBoundaryLast xc yc m n :: gridBoundaryDetour xc yc m n) ∩ modelCurve = ∅

The distinguished cycle of the blueprint's inner grid. The grid fills λQ for some 0 ≤ λ < 1; its boundary is a cycle of the grid graph, occupies the frame of λQ, and misses S. The last clause is why the inner grid is exempt from the mesh's freshness clauses 3 and 4: no edge of it reaches S at all.

Why the grid may not span all of Q

The audit's second finding, made explicit.

theorem Schoenflies.mem_modelCurve_of_supNorm {z : Plane} (h : z.supNorm = 1) : z ∈ modelCurve

theorem Schoenflies.supNorm_mk (a b : ℝ) : (Plane.mk a b).supNorm = max |a| |b|

theorem Schoenflies.gridVEdge_not_subset_modelCurve {xc yc : ℕ → ℝ} {i j : ℕ} (hxi : |xc i| < 1) (h1 : -1 ≤ yc j) (h2 : yc (j + 1) ≤ 1) (hlt : yc j < yc (j + 1)) : ¬(gridVEdge xc yc i j).seg ⊆ modelCurve

A vertical grid edge inside the open strip |x| < 1 and inside |y| ≤ 1 does not lie on S: its midpoint has sup norm < 1.

theorem Schoenflies.gridGraph_full_square_aligned_ends {xc yc : ℕ → ℝ} {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (hxs : StrictMonoOn xc (Set.Iic m)) (hys : StrictMonoOn yc (Set.Iic n)) (hx0 : xc 0 = -1) (hxm : xc m = 1) (hy0 : yc 0 = -1) (hyn : yc n = 1) {i : ℕ} (hi0 : 0 < i) (him : i < m) : gridPt xc yc i 0 ∈ modelCurve ∧ gridPt xc yc i n ∈ modelCurve ∧ (gridPt xc yc i 0).ofLp 0 = (gridPt xc yc i n).ofLp 0 ∧ (∃ P ∈ (gridGraph xc yc m n).edgeSet, (gridPt xc yc i 0 = P.1 ∨ gridPt xc yc i 0 = P.2) ∧ ¬P.seg ⊆ modelCurve) ∧ ∃ P ∈ (gridGraph xc yc m n).edgeSet, (gridPt xc yc i n = P.1 ∨ gridPt xc yc i n = P.2) ∧ ¬P.seg ⊆ modelCurve

The obstruction to a grid spanning all of Q. For a strictly increasing grid on [-1,1]² and any interior column 0 < i < m, the two grid points (xc i, -1) and (xc i, 1) both lie on S, they share their first coordinate, and each is an end of a grid edge that does not lie on S.

Clause 3 of prop:anchored-square-mesh says every internal edge meeting S ends at a fresh point of u(𝒜). Applied to such a grid it therefore demands that u(𝒜) contain both points of a vertically aligned pair, for every interior column — and, by the same argument on rows, for every interior row. Density of u(𝒜) in S supplies no aligned pair, and clause 2 makes the demand unavoidable: an old boundary vertex on the bottom side forces a coordinate xc i, and that coordinate forces the point (xc i, 1) opposite it.

The blueprint's grid therefore fills the inner square λQ with λ < 1, where the clauses are vacuous by gridGraph_inner_cycle; the collar between λQ and S, not the grid, carries the fresh points and their single spokes.

The mesh needs at least two fresh points

The audit asks whether the plan for clause 5 is false when the fresh set is small. It is, and this section proves the extreme case rather than asserting it: with no fresh point there is no spoke, the mesh is meshCount δ ≥ 2 pairwise disjoint concentric frames, and the graph is not even connected.

The invariant is the sup norm. Every mesh segment other than a spoke lies on one ring, so with fresh = [] both ends of every edge have the same sup norm and a walk cannot change it. The corner of the outer ring has sup norm 1, the corner of the innermost ring has N⁻¹ ≠ 1.

With exactly one fresh point z the mesh is connected but still not 2-connected: the spoke at z is the only thing joining the rings, so each of its interior vertices — the crossing points (k/N) • z for 0 < k < N — is a cut vertex, separating the rings inside it from the rings outside. That case is not formalised here; it needs the crossing points to be vertices, which needs the MeetsAreCut clause of the mesh's cut points, and then a separation argument. It is recorded so that no consumer states clause 5 for squareMesh without a hypothesis guaranteeing two distinct fresh points.

theorem Schoenflies.end_mem_vertexSet_meshGraph {N : ℕ} {fresh anchors : List Plane} {R : Piece} (hR : R ∈ meshSegments N fresh) {z : Plane} (hz : z = R.1 ∨ z = R.2) : z ∈ (meshGraph N fresh anchors).vertexSet

An end of a source segment of the mesh is a vertex of the mesh graph.

theorem Schoenflies.supNorm_eq_of_isLink_of_fresh_nil {N : ℕ} (hN : 2 ≤ N) {anchors : List Plane} {P : Piece} {x y : Plane} (h : (meshGraph N [] anchors).IsLink P x y) : x.supNorm = y.supNorm

With no spoke, every edge of the mesh keeps the sup norm: it is a subsegment of a side of one ring.

theorem Schoenflies.not_connected_meshGraph_of_fresh_nil {N : ℕ} (hN : 2 ≤ N) (anchors : List Plane) : ¬(meshGraph N [] anchors).Connected

With no fresh point the mesh is disconnected.

theorem Schoenflies.not_isTwoConnected_squareMesh_of_fresh_nil (δ : ℝ) (anchors : List Plane) : ¬(squareMesh δ [] anchors).IsTwoConnected

prop:anchored-square-mesh clause 5 is false for a mesh with no fresh point. Every statement of 2-connectivity for squareMesh must therefore carry a hypothesis on fresh; see the section docstring for the one-fresh-point case, which is connected but has a cut vertex.

Concatenating two paths

Schoenflies/Graph/Walk.lean has Graph.IsWalk.append and no path analogue, because nothing before this needed one. The general lemma is here; the integrator should hoist it.

theorem Graph.IsPath.append_of_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W₁ : List β} : G.IsPath u W₁ v → ∀ {w : α} {W₂ : List β}, G.IsPath v W₂ w → (∀ x ∈ G.walkVertices u W₁, x ∈ G.walkVertices v W₂ → x = v) → G.IsPath u (W₁ ++ W₂) w

Two paths that meet only at the vertex they share concatenate to a path.

theorem Graph.IsPath.cons_cases {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {W : List β} (h : G.IsPath u (e :: W) v) : ∃ (w : α), G.IsLink e u w ∧ G.IsPath w W v ∧ u ∉ G.walkVertices w W

Reading a path off its first step. cases on Graph.IsPath needs the edge list to be a literal cons before it can discard the nil constructor; this packages that.

The subdivision hypothesis

The one general fact about overlayGraph that Schoenflies/SquareMeshConnected.lean names as missing, stated as a Prop so that the axiom audit stays a real guarantee and the defect shows up at the consumer. It is believed: the pieces of the subdivision of a nondegenerate segment have pairwise disjoint interiors and cover it, so the distance from P.1 orders them into a chain running from P.1 to P.2. Nothing about the mesh appears in it.

def Schoenflies.SubdividesToPath (pieces : List Piece) (points : List Plane) : Prop

The overlay subdivides each source segment into a path. For each nondegenerate source segment P there is an ordering W of exactly the overlay edges lying inside P which is a path of the overlay from P.1 to P.2.

Equations

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

theorem Schoenflies.walkVertices_subset_of_edges {pieces : List Piece} {points : List Plane} {A : Set Plane} {u : Plane} {W : List Piece} (hu : u ∈ A) (hW : ∀ Q ∈ W, Q.seg ⊆ A) {x : Plane} (hx : x ∈ (overlayGraph pieces points).walkVertices u W) : x ∈ A

A vertex an overlay walk visits lies wherever its source and its edges lie.

theorem Schoenflies.edgesCover_eq_seg {pieces : List Piece} {points : List Plane} {P : Piece} (hP : P ∈ pieces) {W : List Piece} (hW : ∀ (Q : Piece), Q ∈ W ↔ Q ∈ (overlayGraph pieces points).edgeSet ∧ Q.seg ⊆ P.seg) : Graph.edgesCover segmentDrawing W = P.seg

The edges of an overlay path along P occupy all of P.

The four sides of the outer ring

Names for the four sides of ringPieces 1 and the six pairwise intersections. Two opposite sides are disjoint; two adjacent ones meet in their common corner. Everything is mem_segment_horiz / mem_segment_vert and plane_eq_of_coords.

def Schoenflies.sideT : Piece

The top side of S, from the north-east corner to the north-west one.

Equations

• Schoenflies.sideT = (Schoenflies.Plane.mk 1 1, Schoenflies.Plane.mk (-1) 1)

def Schoenflies.sideL : Piece

The left side of S.

Equations

• Schoenflies.sideL = (Schoenflies.Plane.mk (-1) 1, Schoenflies.Plane.mk (-1) (-1))

def Schoenflies.sideB : Piece

The bottom side of S.

Equations

• Schoenflies.sideB = (Schoenflies.Plane.mk (-1) (-1), Schoenflies.Plane.mk 1 (-1))

def Schoenflies.sideR : Piece

The right side of S, from the south-east corner back to the north-east one.

Equations

• Schoenflies.sideR = (Schoenflies.Plane.mk 1 (-1), Schoenflies.Plane.mk 1 1)

theorem Schoenflies.sideT_mem_ringPieces : sideT ∈ ringPieces 1

theorem Schoenflies.sideL_mem_ringPieces : sideL ∈ ringPieces 1

theorem Schoenflies.sideB_mem_ringPieces : sideB ∈ ringPieces 1

theorem Schoenflies.sideR_mem_ringPieces : sideR ∈ ringPieces 1

theorem Schoenflies.mem_sideT {x : Plane} (h : x ∈ sideT.seg) : x.ofLp 1 = 1

theorem Schoenflies.mem_sideB {x : Plane} (h : x ∈ sideB.seg) : x.ofLp 1 = -1

theorem Schoenflies.mem_sideL {x : Plane} (h : x ∈ sideL.seg) : x.ofLp 0 = -1

theorem Schoenflies.mem_sideR {x : Plane} (h : x ∈ sideR.seg) : x.ofLp 0 = 1

theorem Schoenflies.sideT_inter_sideL {x : Plane} (h : x ∈ sideT.seg) (h' : x ∈ sideL.seg) : x = Plane.mk (-1) 1

theorem Schoenflies.sideL_inter_sideB {x : Plane} (h : x ∈ sideL.seg) (h' : x ∈ sideB.seg) : x = Plane.mk (-1) (-1)

theorem Schoenflies.sideB_inter_sideR {x : Plane} (h : x ∈ sideB.seg) (h' : x ∈ sideR.seg) : x = Plane.mk 1 (-1)

theorem Schoenflies.sideT_inter_sideR {x : Plane} (h : x ∈ sideT.seg) (h' : x ∈ sideR.seg) : x = Plane.mk 1 1

theorem Schoenflies.sideT_disjoint_sideB {x : Plane} (h : x ∈ sideT.seg) (h' : x ∈ sideB.seg) : False

theorem Schoenflies.sideL_disjoint_sideR {x : Plane} (h : x ∈ sideL.seg) (h' : x ∈ sideR.seg) : False

theorem Schoenflies.sides_cover : sideT.seg ∪ sideL.seg ∪ sideB.seg ∪ sideR.seg = modelCurve

The four sides occupy S.

theorem Schoenflies.side_seg_subset_modelCurve {P : Piece} (h : P = sideT ∨ P = sideL ∨ P = sideB ∨ P = sideR) : P.seg ⊆ modelCurve

The outer cycle of the mesh

The four sides of the outer ring are four overlay paths; three concatenations glue them into one path once round S, and the last edge of the fourth is peeled off to close the cycle. Peeling is why the fourth side is reversed: Graph.IsPath is built at the source end, so its first step is the one that can be split off, and the first step of the reversed side is the last edge of the side.

theorem Schoenflies.meshGraph_outer_cycle {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (anchors : List Plane) (hsub : SubdividesToPath (meshSegments N fresh) (meshPoints N fresh anchors)) : ∃ (e : Piece) (u : Plane) (v : Plane) (x : Plane) (D : List Piece), (meshGraph N fresh anchors).IsLongCycle e u v D x ∧ (∀ Q ∈ e :: D, Q.seg ⊆ modelCurve) ∧ Graph.edgesCover segmentDrawing (e :: D) = modelCurve

prop:anchored-square-mesh, clause 3 as a cycle, for the mesh graph itself. The edges of the mesh lying on S form a cycle of the mesh graph, and they occupy exactly S.

Schoenflies.cover_outerEdges proves only the point-set half of this, and SquareMeshConnected.gridGraph_outer_cycle proves the cycle for a different graph. This is the statement for Schoenflies.meshGraph.

The conclusion is existential because the hypothesis SubdividesToPath is: nothing here can name the edge list of a side without choosing it. Once that hypothesis is discharged by a theorem exporting the chain as a def, this should be restated with the cycle as data.

theorem Schoenflies.squareMesh_outer_cycle_of_subdividesToPath {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) (hsub : SubdividesToPath (meshSegments (meshCount δ) fresh) (meshPoints (meshCount δ) fresh anchors)) : ∃ (e : Piece) (u : Plane) (v : Plane) (x : Plane) (D : List Piece), (squareMesh δ fresh anchors).IsLongCycle e u v D x ∧ (∀ Q ∈ e :: D, Q.seg ⊆ modelCurve) ∧ Graph.edgesCover segmentDrawing (e :: D) = modelCurve

prop:anchored-square-mesh, clause 3 as a cycle, for squareMesh.

theorem Schoenflies.squareMesh_outer_cycleGraph_isTwoConnected_of_subdividesToPath {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) (hsub : SubdividesToPath (meshSegments (meshCount δ) fresh) (meshPoints (meshCount δ) fresh anchors)) : ∃ (e : Piece) (u : Plane) (D : List Piece), ((squareMesh δ fresh anchors).cycleGraph u e D).IsTwoConnected ∧ Graph.edgesCover segmentDrawing (e :: D) = modelCurve

The outer ring of the mesh is a 2-connected subgraph of the mesh. The first step of the blueprint's assembly of clause 5, for squareMesh itself: the cycle carrying S is 2-connected by lem:face-cycles's Graph.IsLongCycle.isTwoConnected. What is still missing is the rest of the assembly — the inner rings as cycles, and the spokes attached as ears at their crossings with each ring.