Closed neighborhoods and cut ports of polygonal embeddings

A declared vertex has a positive closed neighborhood avoiding every other declared point and every nonincident segment. Its radius is smaller than one third of every incident end segment. This includes both separate ends of a loop and imposes no shape on the drawing.

The cut ports are actual real affine points on those end segments, at a common distance from the vertex. They are distinct for distinct incident darts. These are preparation lemmas for local replacement, not a vertex-splitting or general realization theorem.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.exists_restriction_radius {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) (hv : v ∈ G.vertices) : ∃ ρ > 0, (∀ w ∈ G.vertices, D.vertex w ∈ Metric.closedBall (D.vertex v) ρ → w = v) ∧ (∀ (e : Fin G.edges.length) (i : Fin (D.route e).segments), ∀ z ∈ Metric.closedBall (D.vertex v) ρ, z ∈ 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) ∧ ∀ (d : G.Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖

A sufficiently small closed ball isolates the straight star of a declared vertex, avoids the other declared points, and cuts every incident segment before its first third. Repeated vertex declarations and arbitrary natural vertex names are allowed.

noncomputable def Cslib.Complexity.Graph.PolygonalDrawing.cutPort {G : Graph} (D : G.PolygonalDrawing) (ρ : ℝ) (d : G.Dart) : ℂ

The cut port on an actual outgoing end segment, with no chosen angular coordinates.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.dist_cutPort {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) {ρ : ℝ} (hρ : 0 ≤ ρ) (d : G.Dart) : dist (D.cutPort ρ d) (D.vertex d.vertex) = ρ

The common-radius cut port lies at precisely that distance from its own vertex.

theorem Cslib.Complexity.Graph.PolygonalDrawing.cutPort_eq_eval {G : Graph} (D : G.PolygonalDrawing) (ρ : ℝ) (d : G.Dart) : D.cutPort ρ d = (D.route d.1).eval ((D.route d.1).endSegment d.2) (Polygonal.Route.endTime d.2 (ρ / ‖D.germ d‖))

Cutting before the end of the first outgoing segment is an actual segment parameter, including the reversed final segment at the second end of an edge or loop.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.cutPort_mem_support {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) {ρ : ℝ} (hρ : 0 ≤ ρ) (d : G.Dart) (hd : ρ ≤ ‖D.germ d‖) : D.cutPort ρ d ∈ (D.route d.1).support

A cut strictly shorter than its outgoing segment is on that original route.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.arg_cutPort_sub {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) {ρ : ℝ} (hρ : 0 < ρ) (d : G.Dart) : (D.cutPort ρ d - D.vertex d.vertex).arg = (D.germ d).arg

The cut operation preserves the actual outgoing ray in the fixed plane.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.cutPort_injective {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) {ρ : ℝ} (hρ : 0 < ρ) (a b : G.Dart) (hv : a.vertex = b.vertex) (heq : D.cutPort ρ a = D.cutPort ρ b) : a = b

Distinct actual darts at one vertex yield distinct common-radius boundary ports. The two ends of the same loop are included.

noncomputable def Cslib.Complexity.Graph.PolygonalDrawing.restrictionTime {G : Graph} (D : G.PolygonalDrawing) (v : ℕ) (ρ : ℝ) (d : G.Dart) : ℝ

Cut an end precisely when it belongs to the vertex being replaced. The other end of an edge stays unchanged; the two ends of a loop are cut separately.

noncomputable def Cslib.Complexity.Graph.PolygonalDrawing.outsideRoute {G : Graph} (D : G.PolygonalDrawing) (v : ℕ) (ρ : ℝ) (e : Fin G.edges.length) : Polygonal.Route

The exterior part of an edge after cutting at a named vertex. This is route data, not a drawing of a graph with invented port vertices.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.restrictionTime_mem {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hlen : ∀ (d : G.Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) (d : G.Dart) : D.restrictionTime v ρ d ∈ Set.Ico 0 (1 / 3)

A restriction radius gives independent small nonnegative cuts at every edge end.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.restrictionTime_bounds {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hlen : ∀ (d : G.Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) (e : Fin G.edges.length) : 0 ≤ D.restrictionTime v ρ (e, false) ∧ 0 ≤ D.restrictionTime v ρ (e, true) ∧ D.restrictionTime v ρ (e, false) + D.restrictionTime v ρ (e, true) < 1

The two independent end cuts leave a nonempty parameter interval on every route.

theorem Cslib.Complexity.Graph.PolygonalDrawing.endpoint_outsideRoute {G : Graph} (D : G.PolygonalDrawing) (v : ℕ) (ρ : ℝ) (e : Fin G.edges.length) (b : Bool) : (D.outsideRoute v ρ e).endpoint b = if Dart.vertex (e, b) = v then D.cutPort ρ (e, b) else D.vertex (Dart.vertex (e, b))

The two ends of the exterior piece are their respective cut ports or unchanged original endpoints, according to actual incidence with the named vertex.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.outsideRoute_simple {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hlen : ∀ (d : G.Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) (e : Fin G.edges.length) : (D.outsideRoute v ρ e).IsSimple

Exterior pieces retain continuous simplicity, with no assumptions on their slopes, number of bends, loop status or the incidence of their other end.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.support_outsideRoute_subset {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hlen : ∀ (d : G.Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) (e : Fin G.edges.length) : (D.outsideRoute v ρ e).support ⊆ (D.route e).support

Cutting the star does not create any point outside an old edge's continuous support.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.outsideRoute_ball_contact {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) (hlen : ∀ (d : G.Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) (hlocal : ∀ (e : Fin G.edges.length) (i : Fin (D.route e).segments), ∀ z ∈ Metric.closedBall (D.vertex v) ρ, z ∈ 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) (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments) {u : ℝ} (hu : u ∈ Set.Icc 0 1) (hz : (D.outsideRoute v ρ e).eval i u ∈ Metric.closedBall (D.vertex v) ρ) : ∃ (b : Bool), (D.outsideRoute v ρ e).AtEnd i u b ∧ Dart.vertex (e, b) = v ∧ (D.outsideRoute v ρ e).eval i u = D.cutPort ρ (e, b)

Every point where an exterior piece meets the closed replacement ball is its own boundary port at an original end incident to the replaced vertex. Thus an interior patch cannot meet an exterior route interior. Both loop ends remain separate cases.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.exists_restriction {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) (hv : v ∈ G.vertices) : ∃ ρ > 0, (∀ w ∈ G.vertices, D.vertex w ∈ Metric.closedBall (D.vertex v) ρ → w = v) ∧ (∀ (e : Fin G.edges.length), (D.outsideRoute v ρ e).IsSimple) ∧ (∀ (e : Fin G.edges.length), (D.outsideRoute v ρ e).support ⊆ (D.route e).support) ∧ ∀ (e : Fin G.edges.length) (i : Fin (D.outsideRoute v ρ e).segments), ∀ u ∈ Set.Icc 0 1, (D.outsideRoute v ρ e).eval i u ∈ Metric.closedBall (D.vertex v) ρ → ∃ (b : Bool), (D.outsideRoute v ρ e).AtEnd i u b ∧ Dart.vertex (e, b) = v ∧ (D.outsideRoute v ρ e).eval i u = D.cutPort ρ (e, b)

An actual embedding supplies its own common-radius cut and all exterior contact conditions. No local disk, prescribed slopes, port coordinates or patch is a premise. This stops at the exterior pieces: constructing and attaching a split patch is separate.