Unchanged vertex cycles during actual nonloop contraction #
Away from the contracted vertex, the literal successor and all its forward iterates commute with the retained-dart lift. Distances and intervals are preserved on those unchanged fibers only; no distance preservation is asserted across the deleted darts.
theorem Cslib.Complexity.Graph.RotationSystem.vertex_contractionLift_of_ne {G : Graph} {u v : ℕ} (d : (contractLastEdgeGraph G u v).Dart) (hd : d.vertex ≠ v) :
A retained end away from the contracted vertex has its original source name.
theorem Cslib.Complexity.Graph.RotationSystem.contractionLift_rotate_of_ne {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (d : (contractLastEdgeGraph G u v).Dart) (hd : d.vertex ≠ v) :
The outgoing swap and deletions do not change any other vertex's successor.
theorem Cslib.Complexity.Graph.RotationSystem.contractionLift_pow_of_ne {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (d : (contractLastEdgeGraph G u v).Dart) (hd : d.vertex ≠ v) (n : ℕ) :
(r.rotate ^ n) (contractionLift G u v d) = contractionLift G u v (((r.contractLastEdge huv).rotate ^ n) d)
Every forward iterate commutes with the retained lift on an unchanged vertex fiber.
theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_contractionLift_of_ne {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (a b : (contractLastEdgeGraph G u v).Dart) (hab : a.vertex = b.vertex) (ha : a.vertex ≠ v) :
r.rotationDistance (contractionLift G u v a) (contractionLift G u v b) = (r.contractLastEdge huv).rotationDistance a b
First-hit distances agree only on vertex fibers untouched by contraction.
theorem Cslib.Complexity.Graph.RotationSystem.mem_rotationInterval_contractionLift_of_ne {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (a b c : (contractLastEdgeGraph G u v).Dart) (hac : a.vertex = c.vertex) (ha : a.vertex ≠ v) :
b ∈ (r.contractLastEdge huv).rotationInterval a c ↔ contractionLift G u v b ∈ r.rotationInterval (contractionLift G u v a) (contractionLift G u v c)
Literal directed intervals agree on every vertex cycle untouched by contraction.
theorem Cslib.Complexity.Graph.RotationSystem.contraction_dart_cases (G : Graph) (u v : ℕ) (d : (lastEdgeGraph G u v).Dart) :
(∃ (e : (contractLastEdgeGraph G u v).Dart), d = contractionLift G u v e) ∨ ∃ (side : Bool), d = lastEdgeDart G u v side
Every actual source dart is either a lifted retained occurrence or a selected end.