Literal successor tables for a selected outgoing-corner swap

The raw list program is funded by the supplied table length, including malformed inputs. For the actual vertex-identification rotation it is exactly the generated successor table. Only the selected outgoing entries are exchanged; the internal order of both forward blocks is retained. These original identities make no genus claim for arbitrary selected corners.

def Cslib.Complexity.Graph.RotationCertificate.swapSuccessors (c : RotationCertificate) (h k : ℕ) : RotationCertificate

Exchange two outgoing entries in the supplied successor table. Every iteration is funded by the list length; missing selected indices use the ordinary raw-table fallback zero.

theorem Cslib.Complexity.Graph.RotationCertificate.length_swapSuccessors (c : RotationCertificate) (h k : ℕ) : (c.swapSuccessors h k).successor.length = c.successor.length

The raw outgoing swap retains the entire supplied table length, including zero.

theorem Cslib.Complexity.Graph.RotationCertificate.getD_swapSuccessors (c : RotationCertificate) (h k i : ℕ) (hi : i < c.successor.length) : (c.swapSuccessors h k).successor.getD i 0 = c.successor.getD (if i = h then k else if i = k then h else i) 0

Every actual retained position has its explicitly selected old successor. No validity premise is imposed on the input table or its binary entries.

theorem Cslib.Complexity.Graph.RotationSystem.ofRotation_mergeVertices {G : Graph} (r : G.RotationSystem) (h k : G.Dart) (hk : h.vertex ≠ k.vertex) : RotationCertificate.ofRotation (r.mergeVertices h k hk) = (RotationCertificate.ofRotation r).swapSuccessors h.index k.index

The constructed vertex-identification rotation encodes to exactly one outgoing-table swap. This is an equality of complete finite tables, not just their signatures or acceptance.