The sector decomposition of a local disk, and the branches that cut it

Schoenflies/SkeletonLocal.lean proves the radial half of Lemma "Local structure of a polygonal skeleton" (lem:local-skeleton-structure): a point x of a finite polygonal plane graph has a radius r at which the closed disk meets the point set exactly in x together with the radii in the local directions Schoenflies.localDirs. Two things the blueprint proves are missing there, and this module supplies them.

1. The sectors

"Consequently B(x,r) \ |G| is a finite union of open circular sectors" is proved here, in the form the blueprint states it: the punctured disk is the union, over the consecutive pairs of local directions, of the open sectors between them (Schoenflies.IsLocalRadius.ball_diff_eq_iUnion_cone), each of which is open, connected, nonempty and disjoint from the graph. The sector is Plane.cone x (Plane.arcCCW d w) r, the object Schoenflies/Strip.lean already builds; nothing new is defined for it. The union is disjoint (Schoenflies.cone_disjoint_of_isSectorPair), so each sector is exactly a connected component of the punctured disk (Schoenflies.IsLocalRadius.connectedComponentIn_eq_cone).

"Consecutive" is Plane.IsSectorPair D d w: both are in D, they are distinct, and no member of D lies strictly inside arcCCW d w. No angle and no sorting is visible in that definition, and none is used at a call site. The existence proof does sort, and this is the piece with no analogue on main: read as a ternary cyclic order, Plane.arcCCW obeys rotation (Plane.mem_arcCCW_rotate), asymmetry (Plane.notMem_arcCCW_swap, Plane.notMem_arcCCW_asymm), two transitivity laws (Plane.arcCCW_trans, Plane.arcCCW_trans') and — for genuine directions — totality (Plane.mem_arcCCW_total). All of them are pure sign-of-det facts, and the two transitivity laws are one instance each of the Grassmann identity Plane.det_mul_det_add; none of them needs a nondegeneracy hypothesis. Cut at any direction outside D and the cyclic order becomes a linear order; the greatest and the least element of D in it bound the sector containing the cut (Plane.exists_isSectorPair).

2. The branches

On main nothing links localDirs to the edges of the graph, so "with pairwise distinct directions" holds only because a set has distinct members. The blueprint derives it, and that derivation is the mathematical content of the lemma. It is here:

• Graph.IsDrawing.exists_edge_radial and Graph.IsDrawing.edge_radial_unique — each radial segment lies inside exactly one edge arc. The relative interior of the segment is connected and contains no vertex, so Graph.IsDrawing.unique_edge_at makes "the edge through this point" locally constant on it, and the edge arcs being closed and finitely many makes it constant.
• Graph.IsDrawing.not_three_localDirs_on_edge — one edge carries at most two of them. The parametrization of an edge is a continuous injection of a compact interval, hence a closed map, so each radial segment pulls back to an interval of parameters; three such intervals all contain the parameter of x, all reach beyond it, and meet pairwise nowhere else, which is impossible on a line.
• Graph.IsDrawing.localDirs_ncard_le — the two together, counted: there are at most twice as many local directions as edges. This is what makes localDirs a count of branches.

Both steps need a radius at which the disk contains no vertex other than x, which Schoenflies.IsLocalRadius does not record and does not imply — a local radius may perfectly well contain other vertices, sitting out along the radial segments. Graph.IsLocalDisk adds that clause and Graph.IsDrawing.exists_isLocalDisk produces it.

What the consumer gets

lem:polygonal-side-accessibility wants, at once: the finitely many sectors, that each is connected and misses the skeleton, one that meets the prescribed face, and a short straight segment from x into it. Graph.exists_access_sector hands over all four about one named sector, so nothing has to be composed at the call site. The straight segment needs no shortening: a sector is star-shaped about its apex (Schoenflies.openSegment_subset_cone_arcCCW), so (x, y) lies in the very sector y is in.

The two-branch hypothesis

The sector decomposition and Graph.exists_access_sector assume that x has at least two local directions. That is not cosmetic: with one local direction the complement of the ray in the disk is a genuine sector of full turn, and arcCCW d d is empty, so it is not of the form arcCCW d w for d, w ∈ localDirs; with none it is the punctured disk. The consumer form is Graph.IsDrawing.exists_access_region, which returns the connected component of y in the punctured disk — a set with every property of a sector that the accessibility argument uses, but with no claim that it is bounded by two local directions. Whether the two degenerate punctured disks are connected is not settled here; it is not needed, because the component is connected by construction.

Blueprint

• Schoenflies.IsLocalRadius.ball_diff_eq_iUnion_cone, Schoenflies.IsLocalRadius.cone_subset_ball_diff, Schoenflies.IsLocalRadius.isConnected_cone, Schoenflies.isOpen_cone_arcCCW, Schoenflies.cone_disjoint_of_isSectorPair, Schoenflies.IsLocalRadius.connectedComponentIn_eq_cone — "consequently B(x,r) \ |G| is a finite union of open circular sectors" of lem:local-skeleton-structure.
• Graph.IsDrawing.exists_edge_radial, Graph.IsDrawing.edge_radial_unique, Graph.IsDrawing.not_three_localDirs_on_edge, Graph.IsDrawing.localDirs_ncard_le — "two of these radial segments with a common direction would have overlapping relative interiors, which is impossible", the distinct-directions step of the same lemma.
• Graph.IsLocalDisk, Graph.IsDrawing.exists_isLocalDisk — the radius r₀ of the same lemma, with the vertex clause the drawing axioms need.
• Graph.exists_access_sector, Graph.IsDrawing.exists_access_region — "each sector is connected and disjoint from the skeleton … 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.
• Plane.mem_arcCCW_rotate, Plane.notMem_arcCCW_swap, Plane.arcCCW_trans, Plane.arcCCW_trans', Plane.mem_arcCCW_total, Plane.exists_isSectorPair, Plane.IsSectorPair.unique — the cyclic order of finitely many directions. app:background, item 1 lists the two arcs bounded by two directions but not their cyclic order; this is the part of "pairwise distinct directions" that the background package does not cover.

An extreme element of a finite set

The counterclockwise order of directions is a bare relation, not an order instance, so the sorting step is stated for a relation that is total and transitive on the set in question.

theorem Schoenflies.exists_greatest_of_finite {α : Type u_1} {R : α → α → Prop} {D : Set α} (hfin : D.Finite) (hne : D.Nonempty) (htot : ∀ a ∈ D, ∀ b ∈ D, a ≠ b → R a b ∨ R b a) (htr : ∀ a ∈ D, ∀ b ∈ D, ∀ c ∈ D, R a b → R b c → R a c) : ∃ m ∈ D, ∀ a ∈ D, a ≠ m → R a m

A finite nonempty set on which a relation is total and transitive has a greatest element.

The cyclic order of directions

Plane.arcCCW u w is, by definition, the set of d for which at least two of the three consecutive orientation forms of the triple (u, d, w) are positive — Sedgewick's ccw predicate on that triple. Reading it as a ternary cyclic order rather than as an arc is what makes a finite set of directions sortable without an angle: the three lemmas below are exactly the axioms of a cyclic order (rotation, asymmetry, transitivity), and they hold with no nondegeneracy hypothesis at all.

theorem Schoenflies.Plane.det_mul_det_add (a b c e : Plane) : a.det b * c.det e - a.det c * b.det e + a.det e * b.det c = 0

The Grassmann identity for four vectors of the plane: any three of them are linearly dependent, and expanding that dependence against the fourth gives this relation among the six orientation forms. Every transitivity below is one instance of it.

theorem Schoenflies.Plane.mem_arcCCW_rotate {u w d : Plane} : d ∈ u.arcCCW w ↔ w ∈ d.arcCCW u

Rotation. The cyclic order is invariant under rotating its triple: d lies on the arc counterclockwise from u to w exactly when w lies on the arc counterclockwise from d to u.

theorem Schoenflies.Plane.left_notMem_arcCCW (u w : Plane) : u ∉ u.arcCCW w

A bounding ray is not on its own arc.

theorem Schoenflies.Plane.right_notMem_arcCCW (u w : Plane) : w ∉ u.arcCCW w

The other bounding ray is not on the arc either.

theorem Schoenflies.Plane.notMem_arcCCW_swap {u v w : Plane} (h : v ∈ u.arcCCW w) : u ∉ v.arcCCW w

Asymmetry. Transposing the first two entries of the triple negates the cyclic order: if v is counterclockwise of u before w, then u is not counterclockwise of v before w. Two of the three orientation forms would have to be positive and two negative.

The two transitivity laws

Both are the same real-arithmetic fact, extracted so that the det bookkeeping happens once. Write p₁ = det u w, p₂ = det w v, p₃ = det v u for the triple (u, w, v), and q₂ = det v d, q₃ = det d u for the missing entries of (u, v, d); note det u v = -p₃. The Grassmann identity turns into p₃ * s₂ = q₃ * p₂ - p₁ * q₂ with s₂ = det w d.

theorem Schoenflies.Plane.arcCCW_trans {u v w d : Plane} (h₁ : w ∈ u.arcCCW v) (h₂ : v ∈ u.arcCCW d) : w ∈ u.arcCCW d

Transitivity, first form. Counterclockwise order seen from a fixed ray u is transitive: if w comes before v and v before d, then w comes before d. This is what makes a finite set of directions linearly ordered once a ray to cut at has been chosen.

theorem Schoenflies.Plane.arcCCW_trans' {u v w d : Plane} (h₁ : w ∈ u.arcCCW v) (h₂ : v ∈ u.arcCCW d) : v ∈ w.arcCCW d

Transitivity, second form. The same three rays, read from w instead of from u: if w comes before v and v before d as seen from u, then v lies on the arc counterclockwise from w to d. This is the step that turns "nothing of the finite set lies between u and the extreme rays" into "nothing lies inside the sector".

Totality

Totality is the only one of the four order axioms that needs a hypothesis: the two rays being compared must be genuine directions, distinct from each other and from the ray cut at.

theorem Schoenflies.Plane.eq_dir_or_eq_neg_dir {u v : Plane} (hu : u ≠ 0) (hv : v.IsDirection) (h : u.det v = 0) : v = u.dir ∨ v = -u.dir

A unit vector parallel to u is one of the two unit vectors along the line of u.

theorem Schoenflies.Plane.mem_arcCCW_total {u v w : Plane} (hu : u ≠ 0) (hv : v.IsDirection) (hw : w.IsDirection) (hvw : v ≠ w) (hvu : v ≠ u.dir) (hwu : w ≠ u.dir) : v ∈ u.arcCCW w ∨ w ∈ u.arcCCW v

Totality. Two distinct directions, neither of them the direction of u, are comparable in the counterclockwise order seen from u. The three degenerate configurations — one of them opposite to u, or the two opposite to each other — are exactly the three hypotheses of total_aux.

Consecutive directions, and the sector they bound

A finite set D of directions cuts the circle of directions into arcs. A pair (d, w) of members of D is consecutive when nothing of D lies strictly between them: that is the whole of Plane.IsSectorPair, and it is stated with no reference to a sorting of D.

The existence proof does sort, but only relative to a free direction u — one that is not in D. Seen from u the cyclic order becomes the linear order v ≺ w ↔ v ∈ arcCCW u w, whose greatest and least elements are the two rays bounding the sector u lies in.

theorem Schoenflies.Plane.notMem_arcCCW_asymm {u v w : Plane} (h : v ∈ u.arcCCW w) : w ∉ u.arcCCW v

Asymmetry, transposing the last two entries.

theorem Schoenflies.Plane.dir_self {u : Plane} (hu : u.IsDirection) : u.dir = u

A unit vector is its own direction.

theorem Schoenflies.Plane.eq_neg_of_det_eq_zero {u w : Plane} (hu : u.IsDirection) (hw : w.IsDirection) (hne : u ≠ w) (h : u.det w = 0) : w = -u

Two distinct directions killed by the orientation form are opposite.

theorem Schoenflies.Plane.arcCCW_neg (u : Plane) : u.arcCCW (-u) = {v : Plane | 0 < u.det v}

The arc counterclockwise from a ray to its opposite is the open half-plane on its left. This is the sector of a point with exactly two local branches, in a straight line.

theorem Schoenflies.Plane.isConnected_arcCCW_ball_of_ne {u w : Plane} {ρ : ℝ} (hu : u.IsDirection) (hw : w.IsDirection) (hne : u ≠ w) (hρ : 0 < ρ) : IsConnected (u.arcCCW w ∩ Metric.ball 0 ρ)

The sector between two distinct directions is connected, whether or not they are opposite. Plane.isConnected_arcCCW_ball assumes det u w ≠ 0, which excludes the straight case; there the arc is a half-plane, and convex.

theorem Schoenflies.Plane.isConnected_cone_arcCCW_of_ne {u w : Plane} {ρ : ℝ} (x : Plane) (hu : u.IsDirection) (hw : w.IsDirection) (hne : u ≠ w) (hρ : 0 < ρ) : IsConnected (x.cone (u.arcCCW w) ρ)

The sector of radius ρ at x between two distinct directions is connected.

def Schoenflies.Plane.IsSectorPair (D : Set Plane) (d w : Plane) : Prop

d and w are consecutive in D: both belong to D, they are distinct, and no member of D lies strictly inside the arc counterclockwise from d to w. That arc is then a sector of the complement of D.

Equations

• Schoenflies.Plane.IsSectorPair D d w = (d ∈ D ∧ w ∈ D ∧ d ≠ w ∧ ∀ v ∈ D, v ∉ d.arcCCW w)

def Schoenflies.Plane.sectorPairs (D : Set Plane) : Set (Plane × Plane)

The consecutive pairs of a finite set of directions, as a set. Indexing the sectors by this set rather than by a chosen cyclic successor keeps the construction choice-free.

Equations

• Schoenflies.Plane.sectorPairs D = {p : Schoenflies.Plane × Schoenflies.Plane | Schoenflies.Plane.IsSectorPair D p.1 p.2}

theorem Schoenflies.Plane.mem_sectorPairs_iff {D : Set Plane} {p : Plane × Plane} : p ∈ sectorPairs D ↔ IsSectorPair D p.1 p.2

theorem Schoenflies.Plane.sectorPairs_finite {D : Set Plane} (hfin : D.Finite) : (sectorPairs D).Finite

theorem Schoenflies.Plane.exists_isSectorPair {u : Plane} {D : Set Plane} (hfin : D.Finite) (hdir : ∀ v ∈ D, v.IsDirection) (h2 : ∃ a ∈ D, ∃ b ∈ D, a ≠ b) (hu : u ≠ 0) (hud : u.dir ∉ D) : ∃ (d : Plane) (w : Plane), IsSectorPair D d w ∧ u ∈ d.arcCCW w

Every free direction lies in a sector. Given a finite set D of at least two directions and a direction not in D, there is a consecutive pair of D whose arc contains it. The two bounding rays are the greatest and the least element of D in the counterclockwise order seen from the free direction.

The sector a direction lies in is unique

Distinct consecutive pairs bound disjoint arcs, so the sectors are a partition of the free directions and not merely a cover. The proof is the same cyclic-order calculation as the existence proof, run backwards: a free direction inside arcCCW d w forces d to be the greatest and w the least element of D in the order seen from it.

theorem Schoenflies.Plane.mem_arcCCW_rev_of_notMem {d w z : Plane} (hd : d.IsDirection) (hw : w.IsDirection) (hdw : d ≠ w) (hz : z.IsDirection) (hzd : z ≠ d) (hzw : z ≠ w) (h : z ∉ d.arcCCW w) : z ∈ w.arcCCW d

A direction that is neither bounding ray of an arc and is not on it lies on the complementary arc. Both the generic case and the straight case w = -d are covered.

theorem Schoenflies.Plane.IsSectorPair.mem_arcCCW_left {D : Set Plane} {d w v z : Plane} (hp : IsSectorPair D d w) (hdir : ∀ y ∈ D, y.IsDirection) (hv : v ∈ d.arcCCW w) (hz : z ∈ D) (hzd : z ≠ d) : z ∈ v.arcCCW d

d is the greatest element of D seen from a direction of its sector.

theorem Schoenflies.Plane.IsSectorPair.mem_arcCCW_right {D : Set Plane} {d w v z : Plane} (hp : IsSectorPair D d w) (hdir : ∀ y ∈ D, y.IsDirection) (hv : v ∈ d.arcCCW w) (hz : z ∈ D) (hzw : z ≠ w) : w ∈ v.arcCCW z

w is the least element of D seen from a direction of its sector.

theorem Schoenflies.Plane.IsSectorPair.unique {D : Set Plane} {d w d' w' v : Plane} (hdir : ∀ y ∈ D, y.IsDirection) (hp : IsSectorPair D d w) (hp' : IsSectorPair D d' w') (hv : v ∈ d.arcCCW w) (hv' : v ∈ d'.arcCCW w') : d = d' ∧ w = w'

The sector containing a free direction is unique.

theorem Schoenflies.Plane.arcCCW_disjoint_of_isSectorPair {D : Set Plane} {d w d' w' : Plane} (hdir : ∀ y ∈ D, y.IsDirection) (hp : IsSectorPair D d w) (hp' : IsSectorPair D d' w') (hne : d ≠ d' ∨ w ≠ w') : Disjoint (d.arcCCW w) (d'.arcCCW w')

Distinct consecutive pairs bound disjoint arcs.

The punctured local disk is a finite union of open sectors

This is the last clause of lem:local-skeleton-structure, "consequently B(x,r) \ |G| is a finite union of open circular sectors". The sectors are indexed by the consecutive pairs of local directions, and there are finitely many of them because there are finitely many local directions.

theorem Schoenflies.IsLocalRadius.cone_subset_ball_diff {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) {d w : Plane} (hp : Plane.IsSectorPair (localDirs S x) d w) : x.cone (d.arcCCW w) r ⊆ Metric.ball x r \ S

A sector between two consecutive local directions misses S entirely: no point of it is x, because the origin lies on no arc, and no point of it points along a local direction.

theorem Schoenflies.IsLocalRadius.isConnected_cone {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) {d w : Plane} (hp : Plane.IsSectorPair (localDirs S x) d w) : IsConnected (x.cone (d.arcCCW w) r)

Each sector is connected — and in particular nonempty.

theorem Schoenflies.isOpen_cone_arcCCW (x d w : Plane) (r : ℝ) : IsOpen (x.cone (d.arcCCW w) r)

Each sector is open.

theorem Schoenflies.openSegment_subset_cone_arcCCW {x z : Plane} {r : ℝ} {d w : Plane} (hz : z ∈ x.cone (d.arcCCW w) r) : openSegment ℝ x z ⊆ x.cone (d.arcCCW w) r

A sector is star-shaped about the apex. A straight segment from x towards a point of a sector stays in that sector: this is the blueprint's "a short straight segment from x into that sector is a polygonal access arc", with no shortening needed.

theorem Schoenflies.IsLocalRadius.ball_diff_eq_iUnion_cone {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) : Metric.ball x r \ S = ⋃ p ∈ Plane.sectorPairs (localDirs S x), x.cone (p.1.arcCCW p.2) r

The punctured local disk is the union of the sectors between consecutive local directions. The last clause of lem:local-skeleton-structure. The hypothesis is that x has at least two local branches; with fewer, B(x,r) \ S is connected and is not an arc sector (see the module note).

theorem Schoenflies.cone_disjoint_of_isSectorPair {S : Set Plane} {x : Plane} {r : ℝ} {d w d' w' : Plane} (hp : Plane.IsSectorPair (localDirs S x) d w) (hp' : Plane.IsSectorPair (localDirs S x) d' w') (hne : d ≠ d' ∨ w ≠ w') : Disjoint (x.cone (d.arcCCW w) r) (x.cone (d'.arcCCW w') r)

The sectors are pairwise disjoint, so the decomposition of the punctured disk is a partition and not merely a cover.

theorem Schoenflies.IsLocalRadius.connectedComponentIn_eq_cone {S : Set Plane} {x z : Plane} {r : ℝ} (h : IsLocalRadius S x r) (hfin : (localDirs S x).Finite) (h2 : ∃ a ∈ localDirs S x, ∃ b ∈ localDirs S x, a ≠ b) {d w : Plane} (hp : Plane.IsSectorPair (localDirs S x) d w) (hz : z ∈ x.cone (d.arcCCW w) r) : connectedComponentIn (Metric.ball x r \ S) z = x.cone (d.arcCCW w) r

Each sector is a connected component of the punctured disk. The sectors are open, connected, pairwise disjoint and cover, so each is exactly the component of any of its points. This is what makes "the sector y lies in" and "the component of y" the same set, and hence Graph.exists_access_region and Graph.exists_access_sector two readings of one theorem.

Radial segments, two at a time

Two radial segments with distinct directions meet only at the centre, and the relative interior of a radial segment stays strictly inside the disk and off the centre. These are the two facts that turn the drawing axioms into the distinct-directions clause of lem:local-skeleton-structure.

theorem Schoenflies.IsLocalRadius.radial_subset {S : Set Plane} {x : Plane} {r : ℝ} (h : IsLocalRadius S x r) {d : Plane} (hd : d ∈ localDirs S x) : segment ℝ x (x + r • d) ⊆ S

A radius in a local direction lies in the set.

theorem Schoenflies.radial_inter_radial {x : Plane} {r : ℝ} {d₁ d₂ : Plane} (hd₁ : d₁.IsDirection) (hd₂ : d₂.IsDirection) (hne : d₁ ≠ d₂) (hr : 0 < r) : segment ℝ x (x + r • d₁) ∩ segment ℝ x (x + r • d₂) ⊆ {x}

Two radial segments with distinct directions meet only at the centre.

theorem Schoenflies.mem_openSegment_radial {x z : Plane} {r : ℝ} {d : Plane} (hd : d.IsDirection) (hr : 0 < r) (hz : z ∈ openSegment ℝ x (x + r • d)) : z ≠ x ∧ dist z x < r

The relative interior of a radius avoids the centre and stays strictly inside the disk.

Finite polygonal plane graphs

Schoenflies/SkeletonLocal.lean produces a local radius from the point set of the graph, and never looks at the edges. The blueprint's proof does: it derives the pairwise distinctness of the branch directions from the drawing axioms. That derivation is what follows, and it needs one more thing from the radius than IsLocalRadius records — that the disk contains no vertex other than x — because the drawing axioms only control edges away from the vertices.

structure Graph.IsLocalDisk {β : Type u_1} (G : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) (x : Schoenflies.Plane) (r : ℝ) : Prop

A local disk of a plane graph at x: a local radius for the point set whose closed disk contains no vertex but possibly x itself.

The second clause is not a consequence of the first — a local radius may well contain other vertices, sitting on the radial segments — and it is exactly what makes the relative interior of each radial segment a set of non-vertex points, where IsDrawing.unique_edge_at applies.

• isLocalRadius : Schoenflies.IsLocalRadius (G.pointSet drawing) x r

  The disk meets the point set exactly in the radial segments.

• vertex_eq (v : Schoenflies.Plane) : v ∈ G.vertexSet → dist v x ≤ r → v = x

  No vertex other than x is within r of x.

theorem Graph.IsLocalDisk.pos {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} {r : ℝ} (h : G.IsLocalDisk drawing x r) : 0 < r

theorem Graph.IsLocalDisk.mono {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} {r : ℝ} (h : G.IsLocalDisk drawing x r) {ε : ℝ} (hε : 0 < ε) (hle : ε ≤ r) : G.IsLocalDisk drawing x ε

theorem Graph.IsDrawing.exists_isLocalDisk {β : 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 : ℝ), G.IsLocalDisk drawing x r

A local disk exists, by shrinking a local radius below the distance to the other vertices.

Each radial segment lies on exactly one edge

The relative interior of a radial segment is connected and meets no vertex, so IsDrawing.unique_edge_at makes "the edge through this point" a locally constant function on it; the edge arcs being closed and finitely many turns local constancy into global constancy.

theorem Graph.IsDrawing.exists_edge_radial {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x d : Schoenflies.Plane} {r : ℝ} [G.Finite] (h : G.IsDrawing drawing) (hr : G.IsLocalDisk drawing x r) (hd : d ∈ Schoenflies.localDirs (G.pointSet drawing) x) : ∃ e ∈ G.edgeSet, segment ℝ x (x + r • d) ⊆ edgeArc drawing e

Existence. At a local disk radius, a radial segment lies inside a single edge arc.

theorem Graph.IsDrawing.edge_radial_unique {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x d : Schoenflies.Plane} {r : ℝ} (h : G.IsDrawing drawing) (hr : G.IsLocalDisk drawing x r) (hdir : d.IsDirection) {e f : β} (he : e ∈ G.edgeSet) (hf : f ∈ G.edgeSet) (hse : segment ℝ x (x + r • d) ⊆ edgeArc drawing e) (hsf : segment ℝ x (x + r • d) ⊆ edgeArc drawing f) : e = f

Uniqueness. Two edges carrying the same radial segment are the same edge: the relative interior of the segment is off the vertex set, and there a point lies on only one edge.

An edge carries at most two local branches

The parametrization of an edge is a continuous injection of a compact interval, hence a closed map, so the preimage of a connected subset of its arc is connected (IsPreconnected.preimage_of_isClosedMap). Three radial segments inside one edge arc therefore pull back to three intervals of parameters, each containing the parameter of x and a point other than it, and meeting pairwise in nothing else. Two of the three lie on the same side of the parameter of x, and then the smaller of the two extra points belongs to both intervals.

theorem Graph.IsDrawing.not_three_localDirs_on_edge {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} {r : ℝ} (h : G.IsDrawing drawing) (hr : G.IsLocalDisk drawing x r) {e : β} (he : e ∈ G.edgeSet) {d₁ d₂ d₃ : Schoenflies.Plane} (hd₁ : d₁.IsDirection) (hd₂ : d₂.IsDirection) (hd₃ : d₃.IsDirection) (h₁₂ : d₁ ≠ d₂) (h₁₃ : d₁ ≠ d₃) (h₂₃ : d₂ ≠ d₃) (hs₁ : segment ℝ x (x + r • d₁) ⊆ edgeArc drawing e) (hs₂ : segment ℝ x (x + r • d₂) ⊆ edgeArc drawing e) (hs₃ : segment ℝ x (x + r • d₃) ⊆ edgeArc drawing e) : False

An edge carries at most two local branches at x — the blueprint's "two of these radial segments with a common direction would have overlapping relative interiors, which is impossible", in the shape it is actually used: three distinct directions cannot all be carried by one edge. Together with IsDrawing.exists_edge_radial and IsDrawing.edge_radial_unique this says that the local directions at x are in bijection with the local branches, so the radial segments of lem:local-skeleton-structure really do have pairwise distinct directions.

theorem Graph.IsDrawing.localDirs_ncard_le {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} {r : ℝ} [G.Finite] (h : G.IsDrawing drawing) (hr : G.IsLocalDisk drawing x r) (hfin : (Schoenflies.localDirs (G.pointSet drawing) x).Finite) : (Schoenflies.localDirs (G.pointSet drawing) x).ncard ≤ 2 * G.edgeSet.ncard

The local directions are the local branches, counted. Each local direction is carried by exactly one edge and each edge carries at most two of them, so there are at most twice as many local directions as edges. This is the quantitative packaging of the blueprint's "finitely many straight segments from x with pairwise distinct directions": the count is a count of branches, not of an unrelated set of rays.

The access sector

lem:polygonal-side-accessibility needs four things at once: the finitely many sectors, that each is connected and misses the skeleton, one that meets the prescribed face, and a short straight segment from x into it. IsDrawing.exists_access_sector delivers all four about a single named sector, so that the consumer never has to compose three lemmas.

theorem Graph.exists_access_sector {β : 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) (hfin : (Schoenflies.localDirs (G.pointSet drawing) x).Finite) (h2 : ∃ a ∈ Schoenflies.localDirs (G.pointSet drawing) x, ∃ b ∈ Schoenflies.localDirs (G.pointSet drawing) x, a ≠ b) (hy : y ∈ Metric.ball x r) (hyE : y ∈ G.exterior drawing) : ∃ (d : Schoenflies.Plane) (w : Schoenflies.Plane), Schoenflies.Plane.IsSectorPair (Schoenflies.localDirs (G.pointSet drawing) x) d w ∧ y ∈ x.cone (d.arcCCW w) r ∧ IsOpen (x.cone (d.arcCCW w) r) ∧ IsConnected (x.cone (d.arcCCW w) r) ∧ x.cone (d.arcCCW w) r ⊆ Metric.ball x r \ G.pointSet drawing ∧ x.cone (d.arcCCW w) r ⊆ G.face drawing y ∧ openSegment ℝ x y ⊆ x.cone (d.arcCCW w) r

The access sector (lem:polygonal-side-accessibility, the local step). A point y of the exterior inside a local disk about x lies in one of the sectors between consecutive local directions, and that sector is open, connected, nonempty, disjoint from the graph, contained in y's own face, and reached from x by the straight segment (x, y).

theorem Graph.IsDrawing.exists_access_region {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} {r : ℝ} [G.Finite] (h : G.IsDrawing drawing) {y : Schoenflies.Plane} (hr : Schoenflies.IsLocalRadius (G.pointSet drawing) x r) (hy : y ∈ Metric.ball x r) (hyE : y ∈ G.exterior drawing) : ∃ (N : Set Schoenflies.Plane), y ∈ N ∧ IsOpen N ∧ IsConnected N ∧ N ⊆ Metric.ball x r \ G.pointSet drawing ∧ N ⊆ G.face drawing y ∧ openSegment ℝ x y ⊆ N

The access region, with no hypothesis on the number of branches. The connected component of y in the punctured disk has every property lem:polygonal-side-accessibility asks of the sector: it is open, connected, misses the graph, lies in y's face, and contains the straight segment from x to y. When x has at least two local branches it is a sector, by Graph.exists_access_sector; with fewer it is the whole punctured disk, which is not an arc sector, and this is the form to use.