The local source grid, and the missing hypothesis of the anchored square mesh

Two things, and the second is the more important.

1. prop:anchored-square-mesh clause 5 — which hypothesis repairs it

docs/ROADMAP.md records clause 5, the skeleton of T is 2-connected, as false for Schoenflies.squareMesh when the fresh-point set is too small, and names Schoenflies.FreshDense as "the shape the missing hypothesis should take". The first section of this module checks that, and the answer is no: FreshDense alone does not repair clause 5.

• Schoenflies.freshDense_of_four_sqrt_two_le — for 4√2 ≤ δ, FreshDense fresh δ holds for every list fresh, the empty one included, because S itself has diameter 2√2. So FreshDense fresh δ is vacuous at large δ and excludes nothing.
• Schoenflies.freshDense_not_isTwoConnected — the counterexample made formal: at δ = 4√2 the hypotheses 0 < δ and FreshDense [] δ both hold and squareMesh δ [] anchors is still not 2-connected.

What does repair it is FreshDense together with a bound on δ:

• Schoenflies.exists_two_distinct_fresh_of_freshDense — FreshDense fresh δ and δ < 4 force two distinct fresh points. (4 is not the sharp constant — 4√2 is — but it is the one a side of S, whose two ends are 2 apart, gives with no work. The blueprint's own δ = ε_n = 2^{-n} is far below either.)

and two distinct fresh points is exactly the right amount, because fewer is always fatal:

• Schoenflies.not_isTwoConnected_meshGraph_of_fresh_subsingleton — a mesh whose fresh points are not two distinct points is never 2-connected. This closes the case SquareMeshFixed.lean left open in prose: with exactly one fresh point z the mesh is connected, but z is a cut vertex, because the spoke at z is the only edge of the mesh that changes the sup norm and every other edge preserves it.

So the correct statement of clause 5 carries the hypothesis ∃ z ∈ fresh, ∃ w ∈ fresh, z ≠ w, which FreshDense fresh δ ∧ δ < 4 supplies, and which is necessary as well as sufficient in the degenerate range.

2. prop:local-grid-attachment — the grid

The blueprint's proof begins: "Choose sufficiently fine finite horizontal and vertical coordinate sets in W, with at least two intervals in each direction. Begin with the outer rectangle of the resulting grid K … By lem:subdivision-ear-preserve, K is 2-connected."

Schoenflies.localGrid is that K, as a def: the uniform k × k grid on the closed square W of centre p and radius s. Schoenflies/SquareMeshConnected.lean and Schoenflies/SquareMeshFixed.lean supply everything combinatorial about a grid, so what is added here is the quantitative clause the proposition needs — every closed grid rectangle has diameter < ε — together with the instantiation of the general grid lemmas at these coordinates.

The rest of prop:local-grid-attachment — the overlay of K with the polygonal nonboundary skeleton of Γ, the three cases, and the component-joining loop — is not here; see the report.

Blueprint

• prop:anchored-square-mesh, clause 5 — freshDense_of_four_sqrt_two_le, freshDense_not_isTwoConnected, exists_two_distinct_fresh_of_freshDense, not_isTwoConnected_meshGraph_of_fresh_subsingleton, not_isTwoConnected_squareMesh_of_fresh_subsingleton.
• prop:local-grid-attachment, the grid K — localGrid, localGrid_isTwoConnected, localGrid_subdivide_isTwoConnected, localGrid_isDrawing, localGrid_outer_cycle.
• prop:local-grid-attachment, clause 3 — dist_le_of_mem_localGridCell (the closed grid rectangle), dist_lt_of_avoiding_localGrid (a connected subset of W missing the grid), localGridCount, localGridCount_spec, localGrid_fine.
• lem:union-two-connected — used through Graph.IsTwoConnected.union and Graph.IsTwoConnected.ear; Graph.IsTwoConnected.of_le_of_vertexSet_subset is the "spanning 2-connected subgraph" form the assembly needs.

The diameter of S

S = modelCurve is the frame of [-1,1]², so any two of its points are at sup distance at most 2 and hence at Euclidean distance at most 2√2. That single bound is what makes FreshDense fresh δ vacuous once δ ≥ 4√2.

theorem Schoenflies.supDist_le_dist (x y : Plane) : x.supDist y ≤ dist x y

The sup distance is at most the Euclidean distance.

theorem Schoenflies.dist_le_of_mem_modelCurve {x y : Plane} (hx : x ∈ modelCurve) (hy : y ∈ modelCurve) : dist x y ≤ 2 * √2

Any two points of S are within 2√2.

theorem Schoenflies.freshDense_of_four_sqrt_two_le {fresh : List Plane} {δ : ℝ} (hδ : 4 * √2 ≤ δ) : FreshDense fresh δ

FreshDense is vacuous at large δ. For δ ≥ 4√2 every list of fresh points is δ-dense, the empty one included: the whole of S has diameter 2√2 ≤ δ/2.

This is the first half of the finding: FreshDense alone cannot be the missing hypothesis of prop:anchored-square-mesh clause 5, because it does not exclude fresh = [].

theorem Schoenflies.freshDense_not_isTwoConnected (anchors : List Plane) : ∃ (δ : ℝ), 0 < δ ∧ FreshDense [] δ ∧ ¬(squareMesh δ [] anchors).IsTwoConnected

The counterexample, formally. There is a positive δ for which FreshDense [] δ holds and the mesh is still not 2-connected. So clause 5 is not repaired by adding FreshDense alone.

What does repair clause 5

A side of S is a connected subset of S whose two ends are 2 apart. If no two fresh points are distinct then some side avoids all of them — a single point cannot lie on both the top and the bottom side — and FreshDense fresh δ applied to that side forces 4 ≤ δ.

theorem Schoenflies.two_le_dist_side {P : Piece} (h : P = sideT ∨ P = sideB) : 2 ≤ dist P.1 P.2

The two ends of the top or the bottom side of S are at distance at least 2.

theorem Schoenflies.exists_side_avoiding (fresh : List Plane) (hsub : ∀ z ∈ fresh, ∀ w ∈ fresh, z = w) : ∃ (P : Piece), (P = sideT ∨ P = sideB) ∧ ∀ z ∈ fresh, z ∉ P.seg

A single point cannot lie on both horizontal sides of S, so one of them avoids a one-point set.

theorem Schoenflies.exists_two_distinct_fresh_of_freshDense {fresh : List Plane} {δ : ℝ} (hdense : FreshDense fresh δ) (hδ : δ < 4) : ∃ z ∈ fresh, ∃ w ∈ fresh, z ≠ w

FreshDense with a small δ gives two distinct fresh points. This is the hypothesis prop:anchored-square-mesh clause 5 actually needs, and the blueprint supplies it: its δ = ε_n = 2^{-n} is well below 4.

Fewer than two distinct fresh points is always fatal

SquareMeshFixed.not_isTwoConnected_squareMesh_of_fresh_nil settles fresh = [] by showing the mesh disconnected. The remaining degenerate case — exactly one fresh point — is settled here, and by the same invariant.

Every edge of the mesh is a subsegment of a source segment, and a source segment is either a side of a ring, on which the sup norm is constant, or the spoke at a fresh point z, along which the only point of sup norm 1 is z itself. So once z is deleted, no edge of the mesh joins a vertex of sup norm 1 to a vertex of smaller sup norm: z is a cut vertex.

theorem Schoenflies.supNorm_eq_one_iff_of_isLink {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (hsub : ∀ u ∈ fresh, ∀ w ∈ fresh, u = w) {anchors : List Plane} {z : Plane} (hz : z ∈ fresh) {P : Piece} {x y : Plane} (h : (meshGraph N fresh anchors).IsLink P x y) (hx : x ≠ z) (hy : y ≠ z) : x.supNorm = 1 ↔ y.supNorm = 1

Along an edge of the mesh whose ends are both different from the one fresh point z, the predicate "sup norm is 1" is constant.

theorem Schoenflies.corner_mem_vertexSet_meshGraph {N : ℕ} (hN : 2 ≤ N) {fresh anchors : List Plane} {R : Piece} (hR : R ∈ ringPieces 1) : R.1 ∈ (meshGraph N fresh anchors).vertexSet

An end of a side of the outer ring is a vertex of the mesh.

theorem Schoenflies.supNorm_corner_pp : (Plane.mk 1 1).supNorm = 1

theorem Schoenflies.supNorm_corner_mm : (Plane.mk (-1) (-1)).supNorm = 1

theorem Schoenflies.exists_outer_vertex_ne {N : ℕ} (hN : 2 ≤ N) {fresh anchors : List Plane} (z : Plane) : ∃ c ∈ (meshGraph N fresh anchors).vertexSet, c.supNorm = 1 ∧ c ≠ z

Whichever point z is, one of the two corners (1,1), (-1,-1) differs from it and is a vertex of the mesh of sup norm 1.

theorem Schoenflies.exists_inner_vertex {N : ℕ} (hN : 2 ≤ N) {fresh anchors : List Plane} : ∃ c ∈ (meshGraph N fresh anchors).vertexSet, c.supNorm ≠ 1

The corner of the innermost ring is a vertex of the mesh, and its sup norm is not 1.

theorem Schoenflies.not_isTwoConnected_meshGraph_of_fresh_subsingleton {N : ℕ} (hN : 2 ≤ N) {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (hsub : ∀ u ∈ fresh, ∀ w ∈ fresh, u = w) (anchors : List Plane) : ¬(meshGraph N fresh anchors).IsTwoConnected

A mesh whose fresh points are not two distinct points is never 2-connected. With none the mesh is disconnected (not_connected_meshGraph_of_fresh_nil); with one, z, the point z is a cut vertex.

This is the second half of the finding: two distinct fresh points is not merely a convenient hypothesis for clause 5, it is a necessary one.

theorem Schoenflies.not_isTwoConnected_squareMesh_of_fresh_subsingleton {fresh : List Plane} (hfresh : ∀ u ∈ fresh, u ∈ modelCurve) (hsub : ∀ u ∈ fresh, ∀ w ∈ fresh, u = w) (δ : ℝ) (anchors : List Plane) : ¬(squareMesh δ fresh anchors).IsTwoConnected

prop:anchored-square-mesh clause 5 needs two distinct fresh points, for Schoenflies.squareMesh itself.

A spanning 2-connected subgraph makes the whole graph 2-connected

The form in which every assembly out of lem:union-two-connected is finished: a chain of unions produces some graph, and what the consumer wants is 2-connectivity of the graph it started from. As long as the assembled graph is a subgraph that misses no vertex, the two coincide — extra edges can only help connectivity.

theorem Graph.Connected.of_spanning_le {α : Type u_1} {β : Type u_2} {H K : Graph α β} (hH : H.Connected) (hHK : H ≤ K) (hV : K.vertexSet ⊆ H.vertexSet) : K.Connected

Connectedness passes up to a graph with the same vertices.

theorem Graph.IsTwoConnected.of_le_of_vertexSet_subset {α : Type u_1} {β : Type u_2} {H K : Graph α β} (hH : H.IsTwoConnected) (hHK : H ≤ K) (hV : K.vertexSet ⊆ H.vertexSet) : K.IsTwoConnected

2-connectivity passes up to a graph with the same vertices.

Uniform coordinates

prop:local-grid-attachment asks for "sufficiently fine finite horizontal and vertical coordinate sets in W, with at least two intervals in each direction". Equally spaced ones serve, and they make the fineness a single division.

noncomputable def Schoenflies.uniformCoord (a h : ℝ) (i : ℕ) : ℝ

The i-th of the equally spaced coordinates starting at a with step h.

Equations

• Schoenflies.uniformCoord a h i = a + ↑i * h

@[simp]

theorem Schoenflies.uniformCoord_zero (a h : ℝ) : uniformCoord a h 0 = a

theorem Schoenflies.uniformCoord_strictMono {h : ℝ} (hh : 0 < h) (a : ℝ) : StrictMono (uniformCoord a h)

theorem Schoenflies.uniformCoord_le {h : ℝ} (hh : 0 < h) (a : ℝ) {i j : ℕ} (hij : i ≤ j) : uniformCoord a h i ≤ uniformCoord a h j

theorem Schoenflies.abs_sub_lt_of_avoiding {a h : ℝ} (hh : 0 < h) {k : ℕ} {I : Set ℝ} (hI : IsPreconnected I) (hIsub : I ⊆ Set.Icc a (a + ↑k * h)) (havoid : ∀ i ≤ k, uniformCoord a h i ∉ I) {x y : ℝ} (hx : x ∈ I) (hy : y ∈ I) : |x - y| < h

A preconnected set of reals inside [a, a + k·h] that avoids every coordinate a + i·h has diameter less than h. Two of its points more than h apart would straddle one of the coordinates, and a preconnected subset of ℝ contains the interval between any two of its points.

The local grid

prop:local-grid-attachment clauses 2 and 3: a rectangular grid on the window W, all of whose closed rectangles are smaller than ε. Everything combinatorial about it — that it is 2-connected, that it stays 2-connected after subdivision, that it is a plane graph and that its boundary is a distinguished cycle — comes from Schoenflies/SquareMeshConnected.lean and Schoenflies/SquareMeshFixed.lean; the content added here is the fineness.

noncomputable def Schoenflies.localGridX (p : Plane) (s : ℝ) (k : ℕ) : ℕ → ℝ

The x-coordinates of the local grid on the closed square of centre p and radius s, cut into k intervals.

Equations

• Schoenflies.localGridX p s k = Schoenflies.uniformCoord (p.ofLp 0 - s) (2 * s / ↑k)

noncomputable def Schoenflies.localGridY (p : Plane) (s : ℝ) (k : ℕ) : ℕ → ℝ

The y-coordinates of the local grid.

Equations

• Schoenflies.localGridY p s k = Schoenflies.uniformCoord (p.ofLp 1 - s) (2 * s / ↑k)

noncomputable def Schoenflies.localGridEdges (p : Plane) (s : ℝ) (k : ℕ) : List Piece

The edges of the local grid, as a list of segments.

Equations

• Schoenflies.localGridEdges p s k = Schoenflies.gridEdges (Schoenflies.localGridX p s k) (Schoenflies.localGridY p s k) k k

noncomputable def Schoenflies.localGrid (p : Plane) (s : ℝ) (k : ℕ) : Graph Plane Piece

The local grid of prop:local-grid-attachment: the uniform k × k rectangular grid on the closed square W of centre p and radius s.

Equations

• Schoenflies.localGrid p s k = Schoenflies.gridGraph (Schoenflies.localGridX p s k) (Schoenflies.localGridY p s k) k k

theorem Schoenflies.localGrid_eq (p : Plane) (s : ℝ) (k : ℕ) : localGrid p s k = pieceListGraph (localGridEdges p s k)

theorem Schoenflies.localGrid_step_pos {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) : 0 < 2 * s / ↑k

theorem Schoenflies.localGridX_strictMono {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) : StrictMono (localGridX p s k)

theorem Schoenflies.localGridY_strictMono {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) : StrictMono (localGridY p s k)

@[simp]

theorem Schoenflies.localGridX_zero (p : Plane) (s : ℝ) (k : ℕ) : localGridX p s k 0 = p.ofLp 0 - s

@[simp]

theorem Schoenflies.localGridY_zero (p : Plane) (s : ℝ) (k : ℕ) : localGridY p s k 0 = p.ofLp 1 - s

theorem Schoenflies.localGridX_last {p : Plane} {s : ℝ} {k : ℕ} (hk : 1 ≤ k) : localGridX p s k k = p.ofLp 0 + s

theorem Schoenflies.localGridY_last {p : Plane} {s : ℝ} {k : ℕ} (hk : 1 ≤ k) : localGridY p s k k = p.ofLp 1 + s

theorem Schoenflies.localGrid_isTwoConnected {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) : (localGrid p s k).IsTwoConnected

prop:local-grid-attachment: the grid K is 2-connected.

theorem Schoenflies.localGrid_subdivide_isTwoConnected {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) (points : List Plane) : (pieceListGraph (subdivide (localGridEdges p s k) points)).IsTwoConnected

The grid stays 2-connected after subdivision — the lem:subdivision-ear-preserve half of the blueprint's argument, at these coordinates. The overlay of K with the skeleton of Γ subdivides K at the crossing points, and no hypothesis on those points is needed.

theorem Schoenflies.localGrid_isDrawing {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) : (localGrid p s k).IsDrawing segmentDrawing

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

theorem Schoenflies.localGrid_outer_cycle {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) : (localGrid p s k).IsCycleThrough (gridBoundaryLast (localGridX p s k) (localGridY p s k) k k) (gridBoundaryPt (localGridX p s k) (localGridY p s k) k k 0) (gridBoundaryPt (localGridX p s k) (localGridY p s k) k k (2 * k + 2 * k - 1)) (gridBoundaryDetour (localGridX p s k) (localGridY p s k) k k) ∧ Graph.edgesCover segmentDrawing (gridBoundaryLast (localGridX p s k) (localGridY p s k) k k :: gridBoundaryDetour (localGridX p s k) (localGridY p s k) k k) = segment ℝ (Plane.mk (p.ofLp 0 - s) (p.ofLp 1 - s)) (Plane.mk (p.ofLp 0 + s) (p.ofLp 1 - s)) ∪ segment ℝ (Plane.mk (p.ofLp 0 + s) (p.ofLp 1 - s)) (Plane.mk (p.ofLp 0 + s) (p.ofLp 1 + s)) ∪ (segment ℝ (Plane.mk (p.ofLp 0 - s) (p.ofLp 1 + s)) (Plane.mk (p.ofLp 0 + s) (p.ofLp 1 + s)) ∪ segment ℝ (Plane.mk (p.ofLp 0 - s) (p.ofLp 1 - s)) (Plane.mk (p.ofLp 0 - s) (p.ofLp 1 + s)))

The outer boundary of the local grid is a cycle, and it occupies the frame of W.

Fineness

The one quantitative clause: every closed grid rectangle is smaller than ε. Stated twice — for the closed rectangle itself, which is the blueprint's wording, and for any connected subset of W that avoids the grid, which is the form a face of the overlay arrives in.

def Schoenflies.localGridCell (p : Plane) (s : ℝ) (k i j : ℕ) : Set Plane

The closed grid rectangle with lower-left index (i, j).

Equations

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

theorem Schoenflies.dist_le_of_supNorm_bounds {x y : Plane} {c : ℝ} (h0 : |x.ofLp 0 - y.ofLp 0| ≤ c) (h1 : |x.ofLp 1 - y.ofLp 1| ≤ c) : dist x y ≤ √2 * c

theorem Schoenflies.dist_lt_of_supNorm_bounds {x y : Plane} {c : ℝ} (h0 : |x.ofLp 0 - y.ofLp 0| < c) (h1 : |x.ofLp 1 - y.ofLp 1| < c) : dist x y < √2 * c

theorem Schoenflies.dist_le_of_mem_localGridCell {p : Plane} {s : ℝ} {k i j : ℕ} {x y : Plane} (hx : x ∈ localGridCell p s k i j) (hy : y ∈ localGridCell p s k i j) : dist x y ≤ √2 * (2 * s / ↑k)

prop:local-grid-attachment clause 3. Every closed grid rectangle has diameter at most √2 · (2s/k).

theorem Schoenflies.mem_cover_of_coord_eq {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) {z : Plane} {i : ℕ} (hi : i ≤ k) (hz : z ∈ p.closedSquare s) (hz0 : z.ofLp 0 = localGridX p s k i) : z ∈ cover (localGridEdges p s k)

The grid line at index i is part of the grid: a point of W whose first coordinate is a grid coordinate lies on the grid.

theorem Schoenflies.mem_cover_of_coord_eq' {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) {z : Plane} {j : ℕ} (hj : j ≤ k) (hz : z ∈ p.closedSquare s) (hz1 : z.ofLp 1 = localGridY p s k j) : z ∈ cover (localGridEdges p s k)

The same for the second coordinate.

theorem Schoenflies.dist_lt_of_avoiding_localGrid {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) {F : Set Plane} (hF : IsPreconnected F) (hFW : F ⊆ p.closedSquare s) (havoid : ∀ z ∈ F, z ∉ cover (localGridEdges p s k)) {x y : Plane} (hx : x ∈ F) (hy : y ∈ F) : dist x y < √2 * (2 * s / ↑k)

prop:local-grid-attachment clause 3, in the form the overlay consumes. A connected subset of the window W that avoids the grid has diameter less than √2 · (2s/k): it is trapped inside one open grid rectangle, coordinate by coordinate.

Choosing the mesh

prop:local-grid-attachment clause 3 asks for rectangles of diameter < ε.

noncomputable def Schoenflies.localGridCount (s ε : ℝ) : ℕ

The number of intervals per side of W that makes every grid rectangle smaller than ε.

Equations

• Schoenflies.localGridCount s ε = max 1 (⌈2 * √2 * s / ε⌉₊ + 1)

theorem Schoenflies.one_le_localGridCount (s ε : ℝ) : 1 ≤ localGridCount s ε

theorem Schoenflies.localGridCount_spec {s ε : ℝ} (hε : 0 < ε) : √2 * (2 * s / ↑(localGridCount s ε)) < ε

theorem Schoenflies.localGrid_fine {p : Plane} {s ε : ℝ} (hs : 0 < s) (hε : 0 < ε) : (localGrid p s (localGridCount s ε)).IsTwoConnected ∧ (localGrid p s (localGridCount s ε)).IsDrawing segmentDrawing ∧ ∀ (i j : ℕ), ∀ x ∈ localGridCell p s (localGridCount s ε) i j, ∀ y ∈ localGridCell p s (localGridCount s ε) i j, dist x y < ε

prop:local-grid-attachment clauses 2 and 3, packaged. On the window W of centre p and radius s there is a rectangular grid — 2-connected, still 2-connected after any subdivision, a plane graph — every closed rectangle of which has diameter < ε.