Exact clockwise order after actual nonloop restoration

Retained triples preserve literal cyclic order inside either source block. The selected connector occupies its prescribed source insertion slot, including empty-tail cases.

theorem Cslib.Complexity.Graph.PolygonalDrawing.Realizes.clockwise_restoration_retained {G : Graph} {u v : ℕ} (r : (RotationSystem.lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) {D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing} (hD : D.IsEmbedding) (hR : D.Realizes (r.contractLastEdge huv)) {ρ : ℝ} (hρ : 0 < ρ) (hlen : ∀ (d : (RotationSystem.contractLastEdgeGraph G u v).Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) {a b : ℂ} (ha : a ∈ Metric.ball (D.vertex v) ρ) (hb : b ∈ Metric.ball (D.vertex v) ρ) (x y z : (RotationSystem.contractLastEdgeGraph G u v).Dart) (hxy : (RotationSystem.contractionLift G u v x).vertex = (RotationSystem.contractionLift G u v y).vertex) (hyz : (RotationSystem.contractionLift G u v y).vertex = (RotationSystem.contractionLift G u v z).vertex) (hneXY : x ≠ y) (hneYZ : y ≠ z) (hneXZ : x ≠ z) : sbtw ((D.restoration huv ρ a b).direction (RotationSystem.contractionLift G u v z)) ((D.restoration huv ρ a b).direction (RotationSystem.contractionLift G u v y)) ((D.restoration huv ρ a b).direction (RotationSystem.contractionLift G u v x)) ↔ RotationSystem.contractionLift G u v y ∈ r.rotationInterval (RotationSystem.contractionLift G u v x) (RotationSystem.contractionLift G u v z)

Retained triples preserve the exact source clockwise order at every vertex.

theorem Cslib.Complexity.Graph.PolygonalDrawing.clockwise_restoration_selected {G : Graph} {u v : ℕ} (r : (RotationSystem.lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing) (ρ : ℝ) (a b : ℂ) (horder : ∀ (side : Bool) (x y : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑x).vertex = (RotationSystem.lastEdgeDart G u v side).vertex → (RotationSystem.contractionLift G u v ↑y).vertex = (RotationSystem.lastEdgeDart G u v side).vertex → x ≠ y → (sbtw ↑(if side = true then a - b else b - a).arg ↑(D.cutPort ρ ↑x - if side = true then b else a).arg ↑(D.cutPort ρ ↑y - if side = true then b else a).arg ↔ r.rotationDistance (RotationSystem.lastEdgeDart G u v side) (RotationSystem.contractionLift G u v ↑y) < r.rotationDistance (RotationSystem.lastEdgeDart G u v side) (RotationSystem.contractionLift G u v ↑x))) (side : Bool) (y z : (RotationSystem.contractLastEdgeGraph G u v).Dart) (hy : (RotationSystem.contractionLift G u v y).vertex = (RotationSystem.lastEdgeDart G u v side).vertex) (hz : (RotationSystem.contractionLift G u v z).vertex = (RotationSystem.lastEdgeDart G u v side).vertex) (hyz : y ≠ z) : sbtw ((D.restoration huv ρ a b).direction (RotationSystem.contractionLift G u v z)) ((D.restoration huv ρ a b).direction (RotationSystem.contractionLift G u v y)) ((D.restoration huv ρ a b).direction (RotationSystem.lastEdgeDart G u v side)) ↔ RotationSystem.contractionLift G u v y ∈ r.rotationInterval (RotationSystem.lastEdgeDart G u v side) (RotationSystem.contractionLift G u v z)

The selected connector occupies its exact original insertion slot. The retained pair order is the internally constructed complementary fan gap, in either orientation.

theorem Cslib.Complexity.Graph.PolygonalDrawing.Realizes.restoration {G : Graph} {u v : ℕ} (r : (RotationSystem.lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) {D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing} (hD : D.IsEmbedding) (hR : D.Realizes (r.contractLastEdge huv)) {ρ : ℝ} (hρ : 0 < ρ) (hlen : ∀ (d : (RotationSystem.contractLastEdgeGraph G u v).Dart), d.vertex = v → 3 * ρ < ‖D.germ d‖) {a b : ℂ} (ha : a ∈ Metric.ball (D.vertex v) ρ) (hb : b ∈ Metric.ball (D.vertex v) ρ) (hnew : (D.restoration huv ρ a b).IsEmbedding) (horder : ∀ (side : Bool) (x y : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑x).vertex = (RotationSystem.lastEdgeDart G u v side).vertex → (RotationSystem.contractionLift G u v ↑y).vertex = (RotationSystem.lastEdgeDart G u v side).vertex → x ≠ y → (sbtw ↑(if side = true then a - b else b - a).arg ↑(D.cutPort ρ ↑x - if side = true then b else a).arg ↑(D.cutPort ρ ↑y - if side = true then b else a).arg ↔ r.rotationDistance (RotationSystem.lastEdgeDart G u v side) (RotationSystem.contractionLift G u v ↑y) < r.rotationDistance (RotationSystem.lastEdgeDart G u v side) (RotationSystem.contractionLift G u v ↑x))) : (D.restoration huv ρ a b).Realizes r

The actual restored drawing realizes the exact source rotation when its internally constructed connector has the prescribed complementary gap order.