The sector decomposition at every point, and polygonal-side accessibility

Two things are done here. First, the last clause of Lemma "Local structure of a polygonal skeleton" (lem:local-skeleton-structure) is closed: Schoenflies/SkeletonSectors.lean proves it only at a point with at least two local branches, and the blueprint states it for every point. Second, its consumer, Lemma "Polygonal-side accessibility" (lem:polygonal-side-accessibility), is proved.

1. The two degenerate points

Schoenflies.IsLocalRadius.ball_diff_eq_iUnion_cone writes the punctured local disk as the union of the sectors Plane.cone x (Plane.arcCCW d w) r between consecutive local directions d, w. With fewer than two local directions there is no consecutive pair, and the two missing configurations are genuinely different sets:

• one local direction d — the disk slit along the radius in direction d, a sector of full turn (Schoenflies.IsLocalRadius.ball_diff_eq_slit);
• no local direction — the punctured disk, x being an isolated point of the skeleton (Schoenflies.IsLocalRadius.ball_diff_eq_punctured).

Both are connected (Schoenflies.isConnected_ball_diff_radial, Schoenflies.isConnected_ball_diff_singleton), which is everything the decomposition claims about a sector, so the blueprint's clause holds at every point with a single sector. Both proofs cut the set into convex pieces cut out by the sign of Plane.det and glue them along explicit overlaps: no angle, no arctangent, no cyclic order.

The sectors are then named, for every point at once, as what Schoenflies.IsLocalRadius.connectedComponentIn_eq_cone already proves them to be — the connected components of the punctured disk:

Schoenflies.localSectors S x r : Set (Set Plane)

with Schoenflies.localSectors_finite, Schoenflies.sUnion_localSectors, Schoenflies.localSectors_pairwiseDisjoint, Schoenflies.isOpen_of_mem_localSectors and Schoenflies.isConnected_of_mem_localSectors. In the generic case the members are exactly the cones (Schoenflies.cone_mem_localSectors); in the degenerate cases there is exactly one member (Schoenflies.localSectors_eq_of_subsingleton). A set of sets rather than an indexed family, because the natural index — a consecutive pair of local directions — does not exist at the two degenerate points.

2. Polygonal-side accessibility

Graph.exists_access_segment is the theorem, and it exports the construction: a point y of the 2-cell F, as close to x as prescribed, whose straight segment from x lies in F apart from x itself. Graph.polygonal_side_accessibility packages it as Schoenflies.PolyAccessible F x. The length bound is not in the blueprint statement; the shrinking-star arguments downstream need it, and it is free.

The blueprint's proof is followed step by step. Shrink the disk at x below the distance to the compact wild curve C (lem:compact-separation(c)), so that inside it the whole skeleton K = |G| ∪ C is just |G|; the punctured disk is then the union of the sectors; the sector containing y is connected and misses K, so it lies in a single 2-cell, and that cell is F because the sector meets F at y (Graph.localSector_subset_cell — this is the clause the audit found missing from Graph.exists_access_sector); the straight segment from x to y lies in that sector (Schoenflies.IsLocalRadius.openSegment_subset_connectedComponentIn).

The case x ∉ |G| — not excluded by the statement, since x need only lie on the boundary of F — is the degenerate configuration of part 1: the disk misses the skeleton entirely, is itself the only sector, and x turns out to lie in F.

The sector is taken throughout as the connected component of y in the punctured disk, so the number of local branches at x never enters the accessibility proof. Part 1 is what makes that component a sector in the blueprint's sense — at a point with one branch or none there is no consecutive pair of local directions to name it by, and the component is the whole punctured disk.

The one hypothesis

Schoenflies.CellsAbsorb K cells is lem:cellulation-invariants(i), a connected set disjoint from the skeleton lies in a single open 2-cell, in the "meets, hence contained" reading. It is the only thing assumed; two dischargers are supplied (Schoenflies.cellsAbsorb_of_isComponent, Schoenflies.cellsAbsorb_of_isComponent_in), the second of which covers the target side, where the 2-cells only fill an ambient region Q whose frontier belongs to the skeleton.

