Equitable edge-colouring definitions and finite descent

Equitability means that all colour-class sizes differ by at most one, including unused colours. Minimizing the sum of their squared sizes gives the termination argument for Kempe recolouring. An equitable colouring also has every class bounded by the ceiling of the average size.

def LeanPool.Vizing.EquitableDefinitions.IsEquitable {V : Type u_1} {Color : Type u_2} [DecidableEq Color] (E : Finset (Sym2 V)) (colour : Sym2 V → Color) : Prop

All literal colour classes differ in cardinality by at most one.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Vizing.EquitableDefinitions.energy {V : Type u_1} {Color : Type u_2} [Fintype Color] [DecidableEq Color] (E : Finset (Sym2 V)) (colour : Sym2 V → Color) : ℕ

The square-energy used by alternating-component descent.

Equations

• LeanPool.Vizing.EquitableDefinitions.energy E colour = ∑ a : Color, (LeanPool.Vizing.ColourClasses.colourClass E colour a).card ^ 2

theorem LeanPool.Vizing.EquitableDefinitions.two_class_energy_drop {small large : ℕ} (hgap : small + 1 < large) : (large - 1) ^ 2 + (small + 1) ^ 2 < large ^ 2 + small ^ 2

The exact arithmetic behind one balancing move. Moving one edge from a class of size large to a class of size small strictly decreases the square-energy as soon as the two sizes differ by at least two.

theorem LeanPool.Vizing.EquitableDefinitions.exists_equitable_of_energy_descent {V : Type u_1} {Color : Type u_2} [DecidableEq V] [Fintype Color] [DecidableEq Color] (E : Finset (Sym2 V)) (step : ∀ (colour : Sym2 V → Color), ColourClasses.ProperOn E colour → ¬IsEquitable E colour → ∃ (colour' : Sym2 V → Color), ColourClasses.ProperOn E colour' ∧ energy E colour' < energy E colour) (colour : Sym2 V → Color) (hproper : ColourClasses.ProperOn E colour) : ∃ (colour' : Sym2 V → Color), ColourClasses.ProperOn E colour' ∧ IsEquitable E colour'

Finite descent is logically separate from the Kempe-component lemma. If every non-equitable proper colouring admits one proper recolouring of smaller energy, then an equitable proper colouring exists. This packages the global termination argument without assuming any graph-theoretic input.

theorem LeanPool.Vizing.EquitableDefinitions.sum_card_colourClass_univ {V : Type u_1} {Color : Type u_2} [Fintype Color] [DecidableEq Color] (E : Finset (Sym2 V)) (colour : Sym2 V → Color) : ∑ a : Color, (ColourClasses.colourClass E colour a).card = E.card

Summing over the whole declared palette counts every literal edge once; unused colours simply contribute zero.

def LeanPool.Vizing.EquitableDefinitions.classCeiling (m c : ℕ) : ℕ

The natural ceiling of the average class size.

Equations

• LeanPool.Vizing.EquitableDefinitions.classCeiling m c = m ⌈/⌉ c

theorem LeanPool.Vizing.EquitableDefinitions.edge_count_le_colors_mul_ceiling (m c : ℕ) (hc : 0 < c) : m ≤ c * classCeiling m c

theorem LeanPool.Vizing.EquitableDefinitions.class_card_le_ceiling_of_equitable {V : Type u_1} {Color : Type u_2} [Fintype Color] [DecidableEq Color] [Nonempty Color] (E : Finset (Sym2 V)) (colour : Sym2 V → Color) (hEq : IsEquitable E colour) (a : Color) : (ColourClasses.colourClass E colour a).card ≤ classCeiling E.card (Fintype.card Color)

Equitability bounds each class by the ceiling of the average size.

structure LeanPool.Vizing.EquitableDefinitions.BoundedColouring {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (Color : Type u_3) [Fintype Color] [DecidableEq Color] (t : ℕ) : Type (max u_1 u_3)

A proper edge colouring with a uniform bound on every colour class.

• colour : Sym2 V → Color

  The colour assigned to each unordered vertex pair.

• proper : ColourClasses.ProperOn E self.colour
• class_card_le (a : Color) : (ColourClasses.colourClass E self.colour a).card ≤ t

def LeanPool.Vizing.EquitableDefinitions.boundedColouringOfEquitable {V : Type u_1} {Color : Type u_2} [DecidableEq V] [Fintype Color] [DecidableEq Color] [Nonempty Color] (E : Finset (Sym2 V)) (colour : Sym2 V → Color) (hproper : ColourClasses.ProperOn E colour) (hEq : IsEquitable E colour) : BoundedColouring E Color (classCeiling E.card (Fintype.card Color))

Package the class-size bound supplied by an equitable proper colouring.

Equations

• LeanPool.Vizing.EquitableDefinitions.boundedColouringOfEquitable E colour hproper hEq = { colour := colour, proper := hproper, class_card_le := ⋯ }