Components after joining two incident vertices

The actual endpoint update in mergeGraph joins precisely the two selected old components. All other edge components are unchanged. The correspondence is on actual indexed darts; it requires no connectedness, degree bound or injective vertex-name map.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_mergeGraph_iff_join {G : Graph} (h k : G.Dart) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (a b : G.Dart) : RotationCertificate.SameComponent (mergeGraph h k) ((mergeDartEquiv h k) a).vertex ((mergeDartEquiv h k) b).vertex ↔ RotationCertificate.SameComponent G a.vertex b.vertex ∨ RotationCertificate.SameComponent G a.vertex h.vertex ∧ RotationCertificate.SameComponent G k.vertex b.vertex ∨ RotationCertificate.SameComponent G a.vertex k.vertex ∧ RotationCertificate.SameComponent G h.vertex b.vertex

The literal vertex merge joins exactly the two selected components, and no others. The selected vertices may already belong to one component.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_mergeGraph_left_iff {G : Graph} (h k : G.Dart) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (b : G.Dart) : RotationCertificate.SameComponent (mergeGraph h k) ((mergeDartEquiv h k) h).vertex ((mergeDartEquiv h k) b).vertex ↔ RotationCertificate.SameComponent G h.vertex b.vertex ∨ RotationCertificate.SameComponent G k.vertex b.vertex

The component of the first merged corner is exactly the union of the two old ones.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_mergeGraph_unaffected_iff {G : Graph} (h k : G.Dart) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (a b : G.Dart) (ha : ¬RotationCertificate.SameComponent G a.vertex h.vertex) (hb : ¬RotationCertificate.SameComponent G a.vertex k.vertex) : RotationCertificate.SameComponent (mergeGraph h k) ((mergeDartEquiv h k) a).vertex ((mergeDartEquiv h k) b).vertex ↔ RotationCertificate.SameComponent G a.vertex b.vertex

Components disjoint from both selected corners retain precisely their old darts.