Directed contraction of an indexed nonloop edge

The last edge's first endpoint is identified with its second endpoint. The two vertex cycles are spliced at the actual edge ends and those ends are then removed. This retains the direction of the two remaining cyclic blocks, even if one block is empty, and redirects every other loop or parallel edge positionally. No bridge or cofacial hypothesis is used. These are original permutation constructions on the existing listed graph model.

def Cslib.Complexity.Graph.RotationSystem.contractLastEdgeGraph (G : Graph) (u v : ℕ) : Graph

Remove the last edge and replace its first endpoint's name by its second throughout the retained graph. Declared points and repeated edge occurrences are retained.

theorem Cslib.Complexity.Graph.RotationSystem.mergeGraph_lastEdgeDart (G : Graph) (u v : ℕ) : mergeGraph (lastEdgeDart G u v true) (lastEdgeDart G u v false) = lastEdgeGraph (contractLastEdgeGraph G u v) v v

The intermediate corner splice turns the selected edge into a loop at the retained endpoint. This is literal equality of the listed graphs, including all declared points.

def Cslib.Complexity.Graph.RotationSystem.contractLastEdgeSplice {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) : (lastEdgeGraph (contractLastEdgeGraph G u v) v v).RotationSystem

Reinterpret the actual corner splice as a graph with one final loop. No numerical genus premise is imposed on this intermediate rotation.

def Cslib.Complexity.Graph.RotationSystem.contractLastEdge {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) : (contractLastEdgeGraph G u v).RotationSystem

Contract an actual nonloop edge by directed vertex splicing followed by removal of its two ends. The construction applies to arbitrary nonloop edges, including nonbridges.

def Cslib.Complexity.Graph.RotationSystem.contractLastEdgeDartEquiv (G : Graph) (u v : ℕ) : (lastEdgeGraph G u v).Dart ≃ (lastEdgeGraph (contractLastEdgeGraph G u v) v v).Dart

Old edge ends retain their original index and end tag during the preliminary splice.

theorem Cslib.Complexity.Graph.RotationSystem.rotate_contractLastEdgeSplice {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) : (r.contractLastEdgeSplice huv).rotate = (contractLastEdgeDartEquiv G u v).permCongr (r.rotate * Equiv.swap (lastEdgeDart G u v true) (lastEdgeDart G u v false))

Literal successor of the preliminary splice: the outgoing successors of the two selected ends are exchanged, with no reversal of either remaining block.

theorem Cslib.Complexity.Graph.RotationSystem.rotate_contractLastEdge {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) : (r.contractLastEdge huv).rotate = (Equiv.removeNone (((contractLastEdgeDartEquiv G u v).trans (lastEdgeDartEquiv (contractLastEdgeGraph G u v) v v)).permCongr (r.rotate * Equiv.swap (lastEdgeDart G u v true) (lastEdgeDart G u v false)))).removeNone

Literal retained rotation after directed nonloop contraction.

theorem Cslib.Complexity.Graph.RotationSystem.vertex_contractLastEdgeDartEquiv (G : Graph) (u v : ℕ) (d : (lastEdgeGraph G u v).Dart) : ((contractLastEdgeDartEquiv G u v) d).vertex = Function.update id u v d.vertex

The splice changes exactly the selected endpoint name at each actual dart.

theorem Cslib.Complexity.Graph.RotationSystem.reverse_contractLastEdgeDartEquiv (G : Graph) (u v : ℕ) (d : (lastEdgeGraph G u v).Dart) : (contractLastEdgeDartEquiv G u v) d.reverse = ((contractLastEdgeDartEquiv G u v) d).reverse

The preliminary splice retains the original edge reversal.

theorem Cslib.Complexity.Graph.RotationSystem.contractLastEdge_coordinates (G : Graph) (u v : ℕ) : (contractLastEdgeDartEquiv G u v).trans (lastEdgeDartEquiv (contractLastEdgeGraph G u v) v v) = (lastEdgeDartEquiv G u v).trans (Dart.relabelEquiv G (Function.update id u v)).optionCongr.optionCongr

The retained and removed coordinates are literal: old edge/end positions map pointwise, and the two deleted ends keep their tags.

theorem Cslib.Complexity.Graph.RotationSystem.faceNext_contractLastEdgeSplice {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) : (r.contractLastEdgeSplice huv).faceNext = (contractLastEdgeDartEquiv G u v).permCongr (Equiv.swap (lastEdgeDart G u v true) (lastEdgeDart G u v false) * r.faceNext)

The face successor after the preliminary vertex splice has one incoming swap.

theorem Cslib.Complexity.Graph.RotationSystem.contractLastEdge_coordinates_last (G : Graph) (u v : ℕ) (b : Bool) : ((contractLastEdgeDartEquiv G u v).trans (lastEdgeDartEquiv (contractLastEdgeGraph G u v) v v)) (lastEdgeDart G u v b) = if b = true then none else some none

In retained-plus-two-removed coordinates the selected ends remain the two removed points, including when the retained graph has no darts.

theorem Cslib.Complexity.Graph.RotationSystem.faceNext_contractLastEdge {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) : (r.contractLastEdge huv).faceNext = (Equiv.swap (some none) none * ((contractLastEdgeDartEquiv G u v).trans (lastEdgeDartEquiv (contractLastEdgeGraph G u v) v v)).permCongr r.faceNext * Equiv.swap (some none) none).removeNone.removeNone

Exact face successor of nonloop contraction. The incoming and outgoing swaps conjugate the original face permutation at the two removed ends before deleting them. Both swaps are derived from the actual directed splice, rather than assumed face counts.