Face cycles of insertion at specified corners

These original permutation identities count all face cycles, including singleton faces. Inserting an edge between two corners on the same face increases the face count by one; insertion between different faces decreases it by one. Cofaciality is essential, even when both corners belong to the same vertex. Coincident corners are treated explicitly.

theorem Cslib.Complexity.Graph.RotationSystem.cornerDartEquiv_reverse {G : Graph} (h k : G.Dart) (d : (cornerGraph h k).Dart) : (cornerDartEquiv h k) d.reverse = ((Equiv.optionCongr (Dart.reversal G)).optionCongr * Equiv.swap (some none) none) ((cornerDartEquiv h k) d)

Appending an indexed edge preserves reversal on old ends and interchanges exactly the new two ends. The equation uses the same edge/end coordinates as insertEdge.

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

The actual generated rotation in the old-plus-two-new-darts coordinates.

theorem Cslib.Complexity.Graph.RotationSystem.cornerDartEquiv_reversal {G : Graph} (h k : G.Dart) : (cornerDartEquiv h k).permCongr (Dart.reversal (cornerGraph h k)) = (Equiv.optionCongr (Dart.reversal G)).optionCongr * Equiv.swap (some none) none

Exact reversal conjugacy for the appended listed edge.

theorem Cslib.Complexity.Graph.RotationSystem.faceNext_insertEdge {G : Graph} (r : G.RotationSystem) (h k : G.Dart) : (cornerDartEquiv h k).permCongr (r.insertEdge h k).faceNext = Equiv.Perm.CycleSurgery.splice r.faceNext h k

Exact conjugacy of the generated face permutation, with the original chirality. No same-face or same-vertex hypothesis is used in this successor identity.

theorem Cslib.Complexity.Graph.RotationSystem.card_faces_insertEdge_cofacial {G : Graph} (r : G.RotationSystem) (h k : G.Dart) (hc : r.faceNext.SameCycle h k) : Nat.card (r.insertEdge h k).Face = Nat.card r.Face + 1

Inserting an edge at cofacial existing dart corners adds exactly one face, including when the selected corners are identical.

theorem Cslib.Complexity.Graph.RotationSystem.card_faces_insertEdge_different_faces {G : Graph} (r : G.RotationSystem) (h k : G.Dart) (hc : ¬r.faceNext.SameCycle h k) : Nat.card (r.insertEdge h k).Face + 1 = Nat.card r.Face

Inserting between different face cycles merges them. This includes joining components; in one component it is the count responsible for increasing the numerical genus.