Clockwise polygonal realization of loop-only genus-zero rotations

For any finite listed graph whose edges are all loops, declared endpoints and componentwise numerical genus zero suffice to construct an actual polygonal embedding realizing the exact given clockwise rotation. The construction uses first-hit ranks and internally derived nonalternation. There is no matching, drawing, disk, topological or geometric provider premise.

Vertex declarations may repeat, be sparse, or include disconnected isolated names; edges may repeat the same pair of endpoint names arbitrarily often. The empty graph is included. Each indexed loop has five actual real affine segments. No degree, coordinate-bit or connectedness bound is assumed or claimed. This is an original coordinate construction.

This proves only the forward realization for loop-only graphs. It does not restore nonloop edges after contraction or prove the geometric-to-numerical converse.

Main results

• Cslib.Complexity.Graph.RotationSystem.exists_polygonalDrawing_of_loops: loop-only realization.

theorem Cslib.Complexity.Graph.RotationSystem.exists_polygonalDrawing_of_loops {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hr : r.NumericalGenusZero) (hloop : ∀ (e : Fin G.edges.length), Dart.vertex (e, false) = Dart.vertex (e, true)) : ∃ (D : G.PolygonalDrawing), D.IsEmbedding ∧ D.Realizes r

Every loop-only numerical-genus-zero rotation has a genuine polygonal embedding with its exact clockwise germ order. All listed occurrences and both ends of every loop are retained, without any noncrossing or geometric hypothesis.