The anchored square mesh

The geometric core of Proposition prop:anchored-square-mesh, in vocabulary that exists today: Part II's cellulations, V_boundary and fresh points u(𝒜) are not built here, so the mesh is stated as a finite plane graph with a straight-line drawing, with the clauses of the proposition as separate theorems about it.

The construction

squareMesh δ fresh anchors is meshCount δ concentric ring frames of radii 1/N, 2/N, …, 1 inside Q = [-1,1]², together with one full-length radial spoke [z, N⁻¹ • z] at each fresh boundary point z. The list of segments is handed to overlayGraph (Lemma 3.7), which subdivides at every crossing; the anchors are added to the cut points, which is what makes each of them a vertex.

This is not literally the blueprint's construction, and the difference is deliberate. The blueprint has one collar λ ≤ ‖x‖∞ ≤ 1 plus a rectangular grid filling λQ. Here the collar is repeated N times and there is no grid at all: the innermost square N⁻¹ Q is a single cell, of diameter 2√2/N < δ. That removes the "choose fine enough horizontal and vertical coordinates, including the four corners and all the points λ z_i" step entirely, and makes the whole mesh radial, so that one estimate — ‖tz - sw‖ ≤ t‖z - w‖ + |t - s|‖w‖, the blueprint's own — covers every cell. Nothing downstream can tell the difference: the clauses are the interface.

The blueprint's cyclic ordering of the fresh points is likewise gone. Where it says "choose z_0, …, z_{m-1} in cyclic order so that each boundary arc between consecutive ones has diameter < δ/4", this module takes the order-free consequence as a hypothesis, FreshDense fresh δ: every connected subset of S avoiding all the fresh points has diameter at most δ/2. A set-level statement needs no ordering, and it is exactly what the blueprint's own argument (parametrize S by a circle, cut it into small arcs, put one fresh point inside each) produces.

What is proved, and what is not

The clauses about faces, anchors, edges reaching S and connectedness of |T| ∖ S are proved in full. Two gaps, both stated plainly:

• The outer cycle is proved only as a point set. squareMesh_cover_outerEdges says the edges whose segments lie on S occupy exactly S. That these edges form a cycle of the graph is not proved: it needs the fresh points, the anchors and the four corners put in cyclic order along S, which is precisely the ordering this construction was designed to avoid. A later module wanting the outer cycle must build it.
• 2-connectivity is not proved at all. It is not present as a hypothesis either — a hypothesis restating the goal would be worthless. The route is the blueprint's: the innermost ring is a cycle, and each annulus between consecutive rings is added one rectangle at a time by Graph.IsTwoConnected.union, each added cycle sharing at least two vertices with what is already there. Nothing in this module obstructs it.

Connectedness of |T| ∖ S needs at least one fresh point (hz₀ : z₀ ∈ fresh): with no spokes the rings are disjoint frames.

Blueprint

• ringSet, ringPieces, spokePiece, meshSegments — the mesh as a list of segments.
• meshGraph, squareMesh — Proposition "Anchored square mesh", the construction itself.
• FreshDense — the order-free form of "consecutive fresh points bound an arc of diameter < δ/4".
• squareMesh_face_small — clause 1: every bounded 2-cell has diameter < δ, and lies in Q.
• squareMesh_anchor_mem_vertexSet — clause 2: every boundary vertex survives.
• squareMesh_inner_edge_at_fresh, squareMesh_unique_inner_edge — clauses 3 and 4: a new internal edge meeting S ends at a fresh point, and exactly one such edge is incident with each fresh point.
• squareMesh_cover_outerEdges — the point-set half of "S is the outer cycle" (see above).
• squareMesh_isConnected_diff — clause 6: |T| ∖ S is connected.
• radial_diam_bound — the blueprint's radial estimate, isolated from all graph language.
• subdivide_covers_source, subdivide_end_of_mem — two general facts about subdivide that belong in Schoenflies/Subdivide.lean.

Rings: the frame of a square about the origin

def Schoenflies.ringSet (r : ℝ) : Set Plane

The frame of the square of radius r about the origin. For r = 1 this is definitionally modelCurve.

Equations

• Schoenflies.ringSet r = {x : Schoenflies.Plane | x.supNorm = r}

theorem Schoenflies.ringSet_one : ringSet 1 = modelCurve

def Schoenflies.ringPieces (r : ℝ) : List Piece

The four sides of the square of radius r, as a list of pieces.

