Geometric embedding conditions for nonloop restoration

The two new centers stay inside the old isolated neighborhood; all other declared points retain their old coordinates outside it. Duplicate declarations and unused isolated names are retained by membership throughout.

theorem Cslib.Complexity.Graph.PolygonalDrawing.restoredVertex_active_of_mem_closedBall {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) {ρ : ℝ} (hpoints : ∀ w ∈ (RotationSystem.contractLastEdgeGraph G u v).vertices, D.vertex w ∈ Metric.closedBall (D.vertex v) ρ → w = v) (a b : ℂ) (w : ℕ) (hw : w ∈ G.vertices) (hin : D.restoredVertex a b w ∈ Metric.closedBall (D.vertex v) ρ) : w = u ∨ w = v

Only the two restored source names can have their new points in the old closed replacement neighborhood. Unchanged declared isolates stay outside it.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.restoredVertex_injective {G : Graph} {u v : ℕ} {D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing} (hD : D.IsEmbedding) (huv : u ≠ v) {ρ : ℝ} (hpoints : ∀ w ∈ (RotationSystem.contractLastEdgeGraph G u v).vertices, D.vertex w ∈ Metric.closedBall (D.vertex v) ρ → w = v) {a b : ℂ} (ha : a ∈ Metric.ball (D.vertex v) ρ) (hb : b ∈ Metric.ball (D.vertex v) ρ) (hab : a ≠ b) : Set.InjOn (D.restoredVertex a b) {w : ℕ | w ∈ G.vertices}

The restored coordinates separate all original declared names, including isolates and repeated declarations. No enumeration of the ambient natural-number names is used.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.restoredRoute_vertex_contacts {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‖) (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) (i : Fin (D.restoredRoute ρ a b e).segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (w : ℕ) (hw : w ∈ G.vertices) (heq : (D.restoredRoute ρ a b e).eval i t = D.restoredVertex a b w) : ∃ (side : Bool), (D.restoredRoute ρ a b e).AtEnd i t side ∧ Dart.vertex (e, side) = w

A declared source vertex on a restored retained route occurs only at its own original end. This includes unused names and loops, with all real parameters checked.