Indexed edge insertion at two dart corners

A new edge is appended to the actual listed graph. Its two ends are inserted immediately after the two specified old darts. Corners may coincide, and their vertices may coincide: loops and repeated boundary visits do not identify dart occurrences. The result proves the full vertex-fiber rotation contract and gives literal successor equations. Numerical genus requires an additional face-location argument; arbitrary corner insertion need not preserve it.

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

Append a structural edge between the vertices of two chosen dart corners.

def Cslib.Complexity.Graph.RotationSystem.appendedDartEquiv (n : ℕ) : Fin (n + 1) × Bool ≃ Option (Option (Fin n × Bool))

Appending an edge adds exactly two indexed ends to the old dart type.

def Cslib.Complexity.Graph.RotationSystem.cornerDartEquiv {G : Graph} (h k : G.Dart) : (cornerGraph h k).Dart ≃ Option (Option G.Dart)

Target edge/end positions are the old darts plus two distinct new ends.

def Cslib.Complexity.Graph.RotationSystem.oldCornerDart {G : Graph} (h k d : G.Dart) : (cornerGraph h k).Dart

The old edge/end occurrence in the appended graph.

def Cslib.Complexity.Graph.RotationSystem.newCornerDart {G : Graph} (h k : G.Dart) (b : Bool) : (cornerGraph h k).Dart

The first (false) and second (true) ends of the appended edge.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.vertex_oldCornerDart {G : Graph} (h k d : G.Dart) : (oldCornerDart h k d).vertex = d.vertex

Old vertices are unchanged by appending the edge.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.vertex_newCornerDart {G : Graph} (h k : G.Dart) (b : Bool) : (newCornerDart h k b).vertex = if b = true then k.vertex else h.vertex

The inserted ends have exactly their selected corner vertices.

def Cslib.Complexity.Graph.RotationSystem.insertEdge {G : Graph} (r : G.RotationSystem) (h k : G.Dart) : (cornerGraph h k).RotationSystem

Insert both new edge ends at the specified old corners. If h=k, their cyclic order is h, new true, new false, old successor; the ends of a loop remain distinct.

theorem Cslib.Complexity.Graph.RotationSystem.rotate_insertEdge_new_true {G : Graph} (r : G.RotationSystem) (h k : G.Dart) : (cornerDartEquiv h k) ((r.insertEdge h k).rotate (newCornerDart h k true)) = some ((Equiv.Perm.Insertion.insertAfter r.rotate h) (some k))

The second new end is followed by the first insertion's old successor at k.

theorem Cslib.Complexity.Graph.RotationSystem.rotate_insertEdge_at_left {G : Graph} (r : G.RotationSystem) (h k : G.Dart) (hk : h ≠ k) : (r.insertEdge h k).rotate (oldCornerDart h k h) = newCornerDart h k false

When the corners differ, the first selected corner leads to the first new end.

theorem Cslib.Complexity.Graph.RotationSystem.rotate_insertEdge_at_right {G : Graph} (r : G.RotationSystem) (h k : G.Dart) : (r.insertEdge h k).rotate (oldCornerDart h k k) = newCornerDart h k true

The second selected corner always leads to the second new end.