Equations

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

theorem Schoenflies.segment_symm_Icc {r : ℝ} (hr : 0 ≤ r) : segment ℝ (-r) r = Set.Icc (-r) r

theorem Schoenflies.segment_symm_Icc' {r : ℝ} (hr : 0 ≤ r) : segment ℝ r (-r) = Set.Icc (-r) r

theorem Schoenflies.cover_ringPieces {r : ℝ} (hr : 0 ≤ r) : cover (ringPieces r) = ringSet r

The four sides of the square of radius r occupy exactly its frame.

theorem Schoenflies.mk_ne_mk_of_fst {a b c d : ℝ} (h : a ≠ c) : Plane.mk a b ≠ Plane.mk c d

theorem Schoenflies.mk_ne_mk_of_snd {a b c d : ℝ} (h : b ≠ d) : Plane.mk a b ≠ Plane.mk c d

theorem Schoenflies.ringPieces_nondeg {r : ℝ} (hr : 0 < r) (P : Piece) : P ∈ ringPieces r → P.Nondeg

A ring of positive radius has nondegenerate sides.

theorem Schoenflies.mem_ringSet_smul {t r : ℝ} (ht : 0 ≤ t) {x : Plane} (hx : x ∈ ringSet r) : t • x ∈ ringSet (t * r)

Scaling a ring: t • x has sup norm |t| times that of x.

theorem Schoenflies.supNorm_smul_of_mem_modelCurve {t : ℝ} (ht : 0 ≤ t) {z : Plane} (hz : z ∈ modelCurve) : (t • z).supNorm = t

theorem Schoenflies.inv_cast_lt_one {N : ℕ} (hN : 2 ≤ N) : (↑N)⁻¹ < 1

theorem Schoenflies.inv_cast_pos {N : ℕ} (hN : 2 ≤ N) : 0 < (↑N)⁻¹

Radial segments

Every point of a segment between two multiples of z is itself a multiple of z, with the coefficient running through the corresponding real segment. This is the only fact about spokes the whole module uses: along a spoke the coefficient — equivalently, by supNorm_smul_of_mem_modelCurve, the sup norm — is a faithful coordinate.

theorem Schoenflies.mem_smul_segment {a b : ℝ} {z x : Plane} : x ∈ segment ℝ (a • z) (b • z) ↔ ∃ t ∈ segment ℝ a b, x = t • z

theorem Schoenflies.smul_segment_eq_image {a b : ℝ} (hab : a ≤ b) (z : Plane) : segment ℝ (a • z) (b • z) = (fun (t : ℝ) => t • z) '' Set.Icc a b

The radial segment from a • z to b • z, as a set of multiples of z.

Spokes

noncomputable def Schoenflies.spokePiece (N : ℕ) (z : Plane) : Piece

The radial spoke at a boundary point z, running from z inwards to N⁻¹ • z.

Equations

• Schoenflies.spokePiece N z = (z, (↑N)⁻¹ • z)

theorem Schoenflies.spokePiece_seg {N : ℕ} (hN : 2 ≤ N) (z : Plane) : (spokePiece N z).seg = (fun (t : ℝ) => t • z) '' Set.Icc (↑N)⁻¹ 1

A spoke is the set of multiples t • z with N⁻¹ ≤ t ≤ 1.

theorem Schoenflies.spokePiece_inter_modelCurve {N : ℕ} (hN : 2 ≤ N) {z : Plane} (hz : z ∈ modelCurve) : (spokePiece N z).seg ∩ modelCurve = {z}

A spoke meets the model curve exactly at its outer end.

theorem Schoenflies.spokePiece_subset_closedSquare {N : ℕ} (hN : 2 ≤ N) {z : Plane} (hz : z ∈ modelCurve) : (spokePiece N z).seg ⊆ Plane.closedSquare 0 1

A spoke lies inside the closed square.

theorem Schoenflies.spokePiece_nondeg {N : ℕ} (hN : 2 ≤ N) {z : Plane} (hz : z ∈ modelCurve) : (spokePiece N z).Nondeg

Two more facts about subdivide

Both are general and belong beside the others in Schoenflies/Subdivide.lean; they are here because that module is on main.

subdivide_covers_source refines subdivide_cover: a point of a named source piece lies on a piece of the subdivision inside that source. Without the "inside that source" clause one cannot tell, of a point where two sources cross, which of them the piece through it came from — and the whole description of the mesh's edges is by their source.

