Rotation transport across vertex declarations

Changing only the declared vertex list preserves indexed darts, rotations and every face. Equal declared membership preserves componentwise numerical genus zero: vertex counts use distinct declarations, and isolated-point components have the same roots. This applies to repeated declarations produced by arbitrary graph contraction as well as recognition queries.

def Cslib.Complexity.Graph.RotationSystem.redeclare {vertices : List ℕ} {edges : List (ℕ × ℕ)} (r : { vertices := vertices, edges := edges }.RotationSystem) (newVertices : List ℕ) : { vertices := newVertices, edges := edges }.RotationSystem

Keep every indexed edge end and successor while changing the vertex declaration list.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_redeclare {vertices newVertices : List ℕ} {edges : List (ℕ × ℕ)} (hm : ∀ (v : ℕ), v ∈ vertices ↔ v ∈ newVertices) (u v : ℕ) : RotationCertificate.SameComponent { vertices := vertices, edges := edges } u v ↔ RotationCertificate.SameComponent { vertices := newVertices, edges := edges } u v

Component membership depends on declared membership, not repeated declaration positions.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_redeclare_iff {vertices newVertices : List ℕ} {edges : List (ℕ × ℕ)} (hm : ∀ (v : ℕ), v ∈ vertices ↔ v ∈ newVertices) (r : { vertices := vertices, edges := edges }.RotationSystem) : (r.redeclare newVertices).NumericalGenusZero ↔ r.NumericalGenusZero

The numerical Euler predicate is invariant under reordering/repeating existing declared vertices. Every face orbit and listed edge occurrence remains unchanged.

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

Appending a duplicate declaration of an already declared vertex changes no numerical result.