The target side

Graph.polygonal_side_accessibility_target and Graph.polygonal_side_accessibility_square. The blueprint keeps a sector from leaking out of the square by applying thm:polygonal-jordan to the square boundary; that is not needed here. The corresponding step is Schoenflies.subset_of_isPreconnected_of_frontier_disjoint — a connected set missing the frontier of an open set and meeting it lies inside it — together with Schoenflies.frontier_openSquare_subset. Both are elementary, so the target side rests on nothing beyond the shared hypothesis.

Blueprint

• Schoenflies.isConnected_ball_diff_radial, Schoenflies.isConnected_ball_diff_singleton, Schoenflies.IsLocalRadius.ball_diff_eq_slit, Schoenflies.IsLocalRadius.ball_diff_eq_punctured, Schoenflies.IsLocalRadius.isConnected_ball_diff_of_subsingleton — "consequently B(x,r) \ |G| is a finite union of open circular sectors" of lem:local-skeleton-structure, at the two points where Schoenflies/SkeletonSectors.lean leaves it open.
• Schoenflies.localSectors and its API, Graph.IsDrawing.localSectors_finite, Graph.IsDrawing.isOpen_of_mem_localSectors — the same clause for a finite plane graph with polygonal edges.
• Schoenflies.localDirs_union_of_disjoint, Schoenflies.IsLocalRadius.union_of_disjoint, Graph.IsDrawing.exists_isLocalRadius_union — "shrink the disk at x until it also misses the compact set C; the disk then meets the whole skeleton in the finitely many radial segments" of lem:polygonal-side-accessibility.
• Schoenflies.CellsAbsorb, Schoenflies.cellsAbsorb_of_isComponent, Schoenflies.cellsAbsorb_of_isComponent_in — lem:cellulation-invariants(i), assumed, and the two ways a cellulation discharges it.
• Graph.localSector_subset_face, Graph.localSector_subset_cell, Schoenflies.IsLocalRadius.openSegment_subset_connectedComponentIn — "each sector is connected and disjoint from the skeleton, so … lies in a single open 2-cell; and at least one sector lies in F … a short straight segment from x into that sector is a polygonal access arc" of lem:polygonal-side-accessibility.
• Graph.exists_access_segment, Graph.polygonal_side_accessibility — lem:polygonal-side-accessibility, source side.
• Graph.polygonal_side_accessibility_target, Graph.polygonal_side_accessibility_square, Schoenflies.subset_of_isPreconnected_of_frontier_disjoint, Schoenflies.frontier_openSquare_subset — "the analogous assertion holds at every boundary point of a target face" of the same lemma.

Bilinearity conveniences

Two ways to miss a radius

A point of the disk fails to lie on the radius at x in direction d for one of two reasons: it is off the line of d altogether, or it is on that line but on the far side. Both are sign conditions on Plane.det, and both are used three times below.

theorem Schoenflies.notMem_radial_of_det_ne_zero {x z d : Plane} {r : ℝ} (hd : d.IsDirection) (hr : 0 < r) (h : d.det (z - x) ≠ 0) : z ∉ segment ℝ x (x + r • d)

A point off the line of d through x is not on the radius at x in direction d.

theorem Schoenflies.notMem_radial_of_det_perp_pos {x z d : Plane} {r : ℝ} (hd : d.IsDirection) (hr : 0 < r) (h : 0 < d.perp.det (z - x)) : z ∉ segment ℝ x (x + r • d)

A point on the far side of x along the line of d is not on the radius at x in direction d. The hypothesis 0 < det (perp d) (z - x) is ⟪d, z - x⟫ < 0 written without an inner product (Plane.det_perp_left).

The disk minus one radius, and the punctured disk

