Polygonal realization of arbitrary numerical genus-zero rotations

Induction on the actual listed edge count contracts any nonloop occurrence after an indexed permutation. Automatic geometric restoration reopens every retained edge end independently and inserts the selected connector in its literal clockwise slot. Transport back recovers the exact original edge order and declarations. The loop-only base includes empty graphs, isolated declared names, loops, parallel occurrences and disconnected graphs.

This is a forward existence theorem for actual finite polygonal embeddings over the real plane. It asserts neither a coordinate-bit bound nor a planarity recognition algorithm.

Main results

• Cslib.Complexity.Graph.RotationSystem.exists_polygonalDrawing: every declared numerical genus-zero rotation has an actual clockwise polygonal embedding.

theorem Cslib.Complexity.Graph.RotationSystem.exists_polygonalDrawing {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hr : r.NumericalGenusZero) : ∃ (D : G.PolygonalDrawing), D.IsEmbedding ∧ D.Realizes r

Every supplied componentwise numerical genus-zero rotation on an arbitrary actual listed finite graph has a genuine polygonal embedding realizing its exact clockwise order. No geometric patch, separator, drawing or order provider is an additional premise.