Actual routes for restoring a contracted nonloop edge

Each retained edge keeps its exterior route and receives a new straight segment at each end incident to either restored endpoint. The two ends are treated independently: an old source edge between the endpoints is reopened from both ends of its target loop. The selected last edge is an actual one-segment connector. This module constructs the route data and proves endpoints; embedding and rotation order require the local split.

def Cslib.Complexity.Graph.PolygonalDrawing.contractedIndex (G : Graph) (u v : ℕ) : Fin G.edges.length ≃ Fin (RotationSystem.contractLastEdgeGraph G u v).edges.length

The retained edge occurrence after contracting a last nonloop edge.

theorem Cslib.Complexity.Graph.PolygonalDrawing.vertex_contractedIndex (G : Graph) (u v : ℕ) (i : Fin G.edges.length) (b : Bool) : Dart.vertex ((contractedIndex G u v) i, b) = Function.update id u v (Dart.vertex (i, b))

Both endpoint occurrences retain their tag and undergo the prescribed name update.

def Cslib.Complexity.Graph.PolygonalDrawing.restoredVertex {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (a b : ℂ) (w : ℕ) : ℂ

Coordinates of the two restored names; all other names retain their old coordinates.

noncomputable def Cslib.Complexity.Graph.PolygonalDrawing.restoreFirst (u v w : ℕ) (a b : ℂ) (p : Polygonal.Route) : Polygonal.Route

Attach a first spoke precisely when its original source end is restored.

noncomputable def Cslib.Complexity.Graph.PolygonalDrawing.restoreLast (u v w : ℕ) (a b : ℂ) (p : Polygonal.Route) : Polygonal.Route

Attach a last spoke independently of the first end, including for target loops.

def Cslib.Complexity.Graph.PolygonalDrawing.attachmentCount (u v w : ℕ) : ℕ

Number of new segments attached at one original endpoint occurrence.

theorem Cslib.Complexity.Graph.PolygonalDrawing.segments_restoreFirst (u v w : ℕ) (a b : ℂ) (p : Polygonal.Route) : (restoreFirst u v w a b p).segments = p.segments + attachmentCount u v w

A first restoration adds exactly one segment at an affected endpoint.

theorem Cslib.Complexity.Graph.PolygonalDrawing.segments_restoreLast (u v w : ℕ) (a b : ℂ) (p : Polygonal.Route) : (restoreLast u v w a b p).segments = p.segments + attachmentCount u v w

A last restoration adds exactly one segment at an affected endpoint.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoredVertex_mem_ball {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) {ρ : ℝ} {a b : ℂ} (ha : a ∈ Metric.ball (D.vertex v) ρ) (hb : b ∈ Metric.ball (D.vertex v) ρ) (w : ℕ) (hw : w = u ∨ w = v) : D.restoredVertex a b w ∈ Metric.ball (D.vertex v) ρ

A restored endpoint remains strictly inside the replacement ball.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoreFirst_eq_prepend {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (w : ℕ) (hw : w = u ∨ w = v) (a b : ℂ) (p : Polygonal.Route) : restoreFirst u v w a b p = Polygonal.Route.prepend (D.restoredVertex a b w) p

At an affected endpoint, first restoration is exactly one prepend.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoreLast_eq_append {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (w : ℕ) (hw : w = u ∨ w = v) (a b : ℂ) (p : Polygonal.Route) : restoreLast u v w a b p = p.append (D.restoredVertex a b w)

At an affected endpoint, last restoration is exactly one append.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoreFirst_eq_self (u v w : ℕ) (hw : ¬(w = u ∨ w = v)) (a b : ℂ) (p : Polygonal.Route) : restoreFirst u v w a b p = p

An unaffected first endpoint retains the entire route data.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoreLast_eq_self (u v w : ℕ) (hw : ¬(w = u ∨ w = v)) (a b : ℂ) (p : Polygonal.Route) : restoreLast u v w a b p = p

An unaffected last endpoint retains the entire route data.

noncomputable def Cslib.Complexity.Graph.PolygonalDrawing.restoredRoute {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) : Polygonal.Route

Exterior retained route with its two original source endpoint occurrences restored.

theorem Cslib.Complexity.Graph.PolygonalDrawing.segments_restoredRoute {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) : (D.restoredRoute ρ a b e).segments = (D.outsideRoute v ρ ((contractedIndex G u v) e)).segments + attachmentCount u v (Dart.vertex (e, false)) + attachmentCount u v (Dart.vertex (e, true))

The two restored end occurrences contribute their new segments independently.

theorem Cslib.Complexity.Graph.PolygonalDrawing.endpoint_restoreFirst (u v w : ℕ) (a b : ℂ) (p : Polygonal.Route) (side : Bool) : (restoreFirst u v w a b p).endpoint side = if side = true then p.finish else if w = u then a else if w = v then b else p.start

A first attachment sets its start and retains its finish.

theorem Cslib.Complexity.Graph.PolygonalDrawing.endpoint_restoreLast (u v w : ℕ) (a b : ℂ) (p : Polygonal.Route) (side : Bool) : (restoreLast u v w a b p).endpoint side = if side = true then if w = u then a else if w = v then b else p.finish else p.start

A last attachment retains its start and sets its finish.

theorem Cslib.Complexity.Graph.PolygonalDrawing.endpoint_restoredRoute {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) (side : Bool) : (D.restoredRoute ρ a b e).endpoint side = D.restoredVertex a b (Dart.vertex (e, side))

The restored exterior piece has exactly the two named source endpoints.

noncomputable def Cslib.Complexity.Graph.PolygonalDrawing.restoration {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (ρ : ℝ) (a b : ℂ) : (RotationSystem.lastEdgeGraph G u v).PolygonalDrawing

Restore the actual source graph's route data. Retained edge indices use their old exterior pieces; the last selected edge is the straight connector from a to b. This constructor does not assert nonintersection or clockwise realization.