Schoenflies/SkeletonSectors.lean decomposes the punctured local disk into the open sectors between consecutive local directions, and that decomposition says nothing when there are fewer than two directions to be consecutive. The two missing configurations are settled here: with one local direction the punctured disk is the disk slit along a single radius, and with none it is the punctured disk itself. Both are connected, which is everything the decomposition claims about a sector, so the blueprint's clause holds at every point with the number of sectors equal to one.

theorem Schoenflies.isConnected_cone_of_convex {x : Plane} {r : ℝ} {A : Set Plane} (hA : Convex ℝ A) (hne : (x.cone A r).Nonempty) : IsConnected (x.cone A r)

A cone over a convex set of directions is connected as soon as it is nonempty: it is the translate of an intersection of two convex sets.

theorem Schoenflies.isConnected_ball_diff_radial {x d : Plane} {r : ℝ} (hd : d.IsDirection) (hr : 0 < r) : IsConnected (Metric.ball x r \ segment ℝ x (x + r • d))

The disk slit along one radius is connected. When d is the only local direction at x, this single set is the "sector of full turn" that lem:local-skeleton-structure claims; it is not of the form arcCCW d w for two local directions, which is why Schoenflies.IsLocalRadius.ball_diff_eq_iUnion_cone has to assume two branches.

The proof cuts the slit disk into three convex half-disks — the two open sides of the line of d, and the open half-disk pointing away from d — and glues them along their two overlaps. No angle and no cyclic order enters.

theorem Schoenflies.isDirection_mk_one_zero : (Plane.mk 1 0).IsDirection

The horizontal unit vector, used only to have some direction to slit along.

theorem Schoenflies.isConnected_ball_diff_singleton {x : Plane} {r : ℝ} (hr : 0 < r) : IsConnected (Metric.ball x r \ {x})

The punctured disk is connected. Two disks slit along opposite radii cover it and overlap off the line of the slit. This is the "sector" at a point of the skeleton with no local direction — an isolated vertex.

The degenerate local disks

With Schoenflies.isConnected_ball_diff_radial and Schoenflies.isConnected_ball_diff_singleton in hand, the two configurations that Schoenflies/SkeletonSectors.lean had to exclude are read off the membership criterion.

theorem Schoenflies.IsLocalRadius.center_mem {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) : x ∈ S

A local radius is a radius at a point of the set: take z = x in the criterion.

theorem Schoenflies.IsLocalRadius.ball_diff_eq_punctured {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hzero : localDirs S x = ∅) : Metric.ball x r \ S = Metric.ball x r \ {x}

No local branch: inside the disk the set is the single point x.

theorem Schoenflies.IsLocalRadius.ball_diff_eq_slit {S : Set Plane} {x d : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hone : localDirs S x = {d}) : Metric.ball x r \ S = Metric.ball x r \ segment ℝ x (x + r • d)

One local branch: inside the disk the set is the single radius in that direction.

theorem Schoenflies.IsLocalRadius.isConnected_ball_diff_of_subsingleton {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hsub : (localDirs S x).Subsingleton) : IsConnected (Metric.ball x r \ S)

The punctured local disk is connected when x has fewer than two branches. This closes the two configurations Schoenflies.IsLocalRadius.ball_diff_eq_iUnion_cone excludes: there is one sector, and it is the whole punctured disk.

theorem Schoenflies.IsLocalRadius.isOpen_ball_diff {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hfin : (localDirs S x).Finite) : IsOpen (Metric.ball x r \ S)

The punctured local disk is open. IsLocalRadius does not say that S is closed, and does not have to: inside the disk, S is a point together with finitely many closed segments.

Adding a set the disk misses

The blueprint's "shrink the disk at x until it also misses the compact set C; the disk then meets the whole skeleton in the finitely many radial segments". Once the disk is clear of C, neither the membership criterion nor the set of local directions can tell S from S ∪ C.

theorem Schoenflies.localDirs_union_of_disjoint {S : Set Plane} {x : Plane} {r : ℝ} {C : Set Plane} (hr : 0 < r) (hC : Disjoint (Metric.closedBall x r) C) : localDirs (S ∪ C) x = localDirs S x

A set the closed disk misses contributes no local direction.

theorem Schoenflies.IsLocalRadius.union_of_disjoint {S : Set Plane} {x : Plane} {r : ℝ} {C : Set Plane} (h : IsLocalRadius S x r) (hC : Disjoint (Metric.closedBall x r) C) : IsLocalRadius (S ∪ C) x r

A local radius survives adjoining a set the closed disk misses. This is the step that turns a local radius for the polygonal part of a skeleton into one for the whole skeleton.

The sectors of a local disk, at every point

The blueprint's "B(x,r) \ |G| is a finite union of open circular sectors" is delivered here without the two-branch hypothesis, by naming the sectors as what they are proved to be in Schoenflies.IsLocalRadius.connectedComponentIn_eq_cone: the connected components of the punctured disk. With at least two branches each component is one of the cones (Schoenflies.cone_mem_localSectors); with fewer there is exactly one component, the whole punctured disk (Schoenflies.localSectors_eq_of_subsingleton).

def Schoenflies.localSectors (S : Set Plane) (x : Plane) (r : ℝ) : Set (Set Plane)

The sectors of the punctured local disk at x: its connected components.

Defined as a set of sets rather than as an indexed family, because the two degenerate configurations have no natural index — the index in the generic case is a consecutive pair of local directions, and there is no such pair when there are fewer than two of them.

Equations

• Schoenflies.localSectors S x r = (fun (z : Schoenflies.Plane) => connectedComponentIn (Metric.ball x r \ S) z) '' (Metric.ball x r \ S)

theorem Schoenflies.mem_localSectors {S : Set Plane} {x z : Plane} {r : ℝ} (hz : z ∈ Metric.ball x r \ S) : connectedComponentIn (Metric.ball x r \ S) z ∈ localSectors S x r

theorem Schoenflies.subset_ball_diff_of_mem_localSectors {S N : Set Plane} {x : Plane} {r : ℝ} (hN : N ∈ localSectors S x r) : N ⊆ Metric.ball x r \ S

theorem Schoenflies.isConnected_of_mem_localSectors {S N : Set Plane} {x : Plane} {r : ℝ} (hN : N ∈ localSectors S x r) : IsConnected N

Each sector is connected — in particular nonempty.

theorem Schoenflies.isOpen_of_mem_localSectors {S N : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hfin : (localDirs S x).Finite) (hN : N ∈ localSectors S x r) : IsOpen N

Each sector is open.

theorem Schoenflies.sUnion_localSectors {S : Set Plane} {x : Plane} {r : ℝ} : ⋃₀ localSectors S x r = Metric.ball x r \ S

The sectors cover the punctured disk. No hypothesis: this is true of components.

theorem Schoenflies.localSectors_pairwiseDisjoint {S : Set Plane} {x : Plane} {r : ℝ} : (localSectors S x r).PairwiseDisjoint id

The sectors are pairwise disjoint, so the cover is a partition.

theorem Schoenflies.localSectors_finite {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hfin : (localDirs S x).Finite) : (localSectors S x r).Finite

There are finitely many sectors. With at least two branches each is a cone between a consecutive pair of local directions, and there are finitely many such pairs; with fewer there is exactly one sector.

theorem Schoenflies.cone_mem_localSectors {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hfin : (localDirs S x).Finite) (h2 : ∃ a ∈ localDirs S x, ∃ b ∈ localDirs S x, a ≠ b) {e w : Plane} (hp : Plane.IsSectorPair (localDirs S x) e w) : x.cone (e.arcCCW w) r ∈ localSectors S x r

With at least two branches, every cone between consecutive local directions is a sector.

theorem Schoenflies.localSectors_eq_of_subsingleton {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hfin : (localDirs S x).Finite) (hsub : (localDirs S x).Subsingleton) : localSectors S x r = {Metric.ball x r \ S}

With fewer than two branches there is exactly one sector: the whole punctured disk.

theorem Schoenflies.IsLocalRadius.openSegment_subset_connectedComponentIn {S : Set Plane} {x y : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hy : y ∈ Metric.ball x r) (hyS : y ∉ S) : openSegment ℝ x y ⊆ connectedComponentIn (Metric.ball x r \ S) y

The access sector, with no hypothesis on the number of branches. The straight segment from x to a point y of the punctured disk lies in y's own sector, so the sector is reached from x without leaving it.

The sector is named — it is connectedComponentIn (ball x r \ S) y, a member of Schoenflies.localSectors by Schoenflies.mem_localSectors — rather than packaged in an ∃, so a consumer can speak about it before producing it.

lem:cellulation-invariants(i), as a hypothesis

The only thing assumed in this module. It is not a restatement of the goal: it speaks about the cells of a cellulation, an object that has no Lean definition yet, and it is exactly the invariant that another module is proving by induction over the two elementary operations.

def Schoenflies.CellsAbsorb (K : Set Plane) (cells : Set (Set Plane)) : Prop

lem:cellulation-invariants(i) for a family cells of open 2-cells whose skeleton is K: a connected set disjoint from the skeleton lies in a single open 2-cell.

Stated in the "meets, hence contained" reading, which is the form the proof of lem:polygonal-side-accessibility uses and which packages the word single — with the usual ∃-reading one still has to know that distinct 2-cells are disjoint before concluding that the cell found is the prescribed one. It is discharged by Schoenflies.cellsAbsorb_of_isComponent (each 2-cell is a connected component of the complement of the skeleton, which is what invariant (i) asserts) or, when the cells live inside an ambient region whose frontier belongs to the skeleton, by Schoenflies.cellsAbsorb_of_isComponent_in.

Equations

• Schoenflies.CellsAbsorb K cells = ∀ (N : Set Schoenflies.Plane), IsPreconnected N → Disjoint N K → ∀ R ∈ cells, (N ∩ R).Nonempty → N ⊆ R

theorem Schoenflies.subset_of_isPreconnected_of_frontier_disjoint {Q N : Set Plane} (hQ : IsOpen Q) (hN : IsPreconnected N) (hfr : Disjoint N (frontier Q)) (hmeet : (N ∩ Q).Nonempty) : N ⊆ Q

A connected set that misses the frontier of an open set and meets it lies inside it.

theorem Schoenflies.cellsAbsorb_of_isComponent {K : Set Plane} {cells : Set (Set Plane)} (h : ∀ R ∈ cells, ∃ (z : Plane), R = connectedComponentIn Kᶜ z) : CellsAbsorb K cells

The discharger for Schoenflies.CellsAbsorb: the 2-cells are the connected components of the complement of the skeleton. That is the content of lem:cellulation-invariants(i).

theorem Schoenflies.cellsAbsorb_of_isComponent_in {Q K : Set Plane} (hQ : IsOpen Q) (hQK : frontier Q ⊆ K) {cells : Set (Set Plane)} (h : ∀ R ∈ cells, R ⊆ Q ∧ ∃ (z : Plane), R = connectedComponentIn (Q \ K) z) : CellsAbsorb K cells

The discharger on the target side: the 2-cells are the connected components of what is left of an ambient open region Q after the skeleton is removed, and the frontier of Q belongs to the skeleton. The second clause is what stops a sector from leaking out of Q; in the blueprint it is thm:polygonal-jordan applied to the square boundary, and here it is Schoenflies.subset_of_isPreconnected_of_frontier_disjoint.

theorem Schoenflies.frontier_openSquare_subset (c : Plane) (s : ℝ) : frontier (c.openSquare s) ⊆ c.closedSquare s \ c.openSquare s

The frontier of an open axis-parallel square lies in the square's boundary. This is how the hypothesis "the boundary of Q is part of the skeleton" is checked on the target side.

lem:polygonal-side-accessibility

The sector decomposition for a finite polygonal plane graph

lem:local-skeleton-structure's last clause, "consequently B(x,r) \ |G| is a finite union of open circular sectors", now holds at every point of |G|: at a point with at least two local branches the sectors are the cones of Schoenflies.IsLocalRadius.ball_diff_eq_iUnion_cone, and at the two degenerate points there is a single one.

theorem Graph.IsDrawing.exists_isLocalRadius_union {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {C : Set Schoenflies.Plane} {x : Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) (hC : IsCompact C) (hx : x ∈ G.pointSet drawing) (hxC : x ∉ C) : ∃ (r : ℝ), Schoenflies.IsLocalRadius (G.pointSet drawing ∪ C) x r

The disk meets the whole skeleton in the finitely many radial segments. The blueprint's first step in lem:polygonal-side-accessibility: at a point of the polygonal graph off the compact wild set C, a small enough disk is a local disk for |G| ∪ C, not merely for |G|.

Not used below — the accessibility proof works with |G| inside the disk and disposes of C by disjointness — but it is the blueprint sentence, and a consumer wanting the sectors of the whole skeleton wants this.

theorem Graph.IsDrawing.localSectors_finite {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} {r : ℝ} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) (hr : Schoenflies.IsLocalRadius (G.pointSet drawing) x r) : (Schoenflies.localSectors (G.pointSet drawing) x r).Finite

There are finitely many sectors at every point of |G|.

theorem Graph.IsDrawing.isOpen_of_mem_localSectors {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} {r : ℝ} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) (hr : Schoenflies.IsLocalRadius (G.pointSet drawing) x r) {N : Set Schoenflies.Plane} (hN : N ∈ Schoenflies.localSectors (G.pointSet drawing) x r) : IsOpen N

Every sector at a point of |G| is open.

theorem Graph.localSector_subset_face {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x y : Schoenflies.Plane} {r : ℝ} (hy : y ∈ Metric.ball x r) (hyE : y ∈ G.exterior drawing) : connectedComponentIn (Metric.ball x r \ G.pointSet drawing) y ⊆ G.face drawing y

Each sector lies in a single face, namely the face of any of its points. This is the clause Graph.exists_access_sector proves under the two-branch hypothesis, here with none — and in fact with no hypothesis on the radius either, since a component of the punctured disk is a connected subset of the exterior whatever the radius.

theorem Graph.localSector_subset_cell {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {C F K : Set Schoenflies.Plane} {cells : Set (Set Schoenflies.Plane)} {x y : Schoenflies.Plane} {r : ℝ} (hK : K = G.pointSet drawing ∪ C) (hcells : Schoenflies.CellsAbsorb K cells) (hF : F ∈ cells) (hballC : Disjoint (Metric.ball x r) C) (hy : y ∈ Metric.ball x r) (hyF : y ∈ F) (hyS : y ∉ G.pointSet drawing) : connectedComponentIn (Metric.ball x r \ G.pointSet drawing) y ⊆ F

At least one sector lies in F. The clause of lem:polygonal-side-accessibility that Graph.exists_access_sector was credited with and does not prove: the sector containing a point y of the 2-cell F lies wholly inside F.

The reasoning is the blueprint's, once the disk has been shrunk below the distance to the wild set C: the sector is connected and misses the whole skeleton K = |G| ∪ C, so by lem:cellulation-invariants(i) it lies in a single 2-cell, and that cell is F because the sector meets F at y.

theorem Graph.exists_access_segment {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {C F K : Set Schoenflies.Plane} {cells : Set (Set Schoenflies.Plane)} {x : Schoenflies.Plane} {ε : ℝ} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) (hC : IsCompact C) (hK : K = G.pointSet drawing ∪ C) (hcells : Schoenflies.CellsAbsorb K cells) (hF : F ∈ cells) (hFK : Disjoint F K) (hx : x ∈ closure F) (hxC : x ∉ C) (hε : 0 < ε) : ∃ y ∈ F, y ≠ x ∧ dist y x < ε ∧ openSegment ℝ x y ⊆ F

The access segment of lem:polygonal-side-accessibility, with a prescribed length bound. Let G be a finite plane graph with polygonal edges, C a compact set — the wild outer curve — and K = |G| ∪ C the whole skeleton. Let F be an open 2-cell, and x a point at which F accumulates, lying off C. Then arbitrarily near x there is a point y of F whose straight segment from x lies, apart from x itself, inside F.

The straight segment is exported rather than the accessibility predicate, because the later shrinking-star arguments need the access arc to be short; PolyAccessible follows in Graph.polygonal_side_accessibility.

The proof is the blueprint's. Shrink the disk at x below the distance to C, so that inside it the whole skeleton is |G|; then the punctured disk is the union of the sectors of Schoenflies.localSectors, each of them connected and disjoint from the skeleton, and the one containing y lies in a single 2-cell by the assumed lem:cellulation-invariants(i). That cell is F, because the sector meets F at y. When x is not on |G| at all — which the statement does not exclude, since x need only be a limit of points of F — the disk misses the skeleton entirely and is itself the access region.

The sector is named as the connected component of y in the punctured disk, so no hypothesis on the number of local branches at x is needed anywhere.

theorem Graph.polygonal_side_accessibility {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {C F K : Set Schoenflies.Plane} {cells : Set (Set Schoenflies.Plane)} {x : Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) (hC : IsCompact C) (hK : K = G.pointSet drawing ∪ C) (hcells : Schoenflies.CellsAbsorb K cells) (hF : F ∈ cells) (hFK : Disjoint F K) (hx : x ∈ closure F) (hxC : x ∉ C) : Schoenflies.PolyAccessible F x

lem:polygonal-side-accessibility, source side. A boundary point of a 2-cell F of a finite cellulation, lying off the wild outer curve C, is polygonally accessible from F.

x ∈ closure F is assumed rather than x ∈ frontier F: the proof never uses x ∉ F, and the weaker hypothesis is what a consumer holding a limit of points of F actually has.

theorem Graph.polygonal_side_accessibility_target {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {F Q : Set Schoenflies.Plane} {cells : Set (Set Schoenflies.Plane)} {x : Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) (hQ : IsOpen Q) (hQK : frontier Q ⊆ G.pointSet drawing) (hcell : ∀ R ∈ cells, R ⊆ Q ∧ ∃ (z : Schoenflies.Plane), R = connectedComponentIn (Q \ G.pointSet drawing) z) (hF : F ∈ cells) (hx : x ∈ closure F) : Schoenflies.PolyAccessible F x

lem:polygonal-side-accessibility, target side. On the target every edge is polygonal, including every outer edge, so there is no wild set to avoid; but the 2-cells only fill an ambient region Q whose frontier belongs to the skeleton, and a sector at a boundary point of Q may lie outside Q and belong to no cell. That is exactly what Schoenflies.cellsAbsorb_of_isComponent_in handles.

theorem Graph.polygonal_side_accessibility_square {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {F : Set Schoenflies.Plane} {cells : Set (Set Schoenflies.Plane)} {x : Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) (c : Schoenflies.Plane) (s : ℝ) (hS : c.closedSquare s \ c.openSquare s ⊆ G.pointSet drawing) (hcell : ∀ R ∈ cells, R ⊆ c.openSquare s ∧ ∃ (z : Schoenflies.Plane), R = connectedComponentIn (c.openSquare s \ G.pointSet drawing) z) (hF : F ∈ cells) (hx : x ∈ closure F) : Schoenflies.PolyAccessible F x

Graph.polygonal_side_accessibility_target with the ambient region the open square. The blueprint gets "a sector meeting F lies in Q°" from thm:polygonal-jordan applied to the square boundary; here it comes from Schoenflies.frontier_openSquare_subset and the clopen argument in Schoenflies.subset_of_isPreconnected_of_frontier_disjoint, so the polygonal Jordan theorem is not needed.