Vertex-name maps on actual listed graph darts

All declared names and edge endpoints are mapped pointwise. Edge positions and end tags remain unchanged, even for a noninjective map. This supplies endpoint equations for vertex identification and nonloop contraction; arbitrary renaming alone does not supply a rotation or preserve numerical genus. Isolated declarations remain in the mapped vertex list.

def Cslib.Complexity.Graph.relabel (G : Graph) (f : ℕ → ℕ) : Graph

Map the actual declared names and both endpoints of every listed edge occurrence.

theorem Cslib.Complexity.Graph.endpoints_declared_relabel (G : Graph) (f : ℕ → ℕ) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (v : ℕ) : v ∈ (G.relabel f).incidenceVertices → v ∈ (G.relabel f).vertices

Mapping all declared names and edge endpoints retains endpoint declaration, without an injectivity assumption on the map.

def Cslib.Complexity.Graph.Dart.relabelEquiv (G : Graph) (f : ℕ → ℕ) : G.Dart ≃ (G.relabel f).Dart

A vertex-name map retains every original indexed edge end. No injection is required.

theorem Cslib.Complexity.Graph.Dart.vertex_relabelEquiv (G : Graph) (f : ℕ → ℕ) (d : G.Dart) : ((relabelEquiv G f) d).vertex = f d.vertex

The actual endpoint is mapped by the supplied name function.

theorem Cslib.Complexity.Graph.Dart.reverse_relabelEquiv (G : Graph) (f : ℕ → ℕ) (d : G.Dart) : (relabelEquiv G f) d.reverse = ((relabelEquiv G f) d).reverse

Mapping vertex names commutes with edge reversal.