Parity algebra for the four-colour argument

This file records the two finite characteristic-two calculations used after the local choices have been balanced: polarization of the quadratic form along an ordered word, and recovery of the parity of all four colour classes from its linear and quadratic moments.

def Sabidussi.orderedPairBracket {n : ℕ} (f : Fin n → Color) : F₂

The sum of the bracket over all ordered pairs of positions, each pair occurring with its smaller position second.

Equations

• Sabidussi.orderedPairBracket f = ∑ i : Fin n, ∑ j : Fin n, if j < i then Sabidussi.bracket (f i) (f j) else 0

theorem Sabidussi.orderedPairBracket_succ {n : ℕ} (f : Fin (n + 1) → Color) : orderedPairBracket f = (orderedPairBracket fun (i : Fin n) => f i.castSucc) + bracket (∑ i : Fin n, f i.castSucc) (f (Fin.last n))

Adding the last position adds precisely its brackets with all earlier positions.

theorem Sabidussi.quadratic_sum_fin {n : ℕ} (f : Fin n → Color) : quadratic (∑ i : Fin n, f i) = ∑ i : Fin n, quadratic (f i) + orderedPairBracket f

Polarization of quadratic along a finite linearly ordered word.

def Sabidussi.colorFiber {I : Type u_1} [Fintype I] (f : I → Color) (c : Color) : Finset I

The positions carrying a specified colour.

Equations

• Sabidussi.colorFiber f c = {i : I | f i = c}

theorem Sabidussi.cast_colorFiber_card {I : Type u_1} [Fintype I] (f : I → Color) (c : Color) : ↑(colorFiber f c).card = ∑ i : I, if f i = c then 1 else 0

theorem Sabidussi.colorFiber_card_even_of_moments {I : Type u_1} [Fintype I] (f : I → Color) (hcard : Even (Fintype.card I)) (hsum : ∑ i : I, f i = 0) (hquadratic : ∑ i : I, quadratic (f i) = 0) (c : Color) : Even (colorFiber f c).card

In an even finite family of four colours, vanishing of the two linear moments and of the quadratic moment is equivalent to every colour occurring evenly. This is the forward direction needed in the Sabidussi argument.