subdivide_end_of_mem is the converse of subdivide_avoids: a cut point that lies on a source piece is not merely absent from every interior, it is an endpoint of a piece inside that source. That is what makes a prescribed point a vertex of the overlay graph.

theorem Schoenflies.cover_map {α : Type u_1} (f : α → Piece) (l : List α) : cover (List.map f l) = ⋃ a ∈ l, (f a).seg

theorem Schoenflies.cover_flatMap' {α : Type u_1} (f : α → List Piece) (l : List α) : cover (List.flatMap f l) = ⋃ a ∈ l, cover (f a)

theorem Schoenflies.mem_cover_iff {x : Plane} {l : List Piece} : x ∈ cover l ↔ ∃ P ∈ l, x ∈ P.seg

theorem Schoenflies.splitAt_end_of_mem (p : Plane) (P : Piece) (hmem : p ∈ P.seg) : ∃ R ∈ splitAt p P, R.seg ⊆ P.seg ∧ (p = R.1 ∨ p = R.2)

Cutting a piece at a point of it makes that point an endpoint of one of the halves.

theorem Schoenflies.splitAt_preserves_end (q : Plane) {p : Plane} {P : Piece} (h : p = P.1 ∨ p = P.2) : ∃ R ∈ splitAt q P, R.seg ⊆ P.seg ∧ (p = R.1 ∨ p = R.2)

Cutting anywhere keeps an endpoint an endpoint.

theorem Schoenflies.splitAllAt_preserves_end (q : Plane) {p : Plane} {P : Piece} {pieces : List Piece} (h : ∃ R ∈ pieces, R.seg ⊆ P.seg ∧ (p = R.1 ∨ p = R.2)) : ∃ R ∈ splitAllAt q pieces, R.seg ⊆ P.seg ∧ (p = R.1 ∨ p = R.2)

theorem Schoenflies.subdivide_preserves_end (points : List Plane) {pieces : List Piece} {p : Plane} {P : Piece} (h : ∃ R ∈ pieces, R.seg ⊆ P.seg ∧ (p = R.1 ∨ p = R.2)) : ∃ R ∈ subdivide pieces points, R.seg ⊆ P.seg ∧ (p = R.1 ∨ p = R.2)

theorem Schoenflies.subdivide_covers_source (points : List Plane) (pieces : List Piece) (P : Piece) : P ∈ pieces → ∀ x ∈ P.seg, ∃ Q ∈ subdivide pieces points, x ∈ Q.seg ∧ Q.seg ⊆ P.seg

Every point of a source piece lies on a piece of the subdivision contained in that source.

theorem Schoenflies.subdivide_end_of_mem (points : List Plane) (pieces : List Piece) (p : Plane) : p ∈ points → ∀ P ∈ pieces, p ∈ P.seg → ∃ Q ∈ subdivide pieces points, Q.seg ⊆ P.seg ∧ (p = Q.1 ∨ p = Q.2)

A cut point on a source piece is an endpoint of a piece of the subdivision inside it.

Enlarging the list of cut points

Both cut-point conditions ask only that certain points be in the list, so both survive adding more. That is what lets the mesh prescribe extra vertices — the anchors — on top of the cut points the overlay itself needs.

theorem Schoenflies.EndsAreCut.mono {pieces : List Piece} {points points' : List Plane} (h : EndsAreCut pieces points) (hsub : points ⊆ points') : EndsAreCut pieces points'

theorem Schoenflies.MeetsAreCut.mono {pieces : List Piece} {points points' : List Plane} (h : MeetsAreCut pieces points) (hsub : points ⊆ points') : MeetsAreCut pieces points'

The mesh, as a list of segments

N concentric ring frames of radii 1/N, 2/N, …, 1, and one full-length radial spoke at each fresh boundary point. There is no rectangular grid: the innermost region is the square of radius 1/N, which is a single cell of diameter 2√2/N, so filling it is unnecessary once N is large. That is the one deviation from the blueprint's construction, and it removes the whole "choose horizontal and vertical coordinates" step.

noncomputable def Schoenflies.meshRadii (N : ℕ) : List ℝ

The radii of the N concentric rings, 1/N, 2/N, …, 1.

Equations

• Schoenflies.meshRadii N = List.map (fun (j : ℕ) => (↑j + 1) / ↑N) (List.range N)

