Identifying two distinct incident vertices at specified corners

The second endpoint name is replaced by the first throughout the actual listed graph. The successor swap joins precisely the two old vertex cycles. Complete orbit counting proves the one-cycle-per-vertex contract, including singleton old vertex rotations. Edge positions and ends are unchanged; this is not a higher-arity constraint reflection.

def Cslib.Complexity.Graph.RotationSystem.mergeGraph {G : Graph} (h k : G.Dart) : Graph

Identify the second corner's vertex with the first, retaining all listed edge positions.

def Cslib.Complexity.Graph.RotationSystem.mergeDartEquiv {G : Graph} (h k : G.Dart) : G.Dart ≃ (mergeGraph h k).Dart

Merging vertex names retains the actual indexed edge/end occurrence.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.vertex_mergeDartEquiv {G : Graph} (h k d : G.Dart) : ((mergeDartEquiv h k) d).vertex = Function.update id k.vertex h.vertex d.vertex

Literal endpoint renaming at each retained indexed end.

def Cslib.Complexity.Graph.RotationSystem.mergeIncidentEquiv {G : Graph} (h k : G.Dart) (hk : h.vertex ≠ k.vertex) : { v : IncidentVertex G // ↑v ≠ k.vertex } ≃ IncidentVertex (mergeGraph h k)

The incident vertices after merging are exactly the old incident names except the removed second name. Declared points do not enter this dart-indexed correspondence.

theorem Cslib.Complexity.Graph.RotationSystem.card_incidentVertices_mergeGraph {G : Graph} (r : G.RotationSystem) (h k : G.Dart) (hk : h.vertex ≠ k.vertex) : Nat.card (IncidentVertex (mergeGraph h k)) + 1 = Nat.card (IncidentVertex G)

Exactly one nonempty vertex fiber is removed, including when either old fiber was unary.

def Cslib.Complexity.Graph.RotationSystem.mergeVertices {G : Graph} (r : G.RotationSystem) (h k : G.Dart) (hk : h.vertex ≠ k.vertex) : (mergeGraph h k).RotationSystem

Join the two distinct vertex fibers at the specified oriented corners. Its successor is computed by one outgoing swap, and all orbit/vertex facts are proved from that permutation.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.mergeDartEquiv_reverse {G : Graph} (h k d : G.Dart) : (mergeDartEquiv h k) d.reverse = ((mergeDartEquiv h k) d).reverse

Vertex identification preserves the original indexed edge reversal.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.rotate_mergeVertices {G : Graph} (r : G.RotationSystem) (h k : G.Dart) (hk : h.vertex ≠ k.vertex) : (r.mergeVertices h k hk).rotate = (mergeDartEquiv h k).permCongr (r.rotate * Equiv.swap h k)

Literal successor permutation of the constructed vertex identification.

theorem Cslib.Complexity.Graph.RotationSystem.rotate_mergeVertices_left {G : Graph} (r : G.RotationSystem) (h k : G.Dart) (hk : h.vertex ≠ k.vertex) : (r.mergeVertices h k hk).rotate ((mergeDartEquiv h k) h) = (mergeDartEquiv h k) (r.rotate k)

The first chosen corner continues with the second old forward block.

theorem Cslib.Complexity.Graph.RotationSystem.rotate_mergeVertices_right {G : Graph} (r : G.RotationSystem) (h k : G.Dart) (hk : h.vertex ≠ k.vertex) : (r.mergeVertices h k hk).rotate ((mergeDartEquiv h k) k) = (mergeDartEquiv h k) (r.rotate h)

The second chosen corner continues with the first old forward block.

theorem Cslib.Complexity.Graph.RotationSystem.rotate_mergeVertices_other {G : Graph} (r : G.RotationSystem) (h k d : G.Dart) (hk : h.vertex ≠ k.vertex) (hd : d ≠ h) (he : d ≠ k) : (r.mergeVertices h k hk).rotate ((mergeDartEquiv h k) d) = (mergeDartEquiv h k) (r.rotate d)

Every successor outside the two chosen corners is literally retained.