Directed intervals inside the two retained contraction blocks

Each retained source block preserves its strict cyclic triples. Source first-hit ranks are compared only after their explicit deletion offset; raw distances across the deleted ends are never identified.

theorem Cslib.Complexity.Graph.RotationSystem.mem_rotationInterval_contractionLift_active {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (a b c : { d : (contractLastEdgeGraph G u v).Dart // d.vertex = v }) (side : Bool) (ha : (contractionLift G u v ↑a).vertex = (lastEdgeDart G u v side).vertex) (hb : (contractionLift G u v ↑b).vertex = (lastEdgeDart G u v side).vertex) (hc : (contractionLift G u v ↑c).vertex = (lastEdgeDart G u v side).vertex) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) : ↑b ∈ (r.contractLastEdge huv).rotationInterval ↑a ↑c ↔ contractionLift G u v ↑b ∈ r.rotationInterval (contractionLift G u v ↑a) (contractionLift G u v ↑c)

All distinct retained triples in either original endpoint cycle retain literal cyclic order after the outgoing swap and two deletions.