theorem Schoenflies.mem_meshRadii {N : ℕ} {r : ℝ} : r ∈ meshRadii N ↔ ∃ j < N, r = (↑j + 1) / ↑N

theorem Schoenflies.meshRadii_pos {N : ℕ} (hN : 2 ≤ N) {r : ℝ} (hr : r ∈ meshRadii N) : 0 < r

theorem Schoenflies.meshRadii_le_one {N : ℕ} (hN : 2 ≤ N) {r : ℝ} (hr : r ∈ meshRadii N) : r ≤ 1

theorem Schoenflies.one_mem_meshRadii {N : ℕ} (hN : 2 ≤ N) : 1 ∈ meshRadii N

theorem Schoenflies.inv_mem_meshRadii {N : ℕ} (hN : 2 ≤ N) : (↑N)⁻¹ ∈ meshRadii N

noncomputable def Schoenflies.meshSegments (N : ℕ) (fresh : List Plane) : List Piece

The mesh: the four sides of each ring, and one radial spoke at each fresh point.

Equations

• Schoenflies.meshSegments N fresh = List.flatMap Schoenflies.ringPieces (Schoenflies.meshRadii N) ++ List.map (Schoenflies.spokePiece N) fresh

theorem Schoenflies.mem_meshSegments {N : ℕ} {fresh : List Plane} {P : Piece} : P ∈ meshSegments N fresh ↔ (∃ r ∈ meshRadii N, P ∈ ringPieces r) ∨ ∃ z ∈ fresh, P = spokePiece N z

theorem Schoenflies.cover_meshSegments {N : ℕ} (hN : 2 ≤ N) (fresh : List Plane) : cover (meshSegments N fresh) = (⋃ r ∈ meshRadii N, ringSet r) ∪ ⋃ z ∈ fresh, (spokePiece N z).seg

