Contacts between distinct restored edge occurrences #
Exterior pieces inherit their old contacts away from the split vertex. New spokes meet only at their assigned source centers, and the connector meets them only at its corresponding original ends. All statements quantify over real segment parameters.
theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.restoredRoute_edge_contacts {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‖) (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 g : Fin G.edges.length) (heg : e ≠ g) (i : Fin (D.restoredRoute ρ a b e).segments) (j : Fin (D.restoredRoute ρ a b g).segments) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (heq : (D.restoredRoute ρ a b e).eval i s = (D.restoredRoute ρ a b g).eval j t) :
∃ (side : Bool) (tag : Bool),
(D.restoredRoute ρ a b e).AtEnd i s side ∧ (D.restoredRoute ρ a b g).AtEnd j t tag ∧ Dart.vertex (e, side) = Dart.vertex (g, tag)
Distinct retained restored edges meet only at their original common ends. The two occurrences of a contracted loop remain independent throughout.
theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.restoredRoute_connector_contacts {G : Graph} {u v : ℕ} {D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing} (hD : D.IsEmbedding) (huv : u ≠ v) {ρ : ℝ} (hρ : 0 < ρ) (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) (j : Fin (Polygonal.Route.line a b).segments) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (heq : (D.restoredRoute ρ a b e).eval i s = (Polygonal.Route.line a b).eval j t) :
The selected connector meets a retained restored edge only at its corresponding original endpoint. It never touches the unchanged exterior pieces.
theorem Cslib.Complexity.Graph.PolygonalDrawing.connector_vertex_contacts {G : Graph} {u v : ℕ} (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (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) (i : Fin (Polygonal.Route.line a b).segments) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (w : ℕ) (hw : w ∈ G.vertices) (heq : (Polygonal.Route.line a b).eval i t = D.restoredVertex a b w) :
A declared point on the new connector is exactly one of its original named ends.