Simplicity of restored edge routes

Each edge receives zero, one or two new spokes according to its two separate original endpoint occurrences. All real segment contacts are checked. In particular a retained target loop can become an open source edge, or close again at one new source center.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.restoredRoute_simple {G : Graph} {u v : ℕ} {D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing} (hD : D.IsEmbedding) (huv : u ≠ v) {ρ : ℝ} (hρ : 0 < ρ) (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) (e : Fin G.edges.length) : (D.restoredRoute ρ a b e).IsSimple

Separated local fans reattach every retained edge as a continuously simple route. The exterior contact hypotheses are obtained from the old embedding's restriction.