2.16. Indexed Rotation Surgery🔗

The ordinary imports above expose actual indexed rotation operations in Cslib.Complexity.Graph.RotationSystem. Inserting an edge at two cofacial dart corners preserves componentwise numerical genus zero, even when the corners or their vertices coincide:

open Cslib.Complexity in
example {G : Graph} (r : Graph.RotationSystem G)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.1) (hr : r.NumericalGenusZero)
    (h k : Graph.Dart G) (hf : r.faceNext.SameCycle h k) :
    (r.insertEdge h k).NumericalGenusZero :=
  r.numericalGenusZero_insertEdge hG hr h k hf

VertexMergeGenus also identifies distinct cofacial vertices, preserving the directed port blocks and retaining listed edge positions. Its cofacial hypothesis is essential to that theorem. The separate VertexJoinGenus theorem handles different actual components:

open Cslib.Complexity Graph.RotationSystem in
example {G : Graph} (r : Graph.RotationSystem G)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.1)
    (hr : r.NumericalGenusZero) (h k : Graph.Dart G)
    (hk : h.vertex ≠ k.vertex)
    (hc : ¬Graph.RotationCertificate.SameComponent
      G h.vertex k.vertex) :
    (r.mergeVertices h k hk).NumericalGenusZero :=
  r.numericalGenusZero_mergeVertices_of_not_sameComponent hG hr h k hk hc

Disjoint union tags names by parity and concatenates actual declaration and edge lists. Loops, indexed duplicates, sparse names and points remain:

open Cslib.Complexity Graph.RotationSystem in
example {G H : Graph} (r : Graph.RotationSystem G)
    (s : Graph.RotationSystem H)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.1)
    (hH : ∀ v ∈ H.incidenceVertices, v ∈ H.1)
    (hr : r.NumericalGenusZero) (hs : s.NumericalGenusZero) :
    (r.disjointUnion s).NumericalGenusZero :=
  numericalGenusZero_disjointUnion r s hG hH hr hs

Arbitrary edge deletion uses an internally proved face-even extension instead, including splitting bridges, loops and new isolated points:

open Cslib.Complexity Graph.RotationSystem in
example {G : Graph} {u v : ℕ}
    (r : Graph.RotationSystem (lastEdgeGraph G u v))
    (hH : ∀ w ∈ (lastEdgeGraph G u v).incidenceVertices,
      w ∈ (lastEdgeGraph G u v).1) (hr : r.NumericalGenusZero) :
    r.deleteLastEdge.NumericalGenusZero :=
  r.numericalGenusZero_deleteLastEdge hH hr

Contracting an actual nonloop edge needs neither a bridge nor cofaciality nor connectedness. It removes the last edge, splices the directed blocks without reflection, and updates every remaining endpoint named u to v:

open Cslib.Complexity Graph.RotationSystem in
example {G : Graph} {u v : ℕ}
    (r : Graph.RotationSystem (lastEdgeGraph G u v)) (huv : u ≠ v)
    (hH : ∀ w ∈ (lastEdgeGraph G u v).incidenceVertices,
      w ∈ (lastEdgeGraph G u v).1) (hr : r.NumericalGenusZero) :
    (r.contractLastEdge huv).NumericalGenusZero :=
  r.numericalGenusZero_contractLastEdge huv hH hr

The target is exactly G.relabel (Function.update id u v), including its mapped declaration list. Repeated declarations can then be removed while retaining every edge, dart and rotation successor:

open Cslib.Complexity Graph.RotationSystem in
example {vertices : List ℕ} {edges : List (ℕ × ℕ)} {v : ℕ}
    (hv : v ∈ vertices)
    (r : Graph.RotationSystem ⟨vertices ++ [v], edges⟩) :
    (redeclare r vertices).NumericalGenusZero ↔ r.NumericalGenusZero :=
  numericalGenusZero_append_duplicate_iff hv r

The complete regression clients are RotationCornerFaces, VertexIdentification, RotationDeletionComponents, RotationContraction and RotationLiftingConverse under CslibFrontierTests/. They check actual tables and numerical certificates, nonbridge and empty-block cases, and reflected-order rejection. The proofs are original finite permutation and algebraic arguments. Static grammar closure is supplied below; these graph operations assert no native runtime, geometric realization, recognition or Hanani–Tutte theorem.

For permutation-only proofs, import CslibFrontier.Foundations.GroupTheory.Perm.InsertAfter, CycleSurgery or SelectedOrbits. The APIs live in Equiv.Perm.Insertion, Equiv.Perm.CycleSurgery and Equiv.Perm.SelectedOrbits, with no graph dependency. CslibFrontierTests/PermutationSurgery.lean is a complete standalone client.