Numerical genus of a disjoint listed union #
Every incident component has exactly its source vertex, edge and complete face counts. Genus zero follows componentwise from the two source rotations. Empty graphs, closed components and declared points are allowed, with no target-genus provider.
theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_disjointUnion {G H : Graph} (r : G.RotationSystem) (s : H.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hH : ∀ v ∈ H.incidenceVertices, v ∈ H.vertices) (hr : r.NumericalGenusZero) (hs : s.NumericalGenusZero) :
Disjoint union preserves source numerical genus zero component by component.