Transport of actual indexed rotations

Dart equivalences preserve componentwise numerical genus when they preserve reversal and the endpoint-fiber partition. Declared isolated points need no invented darts: their numerical Euler convention is retained separately by the existing predicate. Edge occurrences, loops and parallel edges remain indexed throughout.

def Cslib.Complexity.Graph.RotationSystem.graphEqDartEquiv {G H : Graph} (h : G = H) : G.Dart ≃ H.Dart

Reinterpret literally equal listed graphs by retaining their edge indices and end bits.

theorem Cslib.Complexity.Graph.RotationSystem.vertex_graphEqDartEquiv {G H : Graph} (h : G = H) (d : G.Dart) : ((graphEqDartEquiv h) d).vertex = d.vertex

Equality transport changes no actual endpoint.

theorem Cslib.Complexity.Graph.RotationSystem.val_graphEqDartEquiv {G H : Graph} (h : G = H) (d : G.Dart) : ↑((graphEqDartEquiv h) d).1 = ↑d.1

Equality transport retains the literal indexed edge position.

theorem Cslib.Complexity.Graph.RotationSystem.side_graphEqDartEquiv {G H : Graph} (h : G = H) (d : G.Dart) : ((graphEqDartEquiv h) d).2 = d.2

Equality transport retains the original end tag.

theorem Cslib.Complexity.Graph.RotationSystem.reverse_graphEqDartEquiv {G H : Graph} (h : G = H) (d : G.Dart) : (graphEqDartEquiv h) d.reverse = ((graphEqDartEquiv h) d).reverse

Equality transport commutes with reversing the indexed edge.

def Cslib.Complexity.Graph.RotationSystem.transport {G H : Graph} (r : G.RotationSystem) (e : G.Dart ≃ H.Dart) (hv : ∀ (a b : G.Dart), (e a).vertex = (e b).vertex ↔ a.vertex = b.vertex) : H.RotationSystem

Reindex actual darts without changing the vertex-fiber partition.

theorem Cslib.Complexity.Graph.RotationSystem.sameCycle_reversal_iff {G : Graph} (a b : G.Dart) : (Dart.reversal G).SameCycle a b ↔ a.1 = b.1

Complete reversal orbits are exactly the indexed listed edge occurrences.

noncomputable def Cslib.Complexity.Graph.RotationSystem.vertexOrbitEquiv {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : (Equiv.Perm.SelectedOrbits.OrbitOn r.rotate fun (a : G.Dart) => RotationCertificate.SameComponent G d.vertex a.vertex) ≃ ↥(G.componentVertexSet d.vertex)

Vertex orbits restricted to an actual edge component are its declared vertex set.

noncomputable def Cslib.Complexity.Graph.RotationSystem.edgeOrbitEquiv (G : Graph) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : (Equiv.Perm.SelectedOrbits.OrbitOn (Dart.reversal G) fun (a : G.Dart) => RotationCertificate.SameComponent G d.vertex a.vertex) ≃ ↥(G.componentEdgeSet d.vertex)

Reversal orbits restricted to an actual edge component are its indexed edge set.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_map_darts {G H : Graph} (e : G.Dart → H.Dart) (hv : ∀ (a b : G.Dart), a.vertex = b.vertex → (e a).vertex = (e b).vertex) (he : ∀ (a : G.Dart), e a.reverse = (e a).reverse) (hH : ∀ v ∈ H.incidenceVertices, v ∈ H.vertices) {a b : G.Dart} (hc : RotationCertificate.SameComponent G a.vertex b.vertex) : RotationCertificate.SameComponent H (e a).vertex (e b).vertex

A dart map preserving endpoint identifications and edge reversal maps every existing edge component into one target component. Injectivity is not required.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_transport_iff {G H : Graph} (e : G.Dart ≃ H.Dart) (hv : ∀ (a b : G.Dart), (e a).vertex = (e b).vertex ↔ a.vertex = b.vertex) (he : ∀ (a : G.Dart), e a.reverse = (e a).reverse) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hH : ∀ v ∈ H.incidenceVertices, v ∈ H.vertices) (a b : G.Dart) : RotationCertificate.SameComponent H (e a).vertex (e b).vertex ↔ RotationCertificate.SameComponent G a.vertex b.vertex

Endpoint-fiber and reversal preserving dart coordinates retain exactly the edge components. There is no injectivity requirement on the natural-number vertex labels themselves.

theorem Cslib.Complexity.Graph.RotationSystem.faceNext_transport {G H : Graph} (r : G.RotationSystem) (e : G.Dart ≃ H.Dart) (hv : ∀ (a b : G.Dart), (e a).vertex = (e b).vertex ↔ a.vertex = b.vertex) (he : ∀ (a : G.Dart), e a.reverse = (e a).reverse) (a : G.Dart) : e (r.faceNext a) = (r.transport e hv).faceNext (e a)

Exact face-successor conjugacy, retaining the inverse-rotation chirality convention.

theorem Cslib.Complexity.Graph.RotationSystem.component_cards_transport {G H : Graph} (r : G.RotationSystem) (e : G.Dart ≃ H.Dart) (hv : ∀ (a b : G.Dart), (e a).vertex = (e b).vertex ↔ a.vertex = b.vertex) (he : ∀ (a : G.Dart), e a.reverse = (e a).reverse) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hH : ∀ v ∈ H.incidenceVertices, v ∈ H.vertices) (d : G.Dart) : (H.componentVertexSet (e d).vertex).card = (G.componentVertexSet d.vertex).card ∧ (H.componentEdgeSet (e d).vertex).card = (G.componentEdgeSet d.vertex).card ∧ Nat.card ((r.transport e hv).ComponentFace (e d).vertex) = Nat.card (r.ComponentFace d.vertex)

Actual vertex, indexed edge and full face counts agree in each transported edge component.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_transport {G H : Graph} (r : G.RotationSystem) (e : G.Dart ≃ H.Dart) (hv : ∀ (a b : G.Dart), (e a).vertex = (e b).vertex ↔ a.vertex = b.vertex) (he : ∀ (a : G.Dart), e a.reverse = (e a).reverse) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hH : ∀ v ∈ H.incidenceVertices, v ∈ H.vertices) (hr : r.NumericalGenusZero) : (r.transport e hv).NumericalGenusZero

Reindexing actual darts while preserving reversal and vertex fibers preserves the existing componentwise numerical genus-zero predicate. Arbitrarily many declared point components are allowed on either graph, because the predicate checks their conventional Euler equation.