Deleting the last indexed edge of a rotation

The two ends of the last listed edge are removed from their actual vertex cycles, retaining the direction of every remaining successor. Vertex declarations are retained, including endpoints that become isolated points. The face successor is obtained by swapping the two deleted ends in the old face permutation and then deleting both ends. No connectedness or genus assertion is part of the constructor.

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

The actual graph before deleting its last edge; no corner darts are required at points.

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

Old darts and the last two ends, in their original edge/end positions.

def Cslib.Complexity.Graph.RotationSystem.lastEdgeDart (G : Graph) (u v : ℕ) (b : Bool) : (lastEdgeGraph G u v).Dart

The two indexed ends of the last listed edge, including when the old graph has no darts.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.vertex_lastEdgeDart (G : Graph) (u v : ℕ) (b : Bool) : (lastEdgeDart G u v b).vertex = if b = true then v else u

The last two actual endpoints are exactly the supplied names.

theorem Cslib.Complexity.Graph.RotationSystem.reverse_lastEdgeDart (G : Graph) (u v : ℕ) (b : Bool) : (lastEdgeDart G u v b).reverse = lastEdgeDart G u v !b

Reversal interchanges the two last indexed ends.

def Cslib.Complexity.Graph.RotationSystem.retainedLastEdgeDart (G : Graph) (u v : ℕ) (d : G.Dart) : (lastEdgeGraph G u v).Dart

Retain an old dart, without changing its edge-list index or end.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.vertex_retainedLastEdgeDart (G : Graph) (u v : ℕ) (d : G.Dart) : (retainedLastEdgeDart G u v d).vertex = d.vertex

Retained indexed ends keep their original endpoint names.

def Cslib.Complexity.Graph.RotationSystem.deleteLastEdge {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) : G.RotationSystem

Delete the last two indexed ends from their vertex cycles. The construction works when either endpoint becomes isolated and when there are no remaining edges.

theorem Cslib.Complexity.Graph.RotationSystem.lastEdgeDartEquiv_reversal (G : Graph) (u v : ℕ) : (lastEdgeDartEquiv G u v).permCongr (Dart.reversal (lastEdgeGraph G u v)) = (Equiv.optionCongr (Dart.reversal G)).optionCongr * Equiv.swap (some none) none

Exact reversal in the retained-plus-two-deleted coordinates.

theorem Cslib.Complexity.Graph.RotationSystem.faceNext_deleteLastEdge {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) : r.deleteLastEdge.faceNext = ((lastEdgeDartEquiv G u v).permCongr r.faceNext * Equiv.swap (some none) none).removeNone.removeNone

Deletion splices face successors with the original chirality. The preliminary outgoing swap cancels reversal on the two deleted ends; it is essential even for a loop.

theorem Cslib.Complexity.Graph.RotationSystem.card_faces_deleteLastEdge_balance {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) : Nat.card r.deleteLastEdge.Face + Nat.card (Quotient (Equiv.Perm.SameCycle.setoid r.rotate)) = Nat.card (Quotient (Equiv.Perm.SameCycle.setoid ((lastEdgeDartEquiv G u v).permCongr r.faceNext * Equiv.swap (some none) none))) + Nat.card (Quotient (Equiv.Perm.SameCycle.setoid r.deleteLastEdge.rotate))

Exact accounting for faces lost at endpoints that become isolated. The old vertex orbit count exceeds the retained one by precisely the number of deleted singleton cycles in the preliminary face swap. This identity includes deletion of the only edge or loop.