Local structure of a polygonal skeleton

Close enough to any of its points, a finite union of segments and points looks like a star: the point itself together with finitely many radial segments leaving it, one per local branch. This module proves that, and hands the accessibility argument the form it needs.

What is exported, and why in this shape

The data is Schoenflies.localDirs S x, the set of unit vectors d such that some initial segment [x, x + ε • d] lies in S. It is defined for an arbitrary set, with no choices in it: nothing about a segment decomposition of S enters the definition, so no consumer has to carry one. "Pairwise distinct directions" is then not a clause to be proved but the meaning of the word set, and the blueprint's real content becomes localDirs_finite.

The radius is the one genuinely existential ingredient — there is no canonical r₀ — so it is named by a predicate rather than returned inside an ∃-packaged bundle of properties:

Schoenflies.IsLocalRadius S x r : 0 < r, and every point within r of x lies in S exactly when it is x itself or leaves x in a local direction.

That single membership criterion is equivalent to the blueprint's picture and implies all of its parts, each proved here as a lemma about IsLocalRadius and hence available at every radius below the one produced: the closed-disk formula (IsLocalRadius.closedBall_inter), the open disk minus S as a cone over the complement of the local rays (IsLocalRadius.ball_diff_eq_cone), and the star-shapedness that the accessibility lemma actually cites (IsLocalRadius.openSegment_subset_ball_diff).

What the consumer (lem:polygonal-side-accessibility) needs

That lemma takes y in a face F inside the disk, and wants a polygonal arc from x into F. IsLocalRadius.openSegment_subset_ball_diff gives (x, y) ⊆ B(x, r) \ S directly, and openSegment ℝ x y ∪ {y} is connected and disjoint from the skeleton — which is everything the blueprint's "pick the sector containing y, then a short segment from x into it" is used for. The decomposition of the punctured disk into its individual sectors, one per pair of cyclically adjacent local directions, is therefore not proved here: it needs a cyclic order on directions, and no consumer needs it. IsLocalRadius.ball_diff_eq_cone records the sectors in aggregate — as one Plane.cone over all free directions at once.

Blueprint

• Schoenflies.localDirs, Schoenflies.localDirs_finite — the finitely many local branch directions at x of Lemma "Local structure of a polygonal skeleton" (lem:local-skeleton-structure).
• Schoenflies.IsLocalRadius, Schoenflies.exists_isLocalRadius, Schoenflies.IsLocalRadius.closedBall_inter — the radius r₀, and "for every 0 < r ≤ r₀ the closed disk meets |G| exactly in finitely many straight segments from x with pairwise distinct directions" (same lemma).
• Schoenflies.IsLocalRadius.ball_diff_eq_cone — "consequently B(x,r) \ |G| is a finite union of open circular sectors" (same lemma), in aggregate form.
• Schoenflies.IsLocalRadius.openSegment_subset_ball_diff — the form lem:polygonal-side-accessibility cites: a short straight segment from x towards any point of the punctured disk misses the skeleton.
• Graph.IsDrawing.exists_cover, Graph.IsDrawing.exists_isLocalRadius, Graph.IsDrawing.finite_localDirs — the same statements for a finite plane graph all of whose edges are polygonal.
• Graph.IsDrawing.openSegment_subset_face — the access arc of lem:polygonal-side-accessibility, assembled: a straight segment from x to a point of the exterior inside a local disk lies, minus x, in that point's face.

Radial segments

segment ℝ x (x + r • d) with d a unit vector is the closed radius of length r leaving x in the direction d. Two facts run the whole module: a point lies on it exactly when it is near enough and points the right way (mem_radial_iff), and cutting a longer radius by a smaller ball leaves the shorter radius (radial_inter_closedBall).

theorem Schoenflies.dir_smul_of_isDirection {d : Plane} {t : ℝ} (hd : d.IsDirection) (ht : 0 < t) : (t • d).dir = d

The unit vector along a positive multiple of a unit vector is that vector.

theorem Schoenflies.smul_norm_dir {d : Plane} (h : d ≠ 0) : ‖d‖ • d.dir = d

A nonzero vector is its own length times its own direction.

theorem Schoenflies.dir_smul_pos {t : ℝ} (ht : 0 < t) (u : Plane) : (t • u).dir = u.dir

Positive scaling does not move a direction.

theorem Schoenflies.mem_radial_iff {x z d : Plane} {r : ℝ} (hd : d.IsDirection) (hr : 0 < r) : z ∈ segment ℝ x (x + r • d) ↔ dist z x ≤ r ∧ (z = x ∨ (z - x).dir = d)

Membership in a radius: near enough, and pointing the right way.

theorem Schoenflies.radial_subset_closedBall {x d : Plane} {r : ℝ} (hd : d.IsDirection) (hr : 0 < r) : segment ℝ x (x + r • d) ⊆ Metric.closedBall x r

A radius of length r lies in the closed disk of radius r.

theorem Schoenflies.radial_inter_closedBall {x d : Plane} {r R : ℝ} (hd : d.IsDirection) (hr : 0 < r) (hrR : r ≤ R) : segment ℝ x (x + R • d) ∩ Metric.closedBall x r = segment ℝ x (x + r • d)

Cutting a radius by a smaller concentric disk leaves the shorter radius.

theorem Schoenflies.segment_eq_radial {x c : Plane} (h : c ≠ x) : segment ℝ x c = segment ℝ x (x + dist x c • (c - x).dir)

A segment out of x is the radius of its own length in its own direction.

theorem Schoenflies.segment_inter_closedBall {x c : Plane} {r : ℝ} (hcx : c ≠ x) (hr : 0 < r) (hrc : r ≤ dist x c) : segment ℝ x c ∩ Metric.closedBall x r = segment ℝ x (x + r • (c - x).dir)

Inside a disk too small to reach c, the segment [x, c] is exactly a radius. This is the one geometric step behind the whole module: it turns each straight piece through x into one or two radial segments.

The local directions of a set

def Schoenflies.localDirs (S : Set Plane) (x : Plane) : Set Plane

The local directions of S at x: the unit vectors along which S contains an initial segment issuing from x.

Choice-free and stated for an arbitrary set, so that a consumer never has to name a segment decomposition of S. Being a set of unit vectors, its members are automatically pairwise distinct — the blueprint's "with pairwise distinct directions".

Equations

• Schoenflies.localDirs S x = {d : Schoenflies.Plane | d.IsDirection ∧ ∃ (ε : ℝ), 0 < ε ∧ segment ℝ x (x + ε • d) ⊆ S}

theorem Schoenflies.isDirection_of_mem_localDirs {S : Set Plane} {x d : Plane} (h : d ∈ localDirs S x) : d.IsDirection

theorem Schoenflies.mem_localDirs {S : Set Plane} {x d : Plane} {ε : ℝ} (hd : d.IsDirection) (hε : 0 < ε) (h : segment ℝ x (x + ε • d) ⊆ S) : d ∈ localDirs S x

theorem Schoenflies.localDirs_mono {S T : Set Plane} {x : Plane} (h : S ⊆ T) : localDirs S x ⊆ localDirs T x

theorem Schoenflies.mem_of_mem_localDirs {S : Set Plane} {x d : Plane} (h : d ∈ localDirs S x) : x ∈ S

A local direction witnesses that x itself belongs to S.

The pieces through a point

Everything is now bookkeeping over a finite list of segments and a finite set of stray points. GoodRadius x P r collects what a radius must avoid on account of one piece: pieces missing x must stay outside the disk, and pieces through x must not end inside it.

def Schoenflies.GoodRadius (x : Plane) (P : Piece) (r : ℝ) : Prop

The radius conditions imposed at x by one piece: a piece missing x stays clear of the closed disk, and an endpoint of a piece through x is never inside it.

Equations

• Schoenflies.GoodRadius x P r = ((x ∉ P.seg → ∀ z ∈ P.seg, r < dist x z) ∧ (P.1 ≠ x → r ≤ dist x P.1) ∧ (P.2 ≠ x → r ≤ dist x P.2))

theorem Schoenflies.GoodRadius.mono {x : Plane} {r ε : ℝ} {P : Piece} (h : GoodRadius x P r) (hle : ε ≤ r) : GoodRadius x P ε

theorem Schoenflies.exists_goodRadius (x : Plane) (P : Piece) : ∃ r > 0, GoodRadius x P r

def Schoenflies.pieceDirs (ps : List Piece) (x : Plane) : Set Plane

Auxiliary: the directions in which the pieces of ps leave x. Unlike localDirs this depends on the chosen segment decomposition; the two are proved equal at any good radius.

Equations

• Schoenflies.pieceDirs ps x = {d : Schoenflies.Plane | ∃ P ∈ ps, x ∈ P.seg ∧ (P.1 ≠ x ∧ d = (P.1 - x).dir ∨ P.2 ≠ x ∧ d = (P.2 - x).dir)}

theorem Schoenflies.isDirection_of_mem_pieceDirs {ps : List Piece} {x d : Plane} (h : d ∈ pieceDirs ps x) : d.IsDirection

theorem Schoenflies.pieceDirs_finite (ps : List Piece) (x : Plane) : (pieceDirs ps x).Finite

theorem Schoenflies.radial_subset_cover {ps : List Piece} {x d : Plane} {r : ℝ} (hgood : ∀ P ∈ ps, GoodRadius x P r) (hr : 0 < r) (hd : d ∈ pieceDirs ps x) : segment ℝ x (x + r • d) ⊆ cover ps

A radius in a piece direction, at a good radius, stays inside the pieces.

theorem Schoenflies.cover_inter_closedBall_subset {ps : List Piece} {x : Plane} {r : ℝ} (hgood : ∀ P ∈ ps, GoodRadius x P r) (hr : 0 < r) : cover ps ∩ Metric.closedBall x r ⊆ insert x (⋃ d ∈ pieceDirs ps x, segment ℝ x (x + r • d))

At a good radius, the pieces meet the closed disk only in x and the radii.

The membership criterion

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

r is a local radius for S at x: within distance r of x, the set S consists of x together with the rays leaving x in the local directions.

This one criterion is the whole local picture; the disk formula, the sector description and the star-shapedness are all derived from it below, and each therefore holds at every positive radius below a local radius (IsLocalRadius.mono).

Equations

• Schoenflies.IsLocalRadius S x r = (0 < r ∧ ∀ (z : Schoenflies.Plane), dist z x ≤ r → (z ∈ S ↔ z = x ∨ (z - x).dir ∈ Schoenflies.localDirs S x))

theorem Schoenflies.IsLocalRadius.pos {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) : 0 < r

theorem Schoenflies.IsLocalRadius.mono {S : Set Plane} {x : Plane} {r ε : ℝ} (h : IsLocalRadius S x r) (hε : 0 < ε) (hle : ε ≤ r) : IsLocalRadius S x ε

A local radius exists

The construction: choose a radius good for every piece and strictly below the distance to every stray point other than x.

theorem Schoenflies.exists_pos_goodRadius {F : Set Plane} (hF : F.Finite) (ps : List Piece) (x : Plane) : ∃ r > 0, (∀ P ∈ ps, GoodRadius x P r) ∧ ∀ p ∈ F, p ≠ x → r < dist x p

theorem Schoenflies.pieceDirs_subset_localDirs {S F : Set Plane} {ps : List Piece} {x : Plane} {r : ℝ} (hS : S = F ∪ cover ps) (hr : 0 < r) (hgood : ∀ P ∈ ps, GoodRadius x P r) : pieceDirs ps x ⊆ localDirs S x

Every piece direction is a local direction: at a good radius the whole radius fits in the pieces.

theorem Schoenflies.mem_iff_of_goodRadius {S F : Set Plane} {ps : List Piece} {x z : Plane} {r : ℝ} (hS : S = F ∪ cover ps) (hr : 0 < r) (hx : x ∈ S) (hgood : ∀ P ∈ ps, GoodRadius x P r) (hFgood : ∀ p ∈ F, p ≠ x → r < dist x p) (hz : dist z x ≤ r) : z ∈ S ↔ z = x ∨ (z - x).dir ∈ pieceDirs ps x

The membership criterion, phrased with the auxiliary pieceDirs.

theorem Schoenflies.localDirs_subset_pieceDirs {S F : Set Plane} {ps : List Piece} {x : Plane} {r : ℝ} (hS : S = F ∪ cover ps) (hr : 0 < r) (hgood : ∀ P ∈ ps, GoodRadius x P r) (hFgood : ∀ p ∈ F, p ≠ x → r < dist x p) : localDirs S x ⊆ pieceDirs ps x

Conversely, at a good radius every local direction comes from a piece. This is where the germ hypothesis in localDirs is cashed in: a short segment in S leaving x lands in a piece, and that piece must pass through x.

theorem Schoenflies.localDirs_finite {S F : Set Plane} {ps : List Piece} (hF : F.Finite) (hS : S = F ∪ cover ps) (x : Plane) : (localDirs S x).Finite

The local directions of a finite union of segments and points are finitely many. This is the blueprint's "finitely many straight segments from x with pairwise distinct directions": distinctness is automatic for a set, finiteness is the content.

theorem Schoenflies.exists_isLocalRadius {S F : Set Plane} {ps : List Piece} {x : Plane} (hF : F.Finite) (hS : S = F ∪ cover ps) (hx : x ∈ S) : ∃ (r : ℝ), IsLocalRadius S x r

A local radius exists. Lemma "Local structure of a polygonal skeleton", for a set presented as finitely many points together with finitely many segments.

What a local radius gives

theorem Schoenflies.IsLocalRadius.closedBall_inter {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hx : x ∈ S) : Metric.closedBall x r ∩ S = insert x (⋃ d ∈ localDirs S x, segment ℝ x (x + r • d))

The closed disk meets S exactly in the radial segments. The blueprint's "the closed disk B(x,r) meets |G| exactly in finitely many straight segments from x with pairwise distinct directions".

theorem Schoenflies.IsLocalRadius.ball_diff_eq_cone {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) : Metric.ball x r \ S = x.cone {u : Plane | u ≠ 0 ∧ u.dir ∉ localDirs S x} r

The punctured disk is a union of open sectors, in aggregate: B(x,r) \ S is the open cone over the directions that are not local directions.

The individual sectors — one per cyclically adjacent pair of local directions — are not separated out; see the module docstring.

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

The punctured disk is star-shaped about x. This is the form lem:polygonal-side-accessibility cites: a straight segment from x towards any point of the disk that misses S misses S all the way.

Together with connectedness of openSegment ℝ x y ∪ {y} it replaces the blueprint's "pick the sector containing y, then a short segment from x into it".

theorem Schoenflies.IsLocalRadius.exists_mem_ball_diff {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hfin : (localDirs S x).Finite) : ∃ y ∈ Metric.ball x r, y ∉ S

Some direction at x is free, so the punctured disk is nonempty.

Finite polygonal plane graphs

theorem Graph.IsDrawing.exists_cover {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) : ∃ (ps : List Schoenflies.Piece), G.pointSet drawing = G.vertexSet ∪ Schoenflies.cover ps

The point set of a finite plane graph with polygonal edges is its vertex set together with finitely many straight segments. The blueprint's "write every edge as a finite union of straight segments".

theorem Graph.IsDrawing.exists_segmentCover {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) (hincident : ∀ z ∈ G.vertexSet, ∃ (e : β), G.Inc e z) : ∃ (ps : List Schoenflies.Piece), (∀ P ∈ ps, P.Nondeg) ∧ Schoenflies.cover ps = G.pointSet drawing ∧ ∀ P ∈ ps, ∃ e ∈ G.edgeSet, P.seg ⊆ edgeArc drawing e

A finite polygonal plane graph without isolated vertices is carried exactly by finitely many nondegenerate straight segments. The incidence hypothesis removes the isolated-vertex term from IsDrawing.exists_cover: every vertex already belongs to the segment cover.

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

Local structure of a polygonal skeleton (lem:local-skeleton-structure): a point of a finite polygonal plane graph has a local radius, hence a disk in which the graph is exactly finitely many radial segments.

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

The local branches of a finite polygonal plane graph at a point are finitely many.

theorem Graph.IsDrawing.openSegment_subset_face {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} {r : ℝ} {y : Schoenflies.Plane} (hr : Schoenflies.IsLocalRadius (G.pointSet drawing) x r) (hy : y ∈ Metric.ball x r) (hyE : y ∈ G.exterior drawing) : openSegment ℝ x y ⊆ G.face drawing y

The access arc. A point of the exterior inside a local disk about x is joined to x by a straight segment lying, except for x itself, in that point's own face.

This is lem:polygonal-side-accessibility with everything but the choice of y discharged: the consumer picks y in the face it cares about (possible because the face accumulates at x), shrinks the radius with IsLocalRadius.mono until the disk also misses whatever else it must avoid, and reads off a polygonal access arc. No sector has to be named: the half-open segment does the work the blueprint's sector does.