Embedding of the actual graph after nonloop restoration

The actual retained routes and selected connector satisfy every continuous embedding condition. The radius and split geometry are derived internally in the realization API.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoration_edge_cases (G : Graph) (u v : ℕ) (e : Fin (RotationSystem.lastEdgeGraph G u v).edges.length) : (∃ (j : Fin G.edges.length), e = (RotationSystem.retainedLastEdgeDart G u v (j, false)).1) ∨ e = (RotationSystem.lastEdgeDart G u v false).1

Each source edge occurrence is retained or is the selected final occurrence.

theorem Cslib.Complexity.Graph.PolygonalDrawing.vertex_restoration_retained (G : Graph) (u v : ℕ) (e : Fin G.edges.length) (side : Bool) : Dart.vertex ((RotationSystem.retainedLastEdgeDart G u v (e, false)).1, side) = Dart.vertex (e, side)

An actual retained source edge keeps its original named endpoints.

theorem Cslib.Complexity.Graph.PolygonalDrawing.vertex_restoration_last (G : Graph) (u v : ℕ) (side : Bool) : Dart.vertex ((RotationSystem.lastEdgeDart G u v false).1, side) = if side = true then v else u

The actual selected source edge has its original ordered named endpoints.

theorem Cslib.Complexity.Graph.PolygonalDrawing.route_restoration_retained {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) : (D.restoration huv ρ a b).route (RotationSystem.retainedLastEdgeDart G u v (e, false)).1 = D.restoredRoute ρ a b e

The actual retained route of the restoration is its two-end attachment constructor.

theorem Cslib.Complexity.Graph.PolygonalDrawing.route_restoration_last {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (ρ : ℝ) (a b : ℂ) : (D.restoration huv ρ a b).route (RotationSystem.lastEdgeDart G u v false).1 = Polygonal.Route.line a b

The actual selected route is the oriented single-segment connector.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.restoration {G : Graph} {u v : ℕ} {D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing} (hD : D.IsEmbedding) (huv : u ≠ v) {ρ : ℝ} (hρ : 0 < ρ) (hpoints : ∀ w ∈ (RotationSystem.contractLastEdgeGraph G u v).vertices, D.vertex w ∈ Metric.closedBall (D.vertex v) ρ → w = v) (hlen : ∀ (d : (RotationSystem.contractLastEdgeGraph G u v).Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) (hsimple : ∀ (e : Fin (RotationSystem.contractLastEdgeGraph G u v).edges.length), (D.outsideRoute v ρ e).IsSimple) (hcut : ∀ (e : Fin (RotationSystem.contractLastEdgeGraph G u v).edges.length) (i : Fin (D.outsideRoute v ρ e).segments), ∀ t ∈ Set.Icc 0 1, (D.outsideRoute v ρ e).eval i t ∈ Metric.closedBall (D.vertex v) ρ → ∃ (side : Bool), (D.outsideRoute v ρ e).AtEnd i t side ∧ Dart.vertex (e, side) = v ∧ (D.outsideRoute v ρ e).eval i t = D.cutPort ρ (e, side)) {a b : ℂ} (ha : a ∈ Metric.ball (D.vertex v) ρ) (hb : b ∈ Metric.ball (D.vertex v) ρ) (f : ℂ →ᵃ[ℝ] ℝ) (hsep : f b < f a) (hpa : ∀ (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑d).vertex = u → f a < f (D.cutPort ρ ↑d)) (hpb : ∀ (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑d).vertex = v → f (D.cutPort ρ ↑d) < f b) : (D.restoration huv ρ a b).IsEmbedding

The restored actual drawing is an embedding. Every continuous contact condition is proved for its real segments; no abstract patch or assumed target embedding is substituted.