PathRotation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed-end path rotation

The explicit tail reversal used in manuscript Lemma clq:coloured-path is proved here. The pivot may be the first vertex, and the last vertex becomes the successor of the pivot. No path-rotation theorem is assumed.

def OAI.CycleClique.Construction.rotationIndex line 15
Source documentation
Reverse precisely the indices strictly after the pivot.
```
def rotationIndex {r : ℕ} (p : Fin r) (i : Fin (r + 1)) : Fin (r + 1) :=
…
```
theorem OAI.CycleClique.Construction.rotationIndex_involutive line 19
theorem OAI.CycleClique.Construction.rotationIndex_injective line 26
theorem OAI.CycleClique.Construction.rotationIndex_zero line 29
theorem OAI.CycleClique.Construction.rotationIndex_last line 33
theorem OAI.CycleClique.Construction.rotationIndex_range line 39

theorem OAI.CycleClique.Construction.rotate_path line 51

Source documentation

Rotating a simple path around a neighbour of its last vertex preserves every vertex and the first endpoint, and makes the pivot's successor the new last endpoint.

theorem rotate_path {V : Type*} {G : SimpleGraph V} {r : ℕ}
    (f : Fin (r + 1) → V) (hf : Function.Injective f)
    (hchain : ∀ i : Fin r, G.Adj (f i.castSucc) (f i.succ))
    (p : Fin r) (hp : G.Adj (f (Fin.last r)) (f p.castSucc)) :
    Function.Injective (f ∘ rotationIndex p) ∧
      (∀ i : Fin r, G.Adj ((f ∘ rotationIndex p) i.castSucc)
        ((f ∘ rotationIndex p) i.succ)) ∧
      (f ∘ rotationIndex p) 0 = f 0 ∧
      (f ∘ rotationIndex p) (Fin.last r) = f p.succ ∧
      Set.range (f ∘ rotationIndex p) = Set.range f := by
…

Mentions: OAI.CycleClique.Construction.rotationIndex