Linear ranks and literal directed rotation intervals

Cutting a finite vertex cycle at any one of its darts gives first-hit ranks. These ranks retain the direction of the supplied rotation, without a geometric realization or any restriction on the graph's loops or components.

theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_le {G : Graph} (r : G.RotationSystem) {a b : G.Dart} (hab : a.vertex = b.vertex) {n : ℕ} (hn : (r.rotate ^ n) a = b) : r.rotationDistance a b ≤ n

First-hit distance is bounded by any successful forward iterate.

theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_lt_period {G : Graph} (r : G.RotationSystem) {a b : G.Dart} (hab : a.vertex = b.vertex) : r.rotationDistance a b < Function.minimalPeriod (⇑r.rotate) a

First-hit ranks fit in one complete vertex cycle, including singleton cycles.

theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_pow {G : Graph} (r : G.RotationSystem) (o : G.Dart) (k : ℕ) : r.rotationDistance o ((r.rotate ^ k) o) = k % Function.minimalPeriod (⇑r.rotate) o

The rank of a forward iterate is its exponent reduced modulo the vertex period.

theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_pow_from {G : Graph} (r : G.RotationSystem) (o a : G.Dart) (hoa : o.vertex = a.vertex) (k : ℕ) : r.rotationDistance o ((r.rotate ^ k) a) = (r.rotationDistance o a + k) % Function.minimalPeriod (⇑r.rotate) o

Forward rotation adds to a rank modulo the same vertex period.

theorem Cslib.Complexity.Graph.RotationSystem.mem_rotationInterval_iff_ranks {G : Graph} (r : G.RotationSystem) (o a b c : G.Dart) (hoa : o.vertex = a.vertex) (hob : o.vertex = b.vertex) (hoc : o.vertex = c.vertex) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) : b ∈ r.rotationInterval a c ↔ r.rotationDistance o a < r.rotationDistance o b ∧ r.rotationDistance o b < r.rotationDistance o c ∨ r.rotationDistance o b < r.rotationDistance o c ∧ r.rotationDistance o c < r.rotationDistance o a ∨ r.rotationDistance o c < r.rotationDistance o a ∧ r.rotationDistance o a < r.rotationDistance o b

The actual directed rotation interval is the cyclic order of first-hit ranks at any chosen cut. All three darts must be distinct and belong to that vertex cycle.

noncomputable def Cslib.Complexity.Graph.RotationSystem.portRank {G : Graph} (r : G.RotationSystem) (d : G.Dart) : ℕ

A zero-based linear rank of an incident dart, cutting each literal vertex cycle at one classically chosen dart. Different indexed ends, including loop ends, remain distinct.

theorem Cslib.Complexity.Graph.RotationSystem.portRank_injective {G : Graph} (r : G.RotationSystem) (a b : G.Dart) (hab : a.vertex = b.vertex) (heq : r.portRank a = r.portRank b) : a = b

Ranks distinguish every actual dart at a vertex.

theorem Cslib.Complexity.Graph.RotationSystem.mem_rotationInterval_iff_portRank {G : Graph} (r : G.RotationSystem) (a b c : G.Dart) (hab : a.vertex = b.vertex) (hbc : b.vertex = c.vertex) (hneab : a ≠ b) (hnebc : b ≠ c) (hneac : a ≠ c) : b ∈ r.rotationInterval a c ↔ r.portRank a < r.portRank b ∧ r.portRank b < r.portRank c ∨ r.portRank b < r.portRank c ∧ r.portRank c < r.portRank a ∨ r.portRank c < r.portRank a ∧ r.portRank a < r.portRank b

The chosen linear ranks retain the supplied clockwise cyclic interval.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_self {G : Graph} (r : G.RotationSystem) (a : G.Dart) : r.rotationDistance a a = 0

A vertex cycle first reaches its starting dart at exponent zero.

theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_pos_of_ne {G : Graph} (r : G.RotationSystem) (o a : G.Dart) (hoa : o.vertex = a.vertex) (hne : a ≠ o) : 0 < r.rotationDistance o a

A different dart in the same source cycle has positive first-hit rank.

theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_rotate_of_ne {G : Graph} (r : G.RotationSystem) (o a : G.Dart) (hoa : o.vertex = a.vertex) (hne : r.rotate a ≠ o) : r.rotationDistance o (r.rotate a) = r.rotationDistance o a + 1

A forward source step adds one to the first-hit rank until it returns to the specified cycle cut.

theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_of_rotate_eq {G : Graph} (r : G.RotationSystem) (o a : G.Dart) (hoa : o.vertex = a.vertex) (heq : r.rotate a = o) : r.rotationDistance o a = Function.minimalPeriod (⇑r.rotate) o - 1

The predecessor of a source cycle cut has its last rank, including unary cycles.

noncomputable def Cslib.Complexity.Graph.RotationSystem.sourceTailEquiv {G : Graph} (r : G.RotationSystem) (o : G.Dart) : { d : G.Dart // d.vertex = o.vertex ∧ d ≠ o } ≃ Fin (Function.minimalPeriod (⇑r.rotate) o - 1)

The source vertex cycle after omitting its specified dart, in the original forward order. A unary vertex cycle gives Fin 0, without inventing a corner dart.

theorem Cslib.Complexity.Graph.RotationSystem.sourceTailEquiv_symm_val {G : Graph} (r : G.RotationSystem) (o : G.Dart) (i : Fin (Function.minimalPeriod (⇑r.rotate) o - 1)) : ↑((r.sourceTailEquiv o).symm i) = (r.rotate ^ (↑i + 1)) o

The actual tail enumeration follows the original successor powers, rather than reusing contracted distances that have changed when the selected darts were removed.

theorem Cslib.Complexity.Graph.RotationSystem.mem_rotationInterval_iff_lt_distance {G : Graph} (r : G.RotationSystem) (a b c : G.Dart) (hab : a.vertex = b.vertex) (hac : a.vertex = c.vertex) (hneab : a ≠ b) (hnebc : b ≠ c) (hneac : a ≠ c) : b ∈ r.rotationInterval a c ↔ r.rotationDistance a b < r.rotationDistance a c

A strict interval based at its rank origin compares the two terminal ranks.

theorem Cslib.Complexity.Graph.RotationSystem.mem_rotationInterval_cyclic {G : Graph} (r : G.RotationSystem) (a b c : G.Dart) (hab : a.vertex = b.vertex) (hbc : b.vertex = c.vertex) (hneab : a ≠ b) (hnebc : b ≠ c) (hneac : a ≠ c) : b ∈ r.rotationInterval a c ↔ c ∈ r.rotationInterval b a

Strict literal rotation intervals are cyclic in three distinct incident darts.