The Vizing extension step #
Given a partial proper edge colouring with Δ + 1 colours and an uncoloured edge x y, one can
recolour so that x y becomes coloured and no edge loses its colour. This is the heart of
Vizing's theorem: a maximal fan at x is rotated, after a Kempe chain interchange if needed.
theorem
LeanPool.Vizing.PEC.isFan_kempeSwap
{V : Type u_1}
{C : Type u_2}
[DecidableEq C]
{G : SimpleGraph V}
(c : PEC G C)
{x y : V}
{n : ℕ}
{f : ℕ → V}
(hfan : c.IsFan x y n f)
{a b : C}
(ha : c.IsFree x a)
(w : V)
{m : ℕ}
(hm : m ≤ n)
(hbreak :
∀ i < m, c.col x (f (i + 1)) = some b → ((c.kempeGraph a b).Reachable w (f i) ↔ (c.kempeGraph a b).Reachable w x))
:
A fan survives a Kempe interchange of a and b (where a is free at x) up to the first
index at which the fan edge is coloured b and the interchange separates f i from x.
theorem
LeanPool.Vizing.PEC.vizing_step
{V : Type u_1}
[Fintype V]
{C : Type u_2}
[Fintype C]
{G : SimpleGraph V}
[DecidableRel G.Adj]
(c : PEC G C)
(hcard : G.maxDegree < Fintype.card C)
{x y : V}
(hadj : G.Adj x y)
(hnone : c.col x y = none)
:
Vizing's extension step.