Joining different components preserves numerical genus zero

The literal mergeVertices successor swap joins two different old vertex components. Its vertex and face orbit counts each decrease by one in their union, and every indexed edge is retained. The argument counts all permutation orbits, including fixed points. Declared point components require no darts and retain their conventional Euler equation.

theorem Cslib.Complexity.Graph.RotationSystem.not_sameFace_of_not_sameComponent {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (h k : G.Dart) (hc : ¬RotationCertificate.SameComponent G h.vertex k.vertex) : ¬r.faceNext.SameCycle h k

Different actual edge components cannot share a face orbit.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_mergeVertices_of_not_sameComponent {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hr : r.NumericalGenusZero) (h k : G.Dart) (hk : h.vertex ≠ k.vertex) (hc : ¬RotationCertificate.SameComponent G h.vertex k.vertex) : (r.mergeVertices h k hk).NumericalGenusZero

Joining corners in different components preserves the existing componentwise numerical genus-zero predicate for the actual vertex merge. No target Euler or embedding premise is required. Unselected closed components and all declared points are retained.