Polygonal drawings of arbitrary bouquets of indexed loops

Every vertex receives a translated copy of the five-segment port-loop construction, with ports in the literal clockwise rotation order. A common horizontal spacing separates all natural-number vertex names, including sparse and repeated declarations and isolated names. Each listed edge occurrence retains both of its own ends. The coordinate construction is an original reconstruction and has no degree or component bound.

noncomputable def Cslib.Complexity.Graph.PolygonalDrawing.bouquet {G : Graph} (r : G.RotationSystem) (hloop : ∀ (e : Fin G.edges.length), Dart.vertex (e, false) = Dart.vertex (e, true)) : G.PolygonalDrawing

Explicit five-segment routes for any loop-only graph and any supplied rotation. Each vertex cycle is cut once and its darts placed at positive horizontal ports in rank order. Numerical genus zero is needed for embedding, not to define these actual coordinates.

theorem Cslib.Complexity.Graph.PolygonalDrawing.germ_bouquet {G : Graph} (r : G.RotationSystem) (hloop : ∀ (e : Fin G.edges.length), Dart.vertex (e, false) = Dart.vertex (e, true)) (d : G.Dart) : (bouquet r hloop).germ d = { re := ↑(r.portRank d) + 1, im := 1 }

The two actual loop-end germs are the ports of those very indexed darts.

theorem Cslib.Complexity.Graph.PolygonalDrawing.bouquet_realizes {G : Graph} (r : G.RotationSystem) (hloop : ∀ (e : Fin G.edges.length), Dart.vertex (e, false) = Dart.vertex (e, true)) : (bouquet r hloop).Realizes r

The construction realizes the exact given clockwise rotation, without reflection. This needs no numerical-genus assumption; bouquet_isEmbedding supplies embedding separately.

theorem Cslib.Complexity.Graph.PolygonalDrawing.bouquet_isEmbedding {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)) : (bouquet r hloop).IsEmbedding

For every loop-only listed graph, numerical genus zero makes the constructed five-segment drawing a genuine embedding. Degrees, repeated edge pairs, declared vertex names, isolated vertices and disconnected components are unrestricted.