Right-side colors of an embedded polygonal drawing

The construction uses one internally chosen ray direction, actual segment endpoints, and angular prefix sums. Segment interiors transport colors, the two bend germs transport them through each bend, and literal clockwise realization identifies the empty vertex sectors.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.exists_faceColors {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) {r : G.RotationSystem} (hR : D.Realizes r) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (x : Fin G.edges.length → Bool) (hx : G.VertexEven x) : ∃ (q : r.Face → Bool), r.faceBoundary q = x

Every vertex-even indexed edge label of an actual polygonal embedding is the boundary of colors on the actual face quotient of the literally realized clockwise rotation. The multiplier and all side transport are constructed internally from the finite real-affine segments. No genus or topological separation hypothesis is used.