Vizing fans

A fan at a vertex x starting at an uncoloured edge x y is a sequence of distinct neighbours f 0 = y, f 1, …, f n of x such that the colour of x (f (i+1)) is free at f i. Rotating a fan whose last vertex misses a colour that is also missing at x colours the edge x y.

structure LeanPool.Vizing.PEC.IsFan {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (x y : V) (n : ℕ) (f : ℕ → V) : Prop

f 0, …, f n is a fan at x for the uncoloured edge x y.

• start : f 0 = y
• uncoloured : c.col x y = none
• adj (i : ℕ) : i ≤ n → G.Adj x (f i)
• inj (i : ℕ) : i ≤ n → ∀ j ≤ n, f i = f j → i = j
• step (i : ℕ) : i < n → ∃ (γ : C), c.col x (f (i + 1)) = some γ ∧ c.IsFree (f i) γ

theorem LeanPool.Vizing.PEC.IsFan.length_le {V : Type u_1} [Fintype V] {C : Type u_2} {G : SimpleGraph V} {c : PEC G C} {x y : V} {n : ℕ} {f : ℕ → V} (h : c.IsFan x y n f) : n ≤ Fintype.card V

A fan has at most Fintype.card V vertices.

theorem LeanPool.Vizing.PEC.fan_rotate {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (x y : V) (f : ℕ → V) (n : ℕ) (c : PEC G C) (b : C) : c.IsFan x y n f → c.IsFree x b → c.IsFree (f n) b → ∃ (c' : PEC G C), c.Extends c' ∧ c'.col x y ≠ none

Rotating a fan: if some colour b is free both at x and at the last vertex of the fan, then the uncoloured edge x y can be coloured (after recolouring the fan edges).

theorem LeanPool.Vizing.PEC.exists_maximal_fan {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} [Finite V] (c : PEC G C) {x y : V} (hadj : G.Adj x y) (hnone : c.col x y = none) : ∃ (n : ℕ) (f : ℕ → V), c.IsFan x y n f ∧ ∀ (m : ℕ) (g : ℕ → V), c.IsFan x y m g → m ≤ n

Existence of a maximal fan.