A cycle-space criterion for numerical genus zero

If every vertex-even Boolean edge label is the boundary of colors on the actual face quotient, the rotation is componentwise numerically genus zero. The proof applies the face-even lifting converse to the actual indexed dual and transports the edge labels back. It retains loops, parallel occurrences, disconnected components, sparse or duplicate vertex declarations, isolated points and the empty graph.

This is an original finite algebraic argument. The criterion is not a geometric converse: constructing these colors from a polygonal embedding is a separate obligation.

Main results

• Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_of_vertexEven_faceBoundary: the cycle-space criterion, with no genus assumption.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_of_vertexEven_faceBoundary {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hcolor : ∀ (x : Fin G.edges.length → Bool), G.VertexEven x → ∃ (q : r.Face → Bool), r.faceBoundary q = x) : r.NumericalGenusZero

Exactness of vertex-even labels as boundaries of actual face colors forces numerical genus zero. No connectedness, degree or nonloop assumption is needed. This algebraic criterion does not by itself construct colors from a geometric drawing.