theorem Schoenflies.meshSegments_nondeg {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (P : Piece) : P ∈ meshSegments N fresh → P.Nondeg

theorem Schoenflies.ringPieces_seg_subset {r : ℝ} (hr : 0 ≤ r) {P : Piece} (hP : P ∈ ringPieces r) : P.seg ⊆ ringSet r

A side of a ring lies on that ring.

theorem Schoenflies.meshSegments_subset_closedSquare {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {P : Piece} (hP : P ∈ meshSegments N fresh) : P.seg ⊆ Plane.closedSquare 0 1

Every mesh segment lies inside the closed square.

The mesh as a plane graph

The cut points are the ones exists_cut_points supplies for the mesh segments, together with the prescribed anchors. Enlarging the list is harmless — EndsAreCut.mono and MeetsAreCut.mono — and it is what makes each anchor a vertex.

noncomputable def Schoenflies.meshCutPoints (N : ℕ) (fresh : List Plane) : List Plane

Cut points for the mesh segments, as produced by exists_cut_points.

Equations

• Schoenflies.meshCutPoints N fresh = ⋯.choose

theorem Schoenflies.meshCutPoints_spec (N : ℕ) (fresh : List Plane) : EndsAreCut (meshSegments N fresh) (meshCutPoints N fresh) ∧ MeetsAreCut (meshSegments N fresh) (meshCutPoints N fresh)

noncomputable def Schoenflies.meshPoints (N : ℕ) (fresh anchors : List Plane) : List Plane

The cut points of the mesh: what the overlay needs, plus the prescribed anchors.

Equations

• Schoenflies.meshPoints N fresh anchors = anchors ++ Schoenflies.meshCutPoints N fresh

theorem Schoenflies.meshPoints_endsAreCut (N : ℕ) (fresh anchors : List Plane) : EndsAreCut (meshSegments N fresh) (meshPoints N fresh anchors)

theorem Schoenflies.meshPoints_meetsAreCut (N : ℕ) (fresh anchors : List Plane) : MeetsAreCut (meshSegments N fresh) (meshPoints N fresh anchors)

theorem Schoenflies.anchors_subset_meshPoints (N : ℕ) (fresh anchors : List Plane) : anchors ⊆ meshPoints N fresh anchors

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

The mesh graph.

Equations

• Schoenflies.meshGraph N fresh anchors = Schoenflies.overlayGraph (Schoenflies.meshSegments N fresh) (Schoenflies.meshPoints N fresh anchors)

instance Schoenflies.meshGraph_finite (N : ℕ) (fresh anchors : List Plane) : (meshGraph N fresh anchors).Finite

theorem Schoenflies.meshGraph_isDrawing {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (anchors : List Plane) : (meshGraph N fresh anchors).IsDrawing segmentDrawing

theorem Schoenflies.meshGraph_pointSet (N : ℕ) (fresh anchors : List Plane) : (meshGraph N fresh anchors).pointSet segmentDrawing = cover (meshSegments N fresh)

theorem Schoenflies.meshGraph_edge_source {N : ℕ} {fresh anchors : List Plane} {P : Piece} (hP : P ∈ (meshGraph N fresh anchors).edgeSet) : ∃ R ∈ meshSegments N fresh, P.seg ⊆ R.seg

An edge of the mesh graph is a subsegment of a mesh segment.

theorem Schoenflies.meshGraph_edge_nondeg {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {anchors : List Plane} {P : Piece} (hP : P ∈ (meshGraph N fresh anchors).edgeSet) : P.Nondeg

theorem Schoenflies.meshGraph_mem_vertexSet {N : ℕ} {fresh anchors : List Plane} {v : Plane} : v ∈ (meshGraph N fresh anchors).vertexSet ↔ ∃ P ∈ (meshGraph N fresh anchors).edgeSet, v = P.1 ∨ v = P.2

theorem Schoenflies.outer_ringPieces_mem {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} {R : Piece} (hR : R ∈ ringPieces 1) : R ∈ meshSegments N fresh

A side of the outer ring is a mesh segment.

theorem Schoenflies.spokePiece_mem_meshSegments {N : ℕ} {fresh : List Plane} {z : Plane} (hz : z ∈ fresh) : spokePiece N z ∈ meshSegments N fresh

theorem Schoenflies.fresh_mem_meshPoints {N : ℕ} {fresh : List Plane} (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) : z ∈ meshPoints N fresh anchors

A fresh point is a cut point: it is an endpoint of its own spoke.

Clause 2: the anchors are vertices on S

theorem Schoenflies.anchor_mem_vertexSet {N : ℕ} (hN : 2 ≤ N) {fresh anchors : List Plane} {p : Plane} (hp : p ∈ anchors) (hpS : p ∈ modelCurve) : p ∈ (meshGraph N fresh anchors).vertexSet

Every prescribed anchor on S is a vertex of the mesh. This is what the list of anchors is for: subdivide_end_of_mem turns "is a cut point on a segment" into "is an endpoint of a piece", and an endpoint of a piece is a vertex of the overlay graph.

Clause 3: the outer edges occupy exactly S

The blueprint asks for S to be the union of the edge arcs of a cycle. What is proved here is the point-set half: the edges whose arcs lie on S occupy exactly S. See the module docstring.

def Schoenflies.outerEdges (N : ℕ) (fresh anchors : List Plane) : Set Piece

The edges of the mesh that lie on the model curve.

Equations

• Schoenflies.outerEdges N fresh anchors = {P : Schoenflies.Piece | P ∈ (Schoenflies.meshGraph N fresh anchors).edgeSet ∧ P.seg ⊆ Schoenflies.modelCurve}

theorem Schoenflies.cover_outerEdges {N : ℕ} (hN : 2 ≤ N) (fresh anchors : List Plane) : ⋃ P ∈ outerEdges N fresh anchors, P.seg = modelCurve

The outer edges occupy exactly the model curve.

Clause 4: the edges that reach S from inside

An edge of the mesh that meets S without lying on it is a subsegment of a spoke, and it touches S at that spoke's fresh point only.

theorem Schoenflies.ringSet_disjoint_modelCurve {r : ℝ} (hr : r ≠ 1) : ringSet r ∩ modelCurve = ∅

theorem Schoenflies.smul_left_inj {t s : ℝ} (ht : 0 ≤ t) (hs : 0 ≤ s) {z : Plane} (hz : z ∈ modelCurve) (h : t • z = s • z) : t = s

theorem Schoenflies.meshGraph_inner_edge_at_fresh {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {anchors : List Plane} {P : Piece} (hP : P ∈ (meshGraph N fresh anchors).edgeSet) (hmeet : (P.seg ∩ modelCurve).Nonempty) (hnot : ¬P.seg ⊆ modelCurve) : ∃ z ∈ fresh, P.seg ∩ modelCurve = {z} ∧ (z = P.1 ∨ z = P.2) ∧ P.seg ⊆ (spokePiece N z).seg

An edge that meets S but does not lie on it is a piece of a spoke, and it meets S exactly at that spoke's fresh point, which is one of its endpoints.

theorem Schoenflies.mem_smul_openSegment {a b : ℝ} {z x : Plane} : x ∈ openSegment ℝ (a • z) (b • z) ↔ ∃ t ∈ openSegment ℝ a b, x = t • z

theorem Schoenflies.smul_openSegment_eq_image {a b : ℝ} (hab : a < b) (z : Plane) : openSegment ℝ (a • z) (b • z) = (fun (t : ℝ) => t • z) '' Set.Ioo a b

theorem Schoenflies.spoke_subpiece_interior {N : ℕ} (hN : 2 ≤ N) {z : Plane} {P : Piece} (hnd : P.Nondeg) (hsub : P.seg ⊆ (spokePiece N z).seg) (hend : z = P.1 ∨ z = P.2) : ∃ t₀ < 1, P.interior = (fun (t : ℝ) => t • z) '' Set.Ioo t₀ 1

A nondegenerate subsegment of a spoke having the spoke's outer end z as an endpoint runs from z inwards: its interior is {t • z : t₀ < t < 1} for some t₀ < 1. This is the whole of "only one edge leaves S at a fresh point" — two such edges would overlap near z.

theorem Schoenflies.exists_inner_edge_at_fresh {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ w ∈ fresh, w ∈ modelCurve) (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) : ∃ P ∈ (meshGraph N fresh anchors).edgeSet, (z = P.1 ∨ z = P.2) ∧ ¬P.seg ⊆ modelCurve ∧ P.seg ⊆ (spokePiece N z).seg

Existence for clause 4: a fresh point does carry an edge leaving S.

theorem Schoenflies.inner_edge_at_fresh_unique {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {anchors : List Plane} {z : Plane} (hz : z ∈ fresh) {P Q : Piece} (hP : P ∈ (meshGraph N fresh anchors).edgeSet) (hendP : z = P.1 ∨ z = P.2) (hnotP : ¬P.seg ⊆ modelCurve) (hQ : Q ∈ (meshGraph N fresh anchors).edgeSet) (hendQ : z = Q.1 ∨ z = Q.2) (hnotQ : ¬Q.seg ⊆ modelCurve) : P = Q

Uniqueness for clause 4: exactly one edge leaves S at a fresh point.

theorem Schoenflies.unique_inner_edge_at_fresh {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) : ∃! P : Piece, P ∈ (meshGraph N fresh anchors).edgeSet ∧ (z = P.1 ∨ z = P.2) ∧ ¬P.seg ⊆ modelCurve

Clause 4. Exactly one edge of the mesh leaves S at each fresh point.

Clause 1: every bounded face is small

The estimate is the blueprint's, in radial coordinates. A connected set missing the mesh misses every ring, so its sup norm — continuous, hence with a preconnected image in ℝ — stays inside one open interval (k/N, (k+1)/N) between consecutive ring radii. Inside the innermost square that is already the whole bound; outside it the radial projection x ↦ ‖x‖∞⁻¹ • x maps the set into S, connectedly, and away from every fresh point, because a point projecting to a fresh point lies on that point's spoke. The blueprint's

‖x - y‖ ≤ ‖tz - tw‖ + ‖tw - sw‖ < δ/4 + δ/4 + δ/4

is then t‖z - w‖ + |t - s|‖w‖, with ‖z - w‖ controlled by FreshDense and |t - s| by one ring thickness.

theorem Schoenflies.continuous_supNorm : Continuous Plane.supNorm

theorem Schoenflies.supNorm_sub_le (x y : Plane) : (x - y).supNorm ≤ x.supNorm + y.supNorm

theorem Schoenflies.dist_le_sqrt_two_mul_supNorm (x y : Plane) : dist x y ≤ √2 * (x - y).supNorm

def Schoenflies.FreshDense (fresh : List Plane) (δ : ℝ) : Prop

The fresh points are δ-dense on S: every connected piece of S that avoids all of them has diameter at most δ/2.

This is the hypothesis the blueprint discharges by "parametrize S by a circle, use uniform continuity to cut it into arcs of diameter < δ/8, and pick one fresh point in the relative interior of each". Stated as a property of a set rather than of a cyclic order, it needs no ordering of the fresh points along S — which is what makes the whole mesh order-free.

Equations

• Schoenflies.FreshDense fresh δ = ∀ A ⊆ Schoenflies.modelCurve \ {x : Schoenflies.Plane | x ∈ fresh}, IsPreconnected A → ∀ x ∈ A, ∀ y ∈ A, dist x y ≤ δ / 2

theorem Schoenflies.ringSet_subset_cover {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} {r : ℝ} (hr : r ∈ meshRadii N) : ringSet r ⊆ cover (meshSegments N fresh)

theorem Schoenflies.spokePiece_seg_subset_cover {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} {z : Plane} (hz : z ∈ fresh) : (spokePiece N z).seg ⊆ cover (meshSegments N fresh)

theorem Schoenflies.radial_diam_bound {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} {δ : ℝ} (hNδ : 2 * √2 ≤ δ * ↑N) (hdense : FreshDense fresh δ) {F : Set Plane} (hconn : IsPreconnected F) (hdisj : ∀ x ∈ F, x ∉ cover (meshSegments N fresh)) {base : Plane} (hb : base ∈ F) (hbase : base.supNorm < 1) : (∀ x ∈ F, x.supNorm < 1) ∧ ∀ x ∈ F, ∀ y ∈ F, dist x y ≤ δ / 2 + √2 / ↑N

The radial estimate. A connected set missing the mesh stays inside the open square and has diameter at most δ/2 + √2/N.

theorem Schoenflies.cover_meshSegments_subset {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) : cover (meshSegments N fresh) ⊆ Plane.closedSquare 0 1

The mesh occupies a subset of the closed square.

theorem Schoenflies.meshGraph_face_small {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {anchors : List Plane} {δ : ℝ} (hδ : 0 < δ) (hNδ : 2 * √2 < δ * ↑N) (hdense : FreshDense fresh δ) {base : Plane} (hbase : base ∈ (meshGraph N fresh anchors).exterior segmentDrawing) (hbdd : Bornology.IsBounded ((meshGraph N fresh anchors).face segmentDrawing base)) : (meshGraph N fresh anchors).face segmentDrawing base ⊆ Plane.openSquare 0 1 ∧ Metric.diam ((meshGraph N fresh anchors).face segmentDrawing base) < δ

Clause 1. Every bounded face of the mesh lies in the open square and has diameter < δ.

Clause 5: the mesh minus S is connected

The inner rings and the spokes-minus-their-outer-endpoint are each connected, every inner ring meets every spoke, and every spoke meets the innermost ring. So a single point of the innermost ring reaches everything, which is what isPreconnected_of_forall asks for. At least one fresh point is needed: with no spokes the rings are disjoint circles.

noncomputable def Schoenflies.halfSpoke (N : ℕ) (z : Plane) : Set Plane

A spoke with its outer endpoint removed.

Equations

• Schoenflies.halfSpoke N z = (fun (t : ℝ) => t • z) '' Set.Ico (↑N)⁻¹ 1

theorem Schoenflies.isConnected_halfSpoke {N : ℕ} (hN : 2 ≤ N) (z : Plane) : IsConnected (halfSpoke N z)

theorem Schoenflies.halfSpoke_subset {N : ℕ} (hN : 2 ≤ N) (z : Plane) : halfSpoke N z ⊆ (spokePiece N z).seg

theorem Schoenflies.halfSpoke_disjoint_modelCurve {N : ℕ} (hN : 2 ≤ N) {z : Plane} (hz : z ∈ modelCurve) (x : Plane) : x ∈ halfSpoke N z → x ∉ modelCurve

theorem Schoenflies.smul_mem_halfSpoke {N : ℕ} {t : ℝ} (ht : (↑N)⁻¹ ≤ t) (ht1 : t < 1) (z : Plane) : t • z ∈ halfSpoke N z

theorem Schoenflies.isConnected_ringSet {r : ℝ} (hr : 0 ≤ r) : IsConnected (ringSet r)

The frame of a square is connected: four segments in a cycle, meeting at the corners.

theorem Schoenflies.isConnected_cover_diff_modelCurve {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {z₀ : Plane} (hz₀ : z₀ ∈ fresh) : IsConnected (cover (meshSegments N fresh) \ modelCurve)

Clause 5. The mesh with S removed is connected.

The mesh of a given size

meshCount δ rings make both the innermost square and one ring thickness small compared with δ; 2 √2 < δ N is the single inequality the whole diameter estimate rests on.

noncomputable def Schoenflies.meshCount (δ : ℝ) : ℕ

The number of concentric rings used for mesh size δ.

Equations

• Schoenflies.meshCount δ = max 2 (⌈2 * √2 / δ⌉₊ + 1)

theorem Schoenflies.two_le_meshCount (δ : ℝ) : 2 ≤ meshCount δ

theorem Schoenflies.meshCount_spec {δ : ℝ} (hδ : 0 < δ) : 2 * √2 < δ * ↑(meshCount δ)

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

The anchored square mesh: meshCount δ concentric ring frames inside Q = [-1,1]², one radial spoke at each fresh boundary point, and the anchors inserted as extra vertices of the outer ring.

Equations

• Schoenflies.squareMesh δ fresh anchors = Schoenflies.meshGraph (Schoenflies.meshCount δ) fresh anchors

instance Schoenflies.squareMesh_finite (δ : ℝ) (fresh anchors : List Plane) : (squareMesh δ fresh anchors).Finite

theorem Schoenflies.squareMesh_isDrawing {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) : (squareMesh δ fresh anchors).IsDrawing segmentDrawing

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

theorem Schoenflies.squareMesh_pointSet (δ : ℝ) (fresh anchors : List Plane) : (squareMesh δ fresh anchors).pointSet segmentDrawing = cover (meshSegments (meshCount δ) fresh)

theorem Schoenflies.modelCurve_subset_squareMesh_pointSet (δ : ℝ) (fresh anchors : List Plane) : modelCurve ⊆ (squareMesh δ fresh anchors).pointSet segmentDrawing

The whole model curve is part of the mesh.

theorem Schoenflies.squareMesh_pointSet_subset {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) : (squareMesh δ fresh anchors).pointSet segmentDrawing ⊆ Plane.closedSquare 0 1

The mesh occupies a subset of Q.

theorem Schoenflies.squareMesh_face_small {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {δ : ℝ} (hδ : 0 < δ) (hdense : FreshDense fresh δ) {anchors : List Plane} {base : Plane} (hbase : base ∈ (squareMesh δ fresh anchors).exterior segmentDrawing) (hbdd : Bornology.IsBounded ((squareMesh δ fresh anchors).face segmentDrawing base)) : (squareMesh δ fresh anchors).face segmentDrawing base ⊆ Plane.openSquare 0 1 ∧ Metric.diam ((squareMesh δ fresh anchors).face segmentDrawing base) < δ

Clause 1. Every bounded face lies in the open square and has diameter < δ.

theorem Schoenflies.squareMesh_anchor_mem_vertexSet (δ : ℝ) {fresh anchors : List Plane} {p : Plane} (hp : p ∈ anchors) (hpS : p ∈ modelCurve) : p ∈ (squareMesh δ fresh anchors).vertexSet

Clause 2. Every anchor lying on S is a vertex.

theorem Schoenflies.squareMesh_cover_outerEdges (δ : ℝ) (fresh anchors : List Plane) : ⋃ P ∈ outerEdges (meshCount δ) fresh anchors, P.seg = modelCurve

Clause 3. The edges lying on S occupy exactly S.

theorem Schoenflies.squareMesh_inner_edge_at_fresh {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) {anchors : List Plane} {P : Piece} (hP : P ∈ (squareMesh δ fresh anchors).edgeSet) (hmeet : (P.seg ∩ modelCurve).Nonempty) (hnot : ¬P.seg ⊆ modelCurve) : ∃ z ∈ fresh, P.seg ∩ modelCurve = {z} ∧ (z = P.1 ∨ z = P.2) ∧ P.seg ⊆ (spokePiece (meshCount δ) z).seg

Clause 4, first half. An edge meeting S without lying on it meets it in a single fresh point, which is one of its endpoints.

theorem Schoenflies.squareMesh_unique_inner_edge {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) {z : Plane} (hz : z ∈ fresh) : ∃! P : Piece, P ∈ (squareMesh δ fresh anchors).edgeSet ∧ (z = P.1 ∨ z = P.2) ∧ ¬P.seg ⊆ modelCurve

Clause 4, second half. Exactly one edge leaves S at each fresh point.

theorem Schoenflies.squareMesh_isConnected_diff {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (δ : ℝ) (anchors : List Plane) {z₀ : Plane} (hz₀ : z₀ ∈ fresh) : IsConnected ((squareMesh δ fresh anchors).pointSet segmentDrawing \ modelCurve)

Clause 5. The mesh minus S is connected.