The anchored square mesh, closed

Schoenflies/SquareMesh.lean builds Schoenflies.squareMesh δ fresh anchors and proves the geometric clauses of prop:anchored-square-mesh; Schoenflies/SquareMeshConnected.lean, Schoenflies/SquareMeshFixed.lean and Schoenflies/LocalGrid.lean add the grid combinatorics, the outer cycle from an explicit path-subdivision hypothesis, and the degenerate cases. This module proves that path-subdivision hypothesis for the mesh.

The hypothesis that is discharged here

Schoenflies.SubdividesToPath pieces points says: 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. SquareMeshFixed.lean states it as an explicit hypothesis, and its docstring says the theorem does not exist on main.

It does exist. Schoenflies.exists_incWalk_insideEdges in Schoenflies/SquareCycle.lean is exactly that statement in the vocabulary of Graph.IsIncWalk — a walk along which dist P.1 · strictly increases — and Graph.IsIncWalk.isPath turns it into a path. The two modules were simply never in one import chain: SquareCycle.lean was imported only by Schoenflies/JordanClosed.lean. Schoenflies.subdividesToPath_of_overlay is the four-line bridge, allowing the results of SquareMeshFixed.lean to be applied directly to the mesh.

The outer cycle, as data

Schoenflies.meshGraph_outer_cycle is existential — its own docstring says "once that hypothesis is discharged by a theorem exporting the chain as a def, this should be restated with the cycle as data". That is done here: outerCycleEdge, outerCycleStart, outerCycleEnd, outerCycleThird and outerCycleDetour are defs, and the three clauses are separate lemmas about them. A consumer needing the outer cycle of the mesh takes these five names, not an ∃ it has to destructure at every use.

Clause 5, and the hypothesis that is actually true

Clause 5 — the skeleton of T is 2-connected — was absent from every earlier module, and for a good reason: it is false for Schoenflies.squareMesh δ fresh anchors when fresh has fewer than two distinct points (Schoenflies.not_isTwoConnected_meshGraph_of_fresh_subsingleton), and Schoenflies.FreshDense fresh δ alone does not repair it (Schoenflies.freshDense_not_isTwoConnected). What repairs it is FreshDense fresh δ together with δ < 4, which forces two distinct fresh points (Schoenflies.exists_two_distinct_fresh_of_freshDense). The blueprint's caller uses δ = ε_n = 2⁻ⁿ, far below 4, so the hypothesis is free at the only call site.

The assembly is the blueprint's, with one correction. The blueprint says "adding these finitely many cycles one at a time", but the first addition cannot be a cycle: distinct rings of the mesh are disjoint, so no two of them share the two vertices lem:union-two-connected needs. The first addition is an ear — down the spoke at z, round the inner ring, back up the spoke at w — and that is precisely where the two distinct fresh points are spent. After it, every further ring shares the crossing points r • z ≠ r • w with the spokes and goes in by lem:union-two-connected, and every further spoke is an ear between the outer and inner rings. Graph.IsTwoConnected.of_le_of_vertexSet_subset then transfers 2-connectivity from the assembly to the mesh, since every mesh vertex lies on a ring or on a spoke.

The proposition, clause by clause

prop:anchored-square-mesh is exported as data with its clauses as separate lemmas: the object is the def Schoenflies.squareMesh δ fresh anchors, and nothing is ∃-packaged.

1. every 2-cell has diameter < δ — Schoenflies.squareMesh_face_small;
2. every anchor on S is a boundary vertex — Schoenflies.squareMesh_anchor_mem_vertexSet;
3. every new internal edge meeting S ends at a fresh point — Schoenflies.squareMesh_inner_edge_at_fresh;
4. exactly one such edge at each fresh point — Schoenflies.squareMesh_unique_inner_edge;
5. the skeleton is 2-connected — Schoenflies.squareMesh_isTwoConnected (this module);
6. |T| ∖ S is connected — Schoenflies.squareMesh_isConnected_diff.

and the outer cycle, which def:admissible-graph and every downstream consumer need as a genuine cycle rather than a point set — Schoenflies.squareMesh_isLongCycle_outerCycle, Schoenflies.squareMesh_outerCycle_edgesCover (this module).

Blueprint

• subdividesToPath_of_overlay, meshSubdividesToPath — lem:polygonal-overlay: the subdivision of one source segment is a path of the overlay. This discharges Schoenflies.SubdividesToPath.
• meshGraph_outer_cycle_of_mem_modelCurve, squareMesh_outer_cycle — prop:anchored-square-mesh clause 3 as a cycle, with no hypothesis beyond fresh ⊆ S.
• outerCycleEdge, outerCycleStart, outerCycleEnd, outerCycleThird, outerCycleDetour, squareMesh_isLongCycle_outerCycle, squareMesh_outerCycle_subset_modelCurve, squareMesh_outerCycle_edgesCover — the same cycle as data with its clauses as lemmas.
• rsideT/rsideL/rsideB/rsideR and meshGraph_ring_cycle — the outer-cycle argument at every radius: each ring of the mesh is a long cycle occupying exactly that ring.
• ringGraph, ringGraph_isTwoConnected, mem_vertexSet_ringGraph — each ring as a named 2-connected subgraph, via Schoenflies.squareGraph at centre 0.
• spokePiece_inter_ringSet, smul_mem_meshPoints, smul_mem_vertexSet_ringGraph — the crossing points r • z as vertices, from the MeetsAreCut clause of meshPoints.
• spokeWalk, spokeGraph — each spoke as a path of the mesh.
• meshEar, meshEar_isPath, meshCore_isTwoConnected — lem:subdivision-ear-preserve (b): the ear that joins the outer ring to the inner one.
• attachRings, attachSpokes and their 2-connectivity — lem:union-two-connected and lem:subdivision-ear-preserve iterated, the blueprint's "adding these finitely many cycles one at a time".
• meshGraph_isTwoConnected, squareMesh_isTwoConnected — prop:anchored-square-mesh clause 5.

SubdividesToPath is a theorem

The membership clause of Schoenflies.SubdividesToPath and the membership clause of Schoenflies.insideEdges are the same statement: Q ∈ E(overlayGraph pieces points) unfolds to Q ∈ overlayPieces pieces points by Iff.rfl. So the only work is to turn the increasing walk into a path, which Graph.IsIncWalk.isPath does.

theorem Schoenflies.subdividesToPath_of_overlay {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) : SubdividesToPath pieces points

The subdivision of a source segment is a path of the overlay. This is Schoenflies.SubdividesToPath, the hypothesis Schoenflies/SquareMeshFixed.lean carries through all of its results, proved from Schoenflies.exists_incWalk_insideEdges.

theorem Schoenflies.meshSubdividesToPath {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (anchors : List Plane) : SubdividesToPath (meshSegments N fresh) (meshPoints N fresh anchors)

The mesh's own instance of Schoenflies.SubdividesToPath.

The outer cycle, with no hypothesis

theorem Schoenflies.meshGraph_outer_cycle_of_mem_modelCurve {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (anchors : List Plane) : ∃ (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

Clause 3 as a cycle, for meshGraph.

theorem Schoenflies.squareMesh_outer_cycle {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) : ∃ (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

Clause 3 as a cycle, for squareMesh.

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

The mesh has a 2-connected outer-cycle subgraph.

The outer cycle as data

Five defs and three lemmas, replacing the five-fold existential above. The dite is what makes the definition total: the hypothesis fresh ⊆ S is not available inside a def, so the data is junk when it fails and the lemmas carry the hypothesis.

noncomputable def Schoenflies.outerCycleData (δ : ℝ) (fresh anchors : List Plane) : Piece × Plane × Plane × Plane × List Piece

The outer cycle of the mesh, as a tuple (e, u, v, w, D): the distinguished edge, its two ends, the third vertex, and the detour. Junk when fresh ⊄ S.

Equations

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

noncomputable def Schoenflies.outerCycleEdge (δ : ℝ) (fresh anchors : List Plane) : Piece

The distinguished edge of the outer cycle.

Equations

• Schoenflies.outerCycleEdge δ fresh anchors = (Schoenflies.outerCycleData δ fresh anchors).1

noncomputable def Schoenflies.outerCycleStart (δ : ℝ) (fresh anchors : List Plane) : Plane

The vertex the outer cycle starts at: one end of outerCycleEdge.

Equations

• Schoenflies.outerCycleStart δ fresh anchors = (Schoenflies.outerCycleData δ fresh anchors).2.1

noncomputable def Schoenflies.outerCycleEnd (δ : ℝ) (fresh anchors : List Plane) : Plane

The other end of outerCycleEdge, where the detour ends.

Equations

• Schoenflies.outerCycleEnd δ fresh anchors = (Schoenflies.outerCycleData δ fresh anchors).2.2.1

noncomputable def Schoenflies.outerCycleThird (δ : ℝ) (fresh anchors : List Plane) : Plane

A third vertex of the outer cycle, distinct from its two named ones: this is what makes the cycle long, hence 2-connected.

Equations

• Schoenflies.outerCycleThird δ fresh anchors = (Schoenflies.outerCycleData δ fresh anchors).2.2.2.1

noncomputable def Schoenflies.outerCycleDetour (δ : ℝ) (fresh anchors : List Plane) : List Piece

The detour of the outer cycle: the path from outerCycleStart to outerCycleEnd avoiding outerCycleEdge.

Equations

• Schoenflies.outerCycleDetour δ fresh anchors = (Schoenflies.outerCycleData δ fresh anchors).2.2.2.2

theorem Schoenflies.outerCycleData_spec {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) : (squareMesh δ fresh anchors).IsLongCycle (outerCycleEdge δ fresh anchors) (outerCycleStart δ fresh anchors) (outerCycleEnd δ fresh anchors) (outerCycleDetour δ fresh anchors) (outerCycleThird δ fresh anchors) ∧ (∀ Q ∈ outerCycleEdge δ fresh anchors :: outerCycleDetour δ fresh anchors, Q.seg ⊆ modelCurve) ∧ Graph.edgesCover segmentDrawing (outerCycleEdge δ fresh anchors :: outerCycleDetour δ fresh anchors) = modelCurve

theorem Schoenflies.squareMesh_isLongCycle_outerCycle {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) : (squareMesh δ fresh anchors).IsLongCycle (outerCycleEdge δ fresh anchors) (outerCycleStart δ fresh anchors) (outerCycleEnd δ fresh anchors) (outerCycleDetour δ fresh anchors) (outerCycleThird δ fresh anchors)

Clause 3, as data. The edge, the two ends, the third vertex and the detour form a long cycle of the mesh.

theorem Schoenflies.squareMesh_outerCycle_subset_modelCurve {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) (Q : Piece) : Q ∈ outerCycleEdge δ fresh anchors :: outerCycleDetour δ fresh anchors → Q.seg ⊆ modelCurve

Every edge of the outer cycle lies on S.

theorem Schoenflies.squareMesh_outerCycle_edgesCover {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) : Graph.edgesCover segmentDrawing (outerCycleEdge δ fresh anchors :: outerCycleDetour δ fresh anchors) = modelCurve

The outer cycle occupies exactly S.

theorem Schoenflies.squareMesh_outerCycleGraph_isTwoConnected {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) : ((squareMesh δ fresh anchors).cycleGraph (outerCycleStart δ fresh anchors) (outerCycleEdge δ fresh anchors) (outerCycleDetour δ fresh anchors)).IsTwoConnected

The outer cycle, as a subgraph, is 2-connected.

The four sides of a ring of arbitrary radius

Schoenflies/SquareMeshFixed.lean names the four sides of the outer ring — sideT, sideL, sideB, sideR — and proves the handful of coordinate facts that the outer-cycle argument runs on. Every inner ring needs the same facts, so they are restated here with the radius as a parameter; rsideT 1 = sideT and so on, definitionally.

def Schoenflies.rsideT (r : ℝ) : Piece

The top side of the ring of radius r, from the north-east corner to the north-west one.

Equations

• Schoenflies.rsideT r = (Schoenflies.Plane.mk r r, Schoenflies.Plane.mk (-r) r)

def Schoenflies.rsideL (r : ℝ) : Piece

The left side of the ring of radius r, from north-west to south-west.

Equations

• Schoenflies.rsideL r = (Schoenflies.Plane.mk (-r) r, Schoenflies.Plane.mk (-r) (-r))

def Schoenflies.rsideB (r : ℝ) : Piece

The bottom side of the ring of radius r, from south-west to south-east.

Equations

• Schoenflies.rsideB r = (Schoenflies.Plane.mk (-r) (-r), Schoenflies.Plane.mk r (-r))

def Schoenflies.rsideR (r : ℝ) : Piece

The right side of the ring of radius r, from south-east back to north-east.

Equations

• Schoenflies.rsideR r = (Schoenflies.Plane.mk r (-r), Schoenflies.Plane.mk r r)

theorem Schoenflies.rsideT_one : rsideT 1 = sideT

theorem Schoenflies.rsideL_one : rsideL 1 = sideL

theorem Schoenflies.rsideB_one : rsideB 1 = sideB

theorem Schoenflies.rsideR_one : rsideR 1 = sideR

theorem Schoenflies.rsideT_mem_ringPieces (r : ℝ) : rsideT r ∈ ringPieces r

theorem Schoenflies.rsideL_mem_ringPieces (r : ℝ) : rsideL r ∈ ringPieces r

theorem Schoenflies.rsideB_mem_ringPieces (r : ℝ) : rsideB r ∈ ringPieces r

theorem Schoenflies.rsideR_mem_ringPieces (r : ℝ) : rsideR r ∈ ringPieces r

theorem Schoenflies.mem_rsideT {r : ℝ} {x : Plane} (h : x ∈ (rsideT r).seg) : x.ofLp 1 = r

theorem Schoenflies.mem_rsideB {r : ℝ} {x : Plane} (h : x ∈ (rsideB r).seg) : x.ofLp 1 = -r

theorem Schoenflies.mem_rsideL {r : ℝ} {x : Plane} (h : x ∈ (rsideL r).seg) : x.ofLp 0 = -r

theorem Schoenflies.mem_rsideR {r : ℝ} {x : Plane} (h : x ∈ (rsideR r).seg) : x.ofLp 0 = r

theorem Schoenflies.rsideT_inter_rsideL {r : ℝ} {x : Plane} (h : x ∈ (rsideT r).seg) (h' : x ∈ (rsideL r).seg) : x = Plane.mk (-r) r

theorem Schoenflies.rsideL_inter_rsideB {r : ℝ} {x : Plane} (h : x ∈ (rsideL r).seg) (h' : x ∈ (rsideB r).seg) : x = Plane.mk (-r) (-r)

theorem Schoenflies.rsideB_inter_rsideR {r : ℝ} {x : Plane} (h : x ∈ (rsideB r).seg) (h' : x ∈ (rsideR r).seg) : x = Plane.mk r (-r)

theorem Schoenflies.rsideT_inter_rsideR {r : ℝ} {x : Plane} (h : x ∈ (rsideT r).seg) (h' : x ∈ (rsideR r).seg) : x = Plane.mk r r

theorem Schoenflies.rsideT_disjoint_rsideB {r : ℝ} (hr : 0 < r) {x : Plane} (h : x ∈ (rsideT r).seg) (h' : x ∈ (rsideB r).seg) : False

theorem Schoenflies.rsideL_disjoint_rsideR {r : ℝ} (hr : 0 < r) {x : Plane} (h : x ∈ (rsideL r).seg) (h' : x ∈ (rsideR r).seg) : False

theorem Schoenflies.rsides_cover {r : ℝ} (hr : 0 ≤ r) : (rsideT r).seg ∪ (rsideL r).seg ∪ (rsideB r).seg ∪ (rsideR r).seg = ringSet r

The four sides of the ring of radius r occupy that ring.

theorem Schoenflies.rside_seg_subset_ringSet {r : ℝ} (hr : 0 ≤ r) {P : Piece} (h : P = rsideT r ∨ P = rsideL r ∨ P = rsideB r ∨ P = rsideR r) : P.seg ⊆ ringSet r

theorem Schoenflies.ring_ringPieces_mem {N : ℕ} {fresh : List Plane} {r : ℝ} (hr : r ∈ meshRadii N) {R : Piece} (hR : R ∈ ringPieces r) : R ∈ meshSegments N fresh

Every side of every ring of the mesh is a mesh segment.

Every ring of the mesh is a cycle

Schoenflies.meshGraph_outer_cycle proves this for the outer ring, r = 1, and every step of its proof is about the four sides of that ring and nothing else. With the sides of a ring of arbitrary radius now available, the same argument runs verbatim at every radius: the four sides are four overlay paths, three concatenations glue them into one path once round the ring, and the last edge of the fourth is peeled off to close the cycle.

This is the theorem the blueprint's "adding these finitely many cycles one at a time" needs for the inner rings, and which Schoenflies/SquareMeshFixed.lean names as missing.

theorem Schoenflies.meshGraph_ring_cycle {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (anchors : List Plane) {r : ℝ} (hr : r ∈ meshRadii N) : ∃ (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 ⊆ ringSet r) ∧ Graph.edgesCover segmentDrawing (e :: D) = ringSet r

Every ring of the mesh is a long cycle of the mesh graph, and its edges occupy exactly that ring.

For r = 1 this is Schoenflies.meshGraph_outer_cycle; the content added here is that the statement holds at every radius of Schoenflies.meshRadii, which is what the assembly of clause 5 of prop:anchored-square-mesh consumes.

Each ring of the mesh, as a named 2-connected subgraph

Schoenflies/SquareCycle.lean proves that the part of any polygonal overlay lying on the boundary of a square whose four sides are among the overlay's source segments is a long cycle, and is 2-connected — at any centre and any positive radius. The rings of the mesh are exactly that, at centre 0: squarePieces 0 r and ringPieces r are the same list. So each ring comes with a name, ringGraph, a 2-connectivity proof, and the two membership lemmas the assembly of clause 5 needs, at no cost.

theorem Schoenflies.squarePieces_zero (r : ℝ) : squarePieces 0 r = ringPieces r

The four sides of the square of radius r about the origin are the four sides of the ring of radius r: the two lists are equal, entry for entry.

theorem Schoenflies.frontier_closedSquare_zero {r : ℝ} (hr : 0 ≤ r) : frontier (Plane.closedSquare 0 r) = ringSet r

The frontier of the closed square of radius r about the origin is the ring of radius r.

noncomputable def Schoenflies.ringGraph (N : ℕ) (fresh anchors : List Plane) (r : ℝ) : Graph Plane Piece

The ring of radius r of the mesh, as a subgraph: the mesh edges lying on that ring.

Equations

• Schoenflies.ringGraph N fresh anchors r = Schoenflies.squareGraph (Schoenflies.meshSegments N fresh) (Schoenflies.meshPoints N fresh anchors) 0 r

theorem Schoenflies.ringGraph_le (N : ℕ) (fresh anchors : List Plane) (r : ℝ) : ringGraph N fresh anchors r ≤ meshGraph N fresh anchors

theorem Schoenflies.squarePieces_zero_subset_meshSegments {N : ℕ} {fresh : List Plane} {r : ℝ} (hr : r ∈ meshRadii N) (P : Piece) : P ∈ squarePieces 0 r → P ∈ meshSegments N fresh

The sides of the ring of radius r are mesh segments, for every radius the mesh uses.

theorem Schoenflies.ringGraph_isTwoConnected {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (anchors : List Plane) {r : ℝ} (hr : r ∈ meshRadii N) : (ringGraph N fresh anchors r).IsTwoConnected

Every ring of the mesh is a 2-connected subgraph.

theorem Schoenflies.mem_vertexSet_ringGraph {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {anchors : List Plane} {r : ℝ} (hr : r ∈ meshRadii N) {y : Plane} (hy : y ∈ meshPoints N fresh anchors) (hyr : y ∈ ringSet r) : y ∈ (ringGraph N fresh anchors r).vertexSet

A cut point of the mesh lying on a ring is a vertex of that ring. This is what makes the crossing points of the spokes with the rings usable as the shared vertices of lem:union-two-connected.

Where a spoke crosses a ring

Schoenflies/SquareMeshFixed.lean records the crossing points r • z as the thing its assembly of clause 5 lacked: "the crossing points r • z as vertices (which needs the MeetsAreCut clause of meshPoints)". That is what this section supplies. The sup norm is a faithful coordinate along a spoke (Schoenflies.supNorm_smul_of_mem_modelCurve), so a spoke meets the ring of radius r in the single point r • z; a singleton meet forces both ends of the MeetsAreCut segment to be that point; and mem_vertexSet_ringGraph then makes it a vertex of the ring.

theorem Schoenflies.inv_le_of_mem_meshRadii {N : ℕ} (hN : 2 ≤ N) {r : ℝ} (hr : r ∈ meshRadii N) : (↑N)⁻¹ ≤ r

theorem Schoenflies.spokePiece_inter_ringSet {N : ℕ} (hN : 2 ≤ N) {z : Plane} (hz : z ∈ modelCurve) {r : ℝ} (hr : r ∈ meshRadii N) : (spokePiece N z).seg ∩ ringSet r = {r • z}

A spoke meets a ring in exactly one point.

theorem Schoenflies.smul_mem_ringSet {r : ℝ} (hr : 0 ≤ r) {z : Plane} (hz : z ∈ modelCurve) : r • z ∈ ringSet r

theorem Schoenflies.smul_mem_meshPoints {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) {r : ℝ} (hr : r ∈ meshRadii N) : r • z ∈ meshPoints N fresh anchors

Every crossing point of a spoke with a ring is a cut point of the mesh. The meet of the spoke with the side of the ring through the crossing point is the single point r • z, and MeetsAreCut returns a segment with both ends among the cut points; a segment equal to a singleton has both ends there.

theorem Schoenflies.smul_mem_vertexSet_ringGraph {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) {r : ℝ} (hr : r ∈ meshRadii N) : r • z ∈ (ringGraph N fresh anchors r).vertexSet

The crossing point is a vertex of the ring it lies on.

theorem Schoenflies.smul_ne_smul {r : ℝ} (hr : r ≠ 0) {z w : Plane} (hzw : z ≠ w) : r • z ≠ r • w

Two distinct fresh points have distinct crossing points on every ring.

The spokes, as paths of the mesh

Schoenflies.SubdividesToPath — now a theorem — turns each spoke into a path of the mesh from its outer end z to its inner end N⁻¹ • z. The path is exported as data, spokeWalk, so that the assembly can name it; and the crossing points are shown to be among the vertices it visits, which is what makes each ring attachable at two of them.

theorem Schoenflies.mem_walkVertices_of_mem_points {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) {P : Piece} (hP : P ∈ pieces) {W : List Piece} (hW : ∀ (Q : Piece), Q ∈ W ↔ Q ∈ (overlayGraph pieces points).edgeSet ∧ Q.seg ⊆ P.seg) {q : Plane} (hq : q ∈ points) (hqP : q ∈ P.seg) : q ∈ (overlayGraph pieces points).walkVertices P.1 W

A cut point lying on a source segment is a vertex of the path that subdivides it. The edges of the path cover the segment, and a cut point is interior to no edge of an overlay, so it is an end of one of them.

noncomputable def Schoenflies.spokeWalk (N : ℕ) (fresh anchors : List Plane) (z : Plane) : List Piece

The subdivision of the spoke at a fresh point, as data: the list of mesh edges lying inside spokePiece N z, in order from z inwards. Junk when z is not a fresh point of the model curve.

Equations

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

theorem Schoenflies.spokeWalk_spec {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) : (meshGraph N fresh anchors).IsPath z (spokeWalk N fresh anchors z) ((↑N)⁻¹ • z) ∧ ∀ (Q : Piece), Q ∈ spokeWalk N fresh anchors z ↔ Q ∈ (meshGraph N fresh anchors).edgeSet ∧ Q.seg ⊆ (spokePiece N z).seg

theorem Schoenflies.spokeWalk_isPath {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) : (meshGraph N fresh anchors).IsPath z (spokeWalk N fresh anchors z) ((↑N)⁻¹ • z)

theorem Schoenflies.spokeWalk_seg_subset {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) {Q : Piece} (hQ : Q ∈ spokeWalk N fresh anchors z) : Q.seg ⊆ (spokePiece N z).seg

theorem Schoenflies.smul_mem_walkVertices_spokeWalk {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) {r : ℝ} (hr : r ∈ meshRadii N) : r • z ∈ (meshGraph N fresh anchors).walkVertices z (spokeWalk N fresh anchors z)

Every crossing point on a spoke is a vertex the spoke's path visits.

theorem Schoenflies.walkVertices_spokeWalk_subset {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) {x : Plane} (hx : x ∈ (meshGraph N fresh anchors).walkVertices z (spokeWalk N fresh anchors z)) : x ∈ (spokePiece N z).seg

Every vertex the spoke's path visits lies on the spoke.

The core: outer ring, two spokes, inner ring

The blueprint assembles clause 5 by "adding these finitely many cycles one at a time", but the first addition cannot be a cycle: distinct rings of the mesh are disjoint, so no two of them share the two vertices lem:union-two-connected asks for. What joins them is an ear — a path with both ends on the outer ring — and the only such path runs down one spoke, round part of the inner ring, and back up another spoke. That is why clause 5 needs two distinct fresh points, and why it is false with fewer (Schoenflies.not_isTwoConnected_meshGraph_of_fresh_subsingleton).

Once that ear is in place the inner ring shares the two crossing points N⁻¹ • z and N⁻¹ • w with it, and Graph.IsTwoConnected.union applies; from then on every further ring shares r • z and r • w, and every further spoke is an ear between the outer and inner rings.

theorem Schoenflies.spokePiece_disjoint {N : ℕ} (hN : 2 ≤ N) {z w : Plane} (hz : z ∈ modelCurve) (hw : w ∈ modelCurve) (hzw : z ≠ w) {x : Plane} (hxz : x ∈ (spokePiece N z).seg) (hxw : x ∈ (spokePiece N w).seg) : False

Distinct spokes are disjoint — the blueprint's "two radial segments in the annulus can meet only if they lie on the same ray, and then their endpoints on S are equal".

theorem Schoenflies.ringGraph_edge_seg_subset {N : ℕ} {fresh anchors : List Plane} {r : ℝ} (hr : 0 ≤ r) {Q : Piece} (hQ : Q ∈ (ringGraph N fresh anchors r).edgeSet) : Q.seg ⊆ ringSet r

noncomputable def Schoenflies.ringArc (N : ℕ) (fresh anchors : List Plane) (r : ℝ) (a b : Plane) : List Piece

An arc of the ring of radius r between two of its vertices, as data. The ring is 2-connected, hence connected, so such a path exists; which of the two arcs is chosen does not matter — only that it is a path inside the ring.

Equations

• Schoenflies.ringArc N fresh anchors r a b = if h : ∃ (P : List Schoenflies.Piece), (Schoenflies.ringGraph N fresh anchors r).IsPath a P b then h.choose else []

theorem Schoenflies.ringArc_isPath {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {r : ℝ} (hr : r ∈ meshRadii N) {a b : Plane} (ha : a ∈ (ringGraph N fresh anchors r).vertexSet) (hb : b ∈ (ringGraph N fresh anchors r).vertexSet) : (ringGraph N fresh anchors r).IsPath a (ringArc N fresh anchors r a b) b

noncomputable def Schoenflies.meshEar (N : ℕ) (fresh anchors : List Plane) (z w : Plane) : List Piece

The ear: down the spoke at z, round the inner ring, and back up the spoke at w.

Equations

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

theorem Schoenflies.meshEar_isPath {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {z w : Plane} (hz : z ∈ fresh) (hw : w ∈ fresh) (hzw : z ≠ w) : (meshGraph N fresh anchors).IsPath z (meshEar N fresh anchors z w) w

The assembly

meshCore is the outer ring, the ear, and the inner ring. attachRings then adds every ring by lem:union-two-connected at the two crossing points r • z ≠ r • w, and attachSpokes adds every remaining spoke by lem:subdivision-ear-preserve (b) — its two ends are u on the outer ring and N⁻¹ • u on the inner one, both already present. Finally every vertex of the mesh lies on a ring or on a spoke, so the assembled graph spans the mesh and Graph.IsTwoConnected.of_le_of_vertexSet_subset transfers 2-connectivity to the mesh itself.

noncomputable def Schoenflies.spokeGraph (N : ℕ) (fresh anchors : List Plane) (u : Plane) : Graph Plane Piece

The spoke at u, as a subgraph of the mesh.

Equations

• Schoenflies.spokeGraph N fresh anchors u = (Schoenflies.meshGraph N fresh anchors).pathGraphOf u (Schoenflies.spokeWalk N fresh anchors u)

theorem Schoenflies.spokeGraph_le {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {u : Plane} (hu : u ∈ fresh) : spokeGraph N fresh anchors u ≤ meshGraph N fresh anchors

theorem Schoenflies.smul_ne_self {N : ℕ} (hN : 2 ≤ N) {u : Plane} (hu : u ∈ modelCurve) {r : ℝ} (hr : r ∈ meshRadii N) (hr1 : r ≠ 1) : r • u ≠ u

A crossing point on a ring other than the outer one is not the fresh point itself.

theorem Schoenflies.smul_mem_coveredVertices_spokeWalk {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) (anchors : List Plane) {u : Plane} (hu : u ∈ fresh) {r : ℝ} (hr : r ∈ meshRadii N) (hr1 : r ≠ 1) : r • u ∈ (meshGraph N fresh anchors).coveredVertices (spokeWalk N fresh anchors u)

An inner crossing point is covered by the spoke's path — it is an end of one of its edges, not merely its source.

noncomputable def Schoenflies.meshCore (N : ℕ) (fresh anchors : List Plane) (z w : Plane) : Graph Plane Piece

The core: outer ring, ear, inner ring.

Equations

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

theorem Schoenflies.meshCore_le {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {z w : Plane} (hz : z ∈ fresh) (hw : w ∈ fresh) (hzw : z ≠ w) : meshCore N fresh anchors z w ≤ meshGraph N fresh anchors

theorem Schoenflies.mem_vertexSet_ringGraph_one {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {u : Plane} (hu : u ∈ fresh) : u ∈ (ringGraph N fresh anchors 1).vertexSet

A fresh point is a vertex of the outer ring.

theorem Schoenflies.meshCore_isTwoConnected {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (anchors : List Plane) {z w : Plane} (hz : z ∈ fresh) (hw : w ∈ fresh) (hzw : z ≠ w) : (meshCore N fresh anchors z w).IsTwoConnected

The core is 2-connected.

Adding every ring and every spoke

theorem Schoenflies.smul_mem_walkVertices_meshEar {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) (anchors : List Plane) {z w : Plane} (hz : z ∈ fresh) (hw : w ∈ fresh) (hzw : z ≠ w) {r : ℝ} (hr : r ∈ meshRadii N) : r • z ∈ (meshGraph N fresh anchors).walkVertices z (meshEar N fresh anchors z w) ∧ r • w ∈ (meshGraph N fresh anchors).walkVertices z (meshEar N fresh anchors z w)

Both crossing points of a spoke lie on the ear, whichever ring they belong to.

noncomputable def Schoenflies.attachRings (N : ℕ) (fresh anchors : List Plane) (K : Graph Plane Piece) : List ℝ → Graph Plane Piece

The rings of the mesh, attached one at a time — lem:union-two-connected iterated.

Equations

• Schoenflies.attachRings N fresh anchors K [] = K
• Schoenflies.attachRings N fresh anchors K (r :: rs) = (Schoenflies.attachRings N fresh anchors K rs).union (Schoenflies.ringGraph N fresh anchors r)

noncomputable def Schoenflies.attachSpokes (N : ℕ) (fresh anchors : List Plane) (K : Graph Plane Piece) : List Plane → Graph Plane Piece

The spokes of the mesh, attached one at a time — lem:subdivision-ear-preserve (b) iterated.

Equations

• Schoenflies.attachSpokes N fresh anchors K [] = K
• Schoenflies.attachSpokes N fresh anchors K (u :: us) = (Schoenflies.attachSpokes N fresh anchors K us).union (Schoenflies.spokeGraph N fresh anchors u)

theorem Schoenflies.le_attachRings (N : ℕ) (fresh anchors : List Plane) (K : Graph Plane Piece) (l : List ℝ) : K ≤ attachRings N fresh anchors K l

theorem Schoenflies.le_attachSpokes (N : ℕ) (fresh anchors : List Plane) (K : Graph Plane Piece) (l : List Plane) : K ≤ attachSpokes N fresh anchors K l

theorem Schoenflies.attachRings_le {N : ℕ} {fresh anchors : List Plane} {K : Graph Plane Piece} (hK : K ≤ meshGraph N fresh anchors) (l : List ℝ) : attachRings N fresh anchors K l ≤ meshGraph N fresh anchors

theorem Schoenflies.attachSpokes_le {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) {anchors : List Plane} {K : Graph Plane Piece} (hK : K ≤ meshGraph N fresh anchors) {l : List Plane} (hl : ∀ u ∈ l, u ∈ fresh) : attachSpokes N fresh anchors K l ≤ meshGraph N fresh anchors

theorem Schoenflies.ringGraph_le_attachRings {N : ℕ} {fresh anchors : List Plane} {K : Graph Plane Piece} (hK : K ≤ meshGraph N fresh anchors) {l : List ℝ} {r : ℝ} (hr : r ∈ l) : ringGraph N fresh anchors r ≤ attachRings N fresh anchors K l

theorem Schoenflies.spokeGraph_le_attachSpokes {N : ℕ} {fresh anchors : List Plane} {K : Graph Plane Piece} (hK : K ≤ meshGraph N fresh anchors) {l : List Plane} {u : Plane} (hN : 2 ≤ N) (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) (hl : ∀ x ∈ l, x ∈ fresh) (hu : u ∈ l) : spokeGraph N fresh anchors u ≤ attachSpokes N fresh anchors K l

theorem Schoenflies.attachRings_isTwoConnected {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) {anchors : List Plane} {z w : Plane} (hz : z ∈ fresh) (hw : w ∈ fresh) (hzw : z ≠ w) {K : Graph Plane Piece} (hK : K.IsTwoConnected) (hKle : K ≤ meshGraph N fresh anchors) (hzK : ∀ r ∈ meshRadii N, r • z ∈ K.vertexSet) (hwK : ∀ r ∈ meshRadii N, r • w ∈ K.vertexSet) {l : List ℝ} (hl : ∀ r ∈ l, r ∈ meshRadii N) : (attachRings N fresh anchors K l).IsTwoConnected

theorem Schoenflies.attachSpokes_isTwoConnected {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) {anchors : List Plane} {K : Graph Plane Piece} (hK : K.IsTwoConnected) (hKle : K ≤ meshGraph N fresh anchors) (houter : ∀ u ∈ fresh, u ∈ K.vertexSet) (hinner : ∀ u ∈ fresh, (↑N)⁻¹ • u ∈ K.vertexSet) {l : List Plane} (hl : ∀ u ∈ l, u ∈ fresh) : (attachSpokes N fresh anchors K l).IsTwoConnected

Clause 5: the skeleton of the mesh is 2-connected

noncomputable def Schoenflies.meshAssembly (N : ℕ) (fresh anchors : List Plane) (z w : Plane) : Graph Plane Piece

The whole mesh, assembled: the core, then every ring, then every spoke.

Equations

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

theorem Schoenflies.meshAssembly_le {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) (anchors : List Plane) {z w : Plane} (hz : z ∈ fresh) (hw : w ∈ fresh) (hzw : z ≠ w) : meshAssembly N fresh anchors z w ≤ meshGraph N fresh anchors

theorem Schoenflies.meshAssembly_isTwoConnected {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) (anchors : List Plane) {z w : Plane} (hz : z ∈ fresh) (hw : w ∈ fresh) (hzw : z ≠ w) : (meshAssembly N fresh anchors z w).IsTwoConnected

theorem Schoenflies.vertexSet_meshGraph_subset_meshAssembly {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) (anchors : List Plane) {z w : Plane} (hz : z ∈ fresh) (hw : w ∈ fresh) (hzw : z ≠ w) : (meshGraph N fresh anchors).vertexSet ⊆ (meshAssembly N fresh anchors z w).vertexSet

The assembly spans the mesh. Every vertex of the mesh is an end of an edge, every edge lies inside a mesh segment, and a mesh segment is either a ring side — putting the vertex on that ring — or a spoke, putting it on that spoke's path.

theorem Schoenflies.meshGraph_isTwoConnected {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) (anchors : List Plane) {z w : Plane} (hz : z ∈ fresh) (hw : w ∈ fresh) (hzw : z ≠ w) : (meshGraph N fresh anchors).IsTwoConnected

prop:anchored-square-mesh, clause 5, for meshGraph: the skeleton is 2-connected.

The hypothesis is two distinct fresh points, and it is exactly right: Schoenflies.not_isTwoConnected_meshGraph_of_fresh_subsingleton shows the conclusion is false with fewer.

theorem Schoenflies.squareMesh_isTwoConnected {fresh : List Plane} (hfresh : ∀ x ∈ fresh, x ∈ modelCurve) {δ : ℝ} (hdense : FreshDense fresh δ) (hδ : δ < 4) (anchors : List Plane) : (squareMesh δ fresh anchors).IsTwoConnected

prop:anchored-square-mesh, clause 5, for squareMesh.

Schoenflies.FreshDense fresh δ alone does not suffice — freshDense_not_isTwoConnected is the counterexample — but FreshDense together with δ < 4 does, because it forces two distinct fresh points (Schoenflies.exists_two_distinct_fresh_of_freshDense). The blueprint's caller uses δ = ε_n = 2⁻ⁿ, far below 4.