Transport of polygonal realizations along indexed edge equivalences

An equivalence of edge positions retaining their two named endpoints transports actual routes, every real segment contact, and the literal clockwise rotation. Equal declared membership suffices; declaration lists need not be equal or without repetitions.

theorem Cslib.Complexity.Graph.exists_lastEdge_reindex (G : Graph) (i : Fin G.edges.length) : ∃ (H : Graph) (u : ℕ) (v : ℕ) (e : Fin G.edges.length ≃ Fin (RotationSystem.lastEdgeGraph H u v).edges.length), H.vertices = G.vertices ∧ H.edges.length + 1 = G.edges.length ∧ (∀ (j : Fin G.edges.length) (b : Bool), Dart.vertex (e j, b) = Dart.vertex (j, b)) ∧ e i = (RotationSystem.lastEdgeDart H u v false).1 ∧ u = Dart.vertex (i, false) ∧ v = Dart.vertex (i, true)

Move any selected indexed edge to the last position by an actual permutation of edge occurrences. Both end tags and all declared names remain unchanged. Equal edge pairs are still transported by their positions.

theorem Cslib.Complexity.Graph.endpoints_declared_edge_reindex {G H : Graph} (e : Fin G.edges.length ≃ Fin H.edges.length) (hv : ∀ (i : Fin G.edges.length) (b : Bool), Dart.vertex (e i, b) = Dart.vertex (i, b)) (hm : ∀ (v : ℕ), v ∈ G.vertices ↔ v ∈ H.vertices) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (v : ℕ) : v ∈ H.incidenceVertices → v ∈ H.vertices

Actual indexed edge reindexing preserves declaration of all listed endpoints.

theorem Cslib.Complexity.Graph.RotationSystem.transport_symm {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) (hw : ∀ (a b : H.Dart), (e.symm a).vertex = (e.symm b).vertex ↔ a.vertex = b.vertex) : (r.transport e hv).transport e.symm hw = r

Transporting a literal rotation back along the inverse dart equivalence recovers it.

theorem Cslib.Complexity.Graph.RotationSystem.pow_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) (n : ℕ) (a : G.Dart) : ((r.transport e hv).rotate ^ n) (e a) = e ((r.rotate ^ n) a)

Dart conjugacy retains every literal forward iterate of a rotation.

theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_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) (a b : G.Dart) : (r.transport e hv).rotationDistance (e a) (e b) = r.rotationDistance a b

A dart equivalence preserves first-hit distances, including different vertex fibers.

theorem Cslib.Complexity.Graph.RotationSystem.mem_rotationInterval_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) (a b c : G.Dart) : e b ∈ (r.transport e hv).rotationInterval (e a) (e c) ↔ b ∈ r.rotationInterval a c

Literal directed rotation intervals commute with dart conjugacy.

def Cslib.Complexity.Graph.PolygonalDrawing.edgeTransport {G H : Graph} (D : G.PolygonalDrawing) (e : Fin G.edges.length ≃ Fin H.edges.length) (hv : ∀ (i : Fin G.edges.length) (b : Bool), Dart.vertex (e i, b) = Dart.vertex (i, b)) : H.PolygonalDrawing

Reindex routes by actual edge occurrences, retaining the end tag and named endpoints. The declaration list may be changed separately.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.edgeTransport {G H : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) (e : Fin G.edges.length ≃ Fin H.edges.length) (hv : ∀ (i : Fin G.edges.length) (b : Bool), Dart.vertex (e i, b) = Dart.vertex (i, b)) (hm : ∀ (v : ℕ), v ∈ G.vertices ↔ v ∈ H.vertices) : (D.edgeTransport e hv).IsEmbedding

Indexed edge transport preserves the full real-affine embedding semantics. Repeated declarations are compared by membership, not by their list positions.

theorem Cslib.Complexity.Graph.PolygonalDrawing.germ_edgeTransport {G H : Graph} (D : G.PolygonalDrawing) (e : Fin G.edges.length ≃ Fin H.edges.length) (hv : ∀ (i : Fin G.edges.length) (b : Bool), Dart.vertex (e i, b) = Dart.vertex (i, b)) (a : G.Dart) : (D.edgeTransport e hv).germ (e a.1, a.2) = D.germ a

Actual germ vectors retain the edge occurrence and end tag under transport.

theorem Cslib.Complexity.Graph.PolygonalDrawing.Realizes.edgeTransport {G H : Graph} {D : G.PolygonalDrawing} {r : G.RotationSystem} (hR : D.Realizes r) (e : Fin G.edges.length ≃ Fin H.edges.length) (hv : ∀ (i : Fin G.edges.length) (b : Bool), Dart.vertex (e i, b) = Dart.vertex (i, b)) : (D.edgeTransport e hv).Realizes (r.transport (e.prodCongr (Equiv.refl Bool)) ⋯)

Edge reindexing retains exact clockwise realization, including the two distinct ends of every loop. No reflection or change of the planar coordinates is used.