Local segment neighborhoods of polygonal graph embeddings

Every declared vertex of a polygonal embedding has a positive-radius ball meeting only first or last segments actually incident to that vertex. The finite neighborhood is constructed from the segment arrangement. Both ends of a loop are retained.

This proves a local straight-segment fact; it does not assume or establish a vertex-split patch, an isotopy theorem, Jordan separation or the numerical-genus bridge.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.exists_vertex_ball {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) (hv : v ∈ G.vertices) : ∃ ε > 0, ∀ (e : Fin G.edges.length) (i : Fin (D.route e).segments), ∀ w ∈ Metric.ball (D.vertex v) ε, w ∈ segment ℝ ((D.route e).point i.castSucc) ((D.route e).point i.succ) → ↑i = 0 ∧ Dart.vertex (e, false) = v ∨ ↑i + 1 = (D.route e).segments ∧ Dart.vertex (e, true) = v

Near a declared vertex, every segment met by an embedding is an actual first or last segment at that named vertex. The radius is proved to exist from finite real geometry.