The two retained blocks at a contracted edge

Cut a source vertex cycle at the actual dart of the edge being contracted. Its other darts have the literal successive ranks one through period minus one. A singleton source cycle gives an empty block. Indexed parallel occurrences and both ends of loops are retained as distinct darts.

def Cslib.Complexity.Graph.RotationSystem.contractionLift (G : Graph) (u v : ℕ) (d : (contractLastEdgeGraph G u v).Dart) : (lastEdgeGraph G u v).Dart

Lift a retained contracted dart to its actual source edge occurrence and end tag.

theorem Cslib.Complexity.Graph.RotationSystem.contractionLift_coordinates (G : Graph) (u v : ℕ) (d : (contractLastEdgeGraph G u v).Dart) : ((contractLastEdgeDartEquiv G u v).trans (lastEdgeDartEquiv (contractLastEdgeGraph G u v) v v)) (contractionLift G u v d) = some (some d)

The retained coordinate has exactly its original double-some tag.

theorem Cslib.Complexity.Graph.RotationSystem.contractionLift_relabelEquiv (G : Graph) (u v : ℕ) (d : G.Dart) : contractionLift G u v ((Dart.relabelEquiv G (Function.update id u v)) d) = retainedLastEdgeDart G u v d

A retained edge keeps its literal old index and Boolean end tag under the lift.

theorem Cslib.Complexity.Graph.RotationSystem.contractionLift_injective (G : Graph) (u v : ℕ) : Function.Injective (contractionLift G u v)

Distinct retained ends lift to distinct source ends, including ends of a target loop.

theorem Cslib.Complexity.Graph.RotationSystem.contractionLift_ne_lastEdgeDart (G : Graph) (u v : ℕ) (d : (contractLastEdgeGraph G u v).Dart) (side : Bool) : contractionLift G u v d ≠ lastEdgeDart G u v side

A retained dart is never either deleted end of the selected source edge.

theorem Cslib.Complexity.Graph.RotationSystem.vertex_contractionLift (G : Graph) (u v : ℕ) (d : (contractLastEdgeGraph G u v).Dart) : Function.update id u v (contractionLift G u v d).vertex = d.vertex

Source endpoint names undergo exactly the prescribed directed identification.

theorem Cslib.Complexity.Graph.RotationSystem.contractionLift_vertex_eq_iff (G : Graph) (u v : ℕ) (d : (contractLastEdgeGraph G u v).Dart) : d.vertex = v ↔ (contractionLift G u v d).vertex = u ∨ (contractionLift G u v d).vertex = v

Retained darts at the contracted name originate from precisely the two source endpoint fibers. This includes both occurrences of a source edge that became a loop.

noncomputable def Cslib.Complexity.Graph.RotationSystem.contractionRetainedEquiv (G : Graph) (u v : ℕ) : (contractLastEdgeGraph G u v).Dart ≃ { a : (lastEdgeGraph G u v).Dart // ∀ (side : Bool), a ≠ lastEdgeDart G u v side }

Exactly the two selected source darts are omitted by contraction. The retained correspondence is an equivalence of actual occurrences, without identifying loop ends.

theorem Cslib.Complexity.Graph.RotationSystem.contractionRetainedEquiv_apply_val (G : Graph) (u v : ℕ) (d : (contractLastEdgeGraph G u v).Dart) : ↑((contractionRetainedEquiv G u v) d) = contractionLift G u v d

The retained equivalence lifts to the original indexed source dart.

noncomputable def Cslib.Complexity.Graph.RotationSystem.contractionBlock {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (d : { d : (contractLastEdgeGraph G u v).Dart // d.vertex = v }) : Fin (Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v true) - 1) ⊕ Fin (Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v false) - 1)

The two source blocks of a retained contracted-vertex dart. The first block is the retained v cycle and the second is the retained u cycle, both in their original forward ranks after the deleted dart.

theorem Cslib.Complexity.Graph.RotationSystem.contractionBlock_injective {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) : Function.Injective r.contractionBlock

Source block ranks distinguish every retained occurrence of the contracted vertex.

theorem Cslib.Complexity.Graph.RotationSystem.contractionBlock_surjective {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) : Function.Surjective r.contractionBlock

Every entry of either retained source block is an actual contracted-vertex dart. An empty block remains empty; no corner or port is supplied for it.

noncomputable def Cslib.Complexity.Graph.RotationSystem.contractionBlockEquiv {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) : { d : (contractLastEdgeGraph G u v).Dart // d.vertex = v } ≃ Fin (Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v true) - 1) ⊕ Fin (Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v false) - 1)

Exact source block coordinates for every dart at the contracted vertex.

theorem Cslib.Complexity.Graph.RotationSystem.contractionLift_rotate_paths {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (d : (contractLastEdgeGraph G u v).Dart) : have σ := r.rotate * Equiv.swap (lastEdgeDart G u v true) (lastEdgeDart G u v false); have a := contractionLift G u v d; have b := contractionLift G u v ((r.contractLastEdge huv).rotate d); σ a = b ∨ σ a = lastEdgeDart G u v true ∧ σ (lastEdgeDart G u v true) = b ∨ σ a = lastEdgeDart G u v false ∧ σ (lastEdgeDart G u v false) = b ∨ σ a = lastEdgeDart G u v true ∧ σ (lastEdgeDart G u v true) = lastEdgeDart G u v false ∧ σ (lastEdgeDart G u v false) = b ∨ σ a = lastEdgeDart G u v false ∧ σ (lastEdgeDart G u v false) = lastEdgeDart G u v true ∧ σ (lastEdgeDart G u v true) = b

The actual contracted successor is first return in the literal outgoing-swapped source rotation. The directed paths are obtained from the constructor, not assumed as a block-order or splitter premise.

theorem Cslib.Complexity.Graph.RotationSystem.contractionLift_rotate_cases {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (d : (contractLastEdgeGraph G u v).Dart) : have a := contractionLift G u v d; have b := contractionLift G u v ((r.contractLastEdge huv).rotate d); r.rotate a = b ∨ r.rotate a = lastEdgeDart G u v true ∧ r.rotate (lastEdgeDart G u v false) = b ∨ r.rotate a = lastEdgeDart G u v false ∧ r.rotate (lastEdgeDart G u v true) = b ∨ r.rotate a = lastEdgeDart G u v true ∧ r.rotate (lastEdgeDart G u v false) = lastEdgeDart G u v false ∧ r.rotate (lastEdgeDart G u v true) = b ∨ r.rotate a = lastEdgeDart G u v false ∧ r.rotate (lastEdgeDart G u v true) = lastEdgeDart G u v true ∧ r.rotate (lastEdgeDart G u v false) = b

The outgoing swap joins the retained v block to the retained u block. The three-step alternatives skip a unary source cycle; their order is literal.

noncomputable def Cslib.Complexity.Graph.RotationSystem.contractionRank {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (d : { d : (contractLastEdgeGraph G u v).Dart // d.vertex = v }) : Fin (Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v true) - 1 + (Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v false) - 1))

Consecutive retained source-block ranks, with the v block first.

theorem Cslib.Complexity.Graph.RotationSystem.val_contractionRank {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (d : { d : (contractLastEdgeGraph G u v).Dart // d.vertex = v }) : ↑(r.contractionRank d) = if (contractionLift G u v ↑d).vertex = v then r.rotationDistance (lastEdgeDart G u v true) (contractionLift G u v ↑d) - 1 else Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v true) - 1 + (r.rotationDistance (lastEdgeDart G u v false) (contractionLift G u v ↑d) - 1)

The rank is the original first-hit rank minus the deleted dart, with an offset for the second source block. No contracted distance is reused.

theorem Cslib.Complexity.Graph.RotationSystem.contractionRank_lt_iff_sourceDistance_lt {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (a b : { 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) : ↑(r.contractionRank a) < ↑(r.contractionRank b) ↔ r.rotationDistance (lastEdgeDart G u v side) (contractionLift G u v ↑a) < r.rotationDistance (lastEdgeDart G u v side) (contractionLift G u v ↑b)

Within either source block, retained rank comparisons are original rank comparisons.

noncomputable def Cslib.Complexity.Graph.RotationSystem.contractionRankEquiv {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) : { d : (contractLastEdgeGraph G u v).Dart // d.vertex = v } ≃ Fin (Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v true) - 1 + (Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v false) - 1))

Source block ranks are an equivalence onto one finite consecutive interval.

theorem Cslib.Complexity.Graph.RotationSystem.val_contractionRank_rotate {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (d : { d : (contractLastEdgeGraph G u v).Dart // d.vertex = v }) : have d' := ⟨(r.contractLastEdge huv).rotate ↑d, ⋯⟩; ↑(r.contractionRank d') = (↑(r.contractionRank d) + 1) % (Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v true) - 1 + (Function.minimalPeriod (⇑r.rotate) (lastEdgeDart G u v false) - 1))

The actual contracted rotation traverses the two original retained blocks consecutively, in their original direction. Empty blocks are skipped automatically.

theorem Cslib.Complexity.Graph.RotationSystem.exists_contractionRank_origin {G : Graph} {u v : ℕ} (r : (lastEdgeGraph G u v).RotationSystem) (huv : u ≠ v) (a : { d : (contractLastEdgeGraph G u v).Dart // d.vertex = v }) : ∃ (o : { d : (contractLastEdgeGraph G u v).Dart // d.vertex = v }), ∀ (d : { d : (contractLastEdgeGraph G u v).Dart // d.vertex = v }), (r.contractLastEdge huv).rotationDistance ↑o ↑d = ↑(r.contractionRank d)

Whenever the contracted vertex has a retained dart, its block rank zero is an actual cycle origin, and all first-hit distances from it are the consecutive block ranks.

theorem Cslib.Complexity.Graph.RotationSystem.mem_rotationInterval_contractLastEdge_iff_ranks {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 }) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) : ↑b ∈ (r.contractLastEdge huv).rotationInterval ↑a ↑c ↔ ↑(r.contractionRank a) < ↑(r.contractionRank b) ∧ ↑(r.contractionRank b) < ↑(r.contractionRank c) ∨ ↑(r.contractionRank b) < ↑(r.contractionRank c) ∧ ↑(r.contractionRank c) < ↑(r.contractionRank a) ∨ ↑(r.contractionRank c) < ↑(r.contractionRank a) ∧ ↑(r.contractionRank a) < ↑(r.contractionRank b)

The literal contracted rotation interval is precisely the cyclic order of the two consecutive retained source blocks. Both empty-block conventions are internal.