Automatic restoration of an arbitrary contracted polygonal embedding #
The cut radius, finite circle gaps, split centers, straight fans and connector are constructed internally from the actual contracted drawing and its literal rotation.
Main results #
Cslib.Complexity.Graph.PolygonalDrawing.Realizes.exists_restoration: automatically restore any actual contracted realization, including its exact clockwise order.
theorem Cslib.Complexity.Graph.PolygonalDrawing.Realizes.exists_restoration {G : Graph} {u v : ℕ} (r : (RotationSystem.lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (hG : ∀ w ∈ (RotationSystem.lastEdgeGraph G u v).incidenceVertices, w ∈ G.vertices) {D : (RotationSystem.contractLastEdgeGraph G u v).PolygonalDrawing} (hD : D.IsEmbedding) (hR : D.Realizes (r.contractLastEdge huv)) :
∃ ρ > 0, ∃ (a : ℂ) (b : ℂ), (D.restoration huv ρ a b).IsEmbedding ∧ (D.restoration huv ρ a b).Realizes r
Restore an actual arbitrary contracted drawing as a source embedding, choosing all local geometric data internally, including the exact literal clockwise source rotation.