Literal outgoing germs of restored routes

Affected ends point from the corresponding new center to their own cut port. Unaffected ends retain their old argument, including when cutting the opposite end changes the length of a one-segment route. The selected edge keeps its ordered connector direction.

theorem Cslib.Complexity.Graph.PolygonalDrawing.germ_restoredRoute_active {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) (side : Bool) (hactive : Dart.vertex (e, side) = u ∨ Dart.vertex (e, side) = v) : (D.restoredRoute ρ a b e).germ side = D.cutPort ρ ((contractedIndex G u v) e, side) - D.restoredVertex a b (Dart.vertex (e, side))

Each restored incident end has its own actual straight spoke as outgoing germ.

theorem Cslib.Complexity.Graph.PolygonalDrawing.germ_restoredRoute_inactive {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (ρ : ℝ) (a b : ℂ) (e : Fin G.edges.length) (side : Bool) (hinactive : ¬(Dart.vertex (e, side) = u ∨ Dart.vertex (e, side) = v)) : (D.restoredRoute ρ a b e).germ side = (D.outsideRoute v ρ ((contractedIndex G u v) e)).germ side

An unaffected end retains the outgoing germ of its exterior piece.

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

Every exterior cut preserves the literal outgoing direction of the old actual route.

theorem Cslib.Complexity.Graph.PolygonalDrawing.germ_restoration_retained {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (ρ : ℝ) (a b : ℂ) (d : G.Dart) : (D.restoration huv ρ a b).germ (RotationSystem.retainedLastEdgeDart G u v d) = (D.restoredRoute ρ a b d.1).germ d.2

A retained actual source dart has exactly its attached route's outgoing germ.

theorem Cslib.Complexity.Graph.PolygonalDrawing.germ_restoration_last {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (ρ : ℝ) (a b : ℂ) (side : Bool) : (D.restoration huv ρ a b).germ (RotationSystem.lastEdgeDart G u v side) = if side = true then a - b else b - a

The selected actual source dart has the exact oriented connector germ.

theorem Cslib.Complexity.Graph.PolygonalDrawing.germ_restoration_lift_active {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (huv : u ≠ v) (ρ : ℝ) (a b : ℂ) (d : (RotationSystem.contractLastEdgeGraph G u v).Dart) (hd : d.vertex = v) : (D.restoration huv ρ a b).germ (RotationSystem.contractionLift G u v d) = D.cutPort ρ d - D.restoredVertex a b (RotationSystem.contractionLift G u v d).vertex

A lifted contracted end at either restored vertex has its own literal spoke germ.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.direction_restoration_lift_inactive {G : Graph} {u v : ℕ} {D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing} (hD : D.IsEmbedding) (huv : u ≠ v) {ρ : ℝ} (hρ : 0 < ρ) (hlen : ∀ (d : (RotationSystem.contractLastEdgeGraph G u v).Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) (a b : ℂ) (d : (RotationSystem.contractLastEdgeGraph G u v).Dart) (hd : d.vertex ≠ v) : (D.restoration huv ρ a b).direction (RotationSystem.contractionLift G u v d) = D.direction d

At an unchanged vertex, a lifted end retains its old literal geometric direction.