Automatic local split layout from an actual contracted realization

Literal contraction block coordinates determine an open turn of actual germ angles, with the prescribed source insertion slot retained. No separator, drawing patch or geometric order provider is an input.

theorem Cslib.Complexity.Graph.PolygonalDrawing.Realizes.exists_contraction_angle_lift {G : Graph} {u v : ℕ} (r : (RotationSystem.lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) {D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing} (hR : D.Realizes (r.contractLastEdge huv)) : ∃ (cut : ℝ) (L : Real.Angle → ℝ), (∀ (d : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), L (D.direction ↑d) ∈ Set.Ioo cut (cut + 2 * Real.pi)) ∧ (∀ (φ : Real.Angle), ↑(L φ) = φ) ∧ ∀ (a b : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), L (D.direction ↑a) < L (D.direction ↑b) ↔ ↑(r.contractionRank b) < ↑(r.contractionRank a)

An arbitrary actual contracted realization supplies real angular representatives in the exact reverse order of the two literal source blocks. The cut lies in their specified insertion gap. The empty contracted star is included.

theorem Cslib.Complexity.Graph.PolygonalDrawing.Realizes.exists_contraction_split {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 < ρ) : ∃ a ∈ Metric.ball (D.vertex v) ρ, ∃ b ∈ Metric.ball (D.vertex v) ρ, ∃ (f : ℂ →ᵃ[ℝ] ℝ), f b < f a ∧ (∀ (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)) ∧ (∀ (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) ∧ (∀ (x y : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑x).vertex = u → (RotationSystem.contractionLift G u v ↑y).vertex = u → x ≠ y → (sbtw ↑(b - a).arg ↑(D.cutPort ρ ↑x - a).arg ↑(D.cutPort ρ ↑y - a).arg ↔ r.rotationDistance (RotationSystem.lastEdgeDart G u v false) (RotationSystem.contractionLift G u v ↑y) < r.rotationDistance (RotationSystem.lastEdgeDart G u v false) (RotationSystem.contractionLift G u v ↑x))) ∧ ∀ (x y : { d : (RotationSystem.contractLastEdgeGraph G u v).Dart // d.vertex = v }), (RotationSystem.contractionLift G u v ↑x).vertex = v → (RotationSystem.contractionLift G u v ↑y).vertex = v → x ≠ y → (sbtw ↑(a - b).arg ↑(D.cutPort ρ ↑x - b).arg ↑(D.cutPort ρ ↑y - b).arg ↔ r.rotationDistance (RotationSystem.lastEdgeDart G u v true) (RotationSystem.contractionLift G u v ↑y) < r.rotationDistance (RotationSystem.lastEdgeDart G u v true) (RotationSystem.contractionLift G u v ↑x))

An actual contracted embedding supplies its own two separated fans and connector in the exact source insertion slots. No geometric split data are premises. The cut circle may have any positive radius; a restriction radius is chosen separately.