Clockwise order of cut ports after moving their center

An interior fan to common-radius cut ports retains the exact clockwise order of the original drawing. Both ends of a loop and all indexed parallel occurrences remain distinct. The center can move anywhere in the open cut ball, without a semicircle restriction on the old ports. This does not construct a separator or restore a contracted edge.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.cutPort_sub_ne_zero {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) {x : ℂ} (hx : x ∈ Metric.ball (D.vertex v) ρ) (d : G.Dart) (hd : d.vertex = v) : D.cutPort ρ d - x ≠ 0

A new fan center strictly inside the cut circle differs from every boundary port.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.cutPort_direction_injective {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) {x : ℂ} (hx : x ∈ Metric.ball (D.vertex v) ρ) (a b : G.Dart) (ha : a.vertex = v) (hb : b.vertex = v) (heq : ↑(D.cutPort ρ a - x).arg = ↑(D.cutPort ρ b - x).arg) : a = b

Distinct retained darts still have distinct outgoing directions at any new interior fan center, including the two separate ends of an old loop.

theorem Cslib.Complexity.Graph.PolygonalDrawing.Realizes.cutPort_clockwise {G : Graph} {D : G.PolygonalDrawing} {r : G.RotationSystem} (hR : D.Realizes r) (hD : D.IsEmbedding) (v : ℕ) {ρ : ℝ} (hρ : 0 < ρ) {x : ℂ} (hx : x ∈ Metric.ball (D.vertex v) ρ) (a b c : G.Dart) (ha : a.vertex = v) (hb : b.vertex = v) (hc : c.vertex = v) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) : sbtw ↑(D.cutPort ρ c - x).arg ↑(D.cutPort ρ b - x).arg ↑(D.cutPort ρ a - x).arg ↔ b ∈ r.rotationInterval a c

Replacing a vertex by any interior fan center preserves the literal clockwise order of its retained port triples. Connector insertion and separation into two blocks require additional geometric work and are not asserted by this theorem.