The cyclic-word four-colouring lemma

This file is the combinatorial core of the compatibility proof. A letter at a position records the transition between the preceding and the current gap. If every letter occurs at least twice, the local patterns from LocalPattern and the odd balancing theorem produce colours on the gaps such that adjacent gaps have different colours and every colour occurs evenly at each letter.

structure Sabidussi.CyclicWord.Word {V : Type u_1} : Type u_1

A nonempty cyclic word, represented with a chosen cut.

• n : ℕ

  The word has n + 1 positions, so it is always nonempty.

• letter : Fin (self.n + 1) → V

  The letter recorded at each position.

@[reducible, inline]

abbrev Sabidussi.CyclicWord.Word.Pos {V : Type u_1} (W : Word) : Type

Positions of the cyclic word.

Equations

• W.Pos = Fin (W.n + 1)

def Sabidussi.CyclicWord.Word.prev {V : Type u_1} (W : Word) (i : W.Pos) : W.Pos

The position immediately preceding i, cyclically.

Equations

• W.prev i = (Equiv.symm (finRotate (W.n + 1))) i

@[reducible, inline]

abbrev Sabidussi.CyclicWord.Word.Occurrence {V : Type u_1} (W : Word) (v : V) : Type

Occurrences of a letter.

Equations

• W.Occurrence v = { i : W.Pos // W.letter i = v }

@[implicit_reducible]

instance Sabidussi.CyclicWord.Word.instFintypeOccurrence {V : Type u_1} [DecidableEq V] (W : Word) (v : V) : Fintype (W.Occurrence v)

Equations

• W.instFintypeOccurrence v = Subtype.fintype fun (i : W.Pos) => W.letter i = v

def Sabidussi.CyclicWord.Word.incidentColor {V : Type u_1} (W : Word) (x : W.Pos → Color) {v : V} (o : W.Occurrence v) (s : Fin 2) : Color

The two gap colours incident with an occurrence.

Equations

• W.incidentColor x o s = if s = 0 then x (W.prev ↑o) else x ↑o

structure Sabidussi.CyclicWord.Word.Coloring {V : Type u_1} [DecidableEq V] (W : Word) : Type

The desired output of the cyclic-word construction.

• color : W.Pos → Color

  The colour assigned to each gap of the cyclic word.

• transition_ne (i : W.Pos) : self.color (W.prev i) ≠ self.color i

  Consecutive gaps receive different colours.

• color_even (v : V) (z : Color) : Even (Fintype.card { os : W.Occurrence v × Fin 2 // W.incidentColor self.color os.1 os.2 = z })

  Each colour occurs an even number of times among the incidences at every letter.

def Sabidussi.CyclicWord.localQuadraticContribution (n : ℕ) (c : Fin 3) : F₂

The quadratic contribution of a finite ordered difference pattern.

Equations

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

theorem Sabidussi.CyclicWord.quadratic_sum_fin (k : ℕ) (f : Fin k → Color) : quadratic (∑ i : Fin k, f i) = ∑ i : Fin k, quadratic (f i) + ∑ i : Fin k, ∑ j : Fin k, if j < i then bracket (f i) (f j) else 0

Polarization of quadratic over a linearly ordered finite family.

theorem Sabidussi.CyclicWord.localQuadraticContribution_eq_zero (n : ℕ) (c : Fin 3) : localQuadraticContribution n c = 0

The recursively extended local patterns retain the quadratic cancellation of the pair and triple base cases.

noncomputable def Sabidussi.CyclicWord.Word.occurrenceOrderIsoFin {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (v : V) : W.Occurrence v ≃o Fin (Fintype.card (W.Occurrence v) - 2 + 2)

An arbitrary enumeration of the occurrences of each letter, used only to transport the explicit local patterns.

Equations

• W.occurrenceOrderIsoFin hmin v = (Fintype.orderIsoFinOfCardEq (W.Occurrence v) ⋯).symm

noncomputable def Sabidussi.CyclicWord.Word.frameDifference {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (v : V) (c : Fin 3) (o : W.Occurrence v) : Color

The difference at an occurrence for one of the three local choices.

Equations

• W.frameDifference hmin v c o = Sabidussi.localDifference (Fintype.card (W.Occurrence v) - 2) c ((W.occurrenceOrderIsoFin hmin v) o)

theorem Sabidussi.CyclicWord.Word.frameDifference_ne_zero {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (v : V) (c : Fin 3) (o : W.Occurrence v) : W.frameDifference hmin v c o ≠ 0

theorem Sabidussi.CyclicWord.Word.sum_frameDifference_occurrences {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (v : V) (c : Fin 3) : ∑ o : W.Occurrence v, W.frameDifference hmin v c o = 0

theorem Sabidussi.CyclicWord.Word.sum_frameDifference_choices {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (v : V) (o : W.Occurrence v) : ∑ c : Fin 3, W.frameDifference hmin v c o = 0

theorem Sabidussi.CyclicWord.Word.frameDifference_localQuadratic {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (v : V) (c : Fin 3) : (∑ o : W.Occurrence v, quadratic (W.frameDifference hmin v c o) + ∑ o : W.Occurrence v, ∑ p : W.Occurrence v, if ↑p < ↑o then bracket (W.frameDifference hmin v c o) (W.frameDifference hmin v c p) else 0) = 0

noncomputable def Sabidussi.CyclicWord.Word.interaction {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (v u : V) (cv cu : Fin 3) : F₂

The ordered interaction between the local patterns at two letters. The diagonal is set to zero because the balancing theorem is phrased on all ordered pairs of letters.

Equations

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

theorem Sabidussi.CyclicWord.Word.interaction_symm {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (v u : V) (cv cu : Fin 3) : W.interaction hmin v u cv cu = W.interaction hmin u v cu cv

theorem Sabidussi.CyclicWord.Word.sum_interaction_choices {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (v u : V) (cv : Fin 3) : ∑ cu : Fin 3, W.interaction hmin v u cv cu = 0

theorem Sabidussi.CyclicWord.Word.exists_balanced_choice {V : Type u_1} [Fintype V] [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) : ∃ (choice : V → Fin 3), ∀ (v : V), OddBalance.obstruction (W.interaction hmin) choice v = 0

The odd balancing theorem chooses one local frame at every letter so that every external interaction obstruction vanishes.

noncomputable def Sabidussi.CyclicWord.Word.chosenDifference {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (choice : V → Fin 3) (i : W.Pos) : Color

Differences on all positions induced by choices of the local frames.

Equations

• W.chosenDifference hmin choice i = W.frameDifference hmin (W.letter i) (choice (W.letter i)) ⟨i, ⋯⟩

theorem Sabidussi.CyclicWord.Word.chosenDifference_ne_zero {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (choice : V → Fin 3) (i : W.Pos) : W.chosenDifference hmin choice i ≠ 0

theorem Sabidussi.CyclicWord.Word.chosenDifference_at_occurrence {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (choice : V → Fin 3) (v : V) (o : W.Occurrence v) : W.chosenDifference hmin choice ↑o = W.frameDifference hmin v (choice v) o

theorem Sabidussi.CyclicWord.Word.sum_chosenDifference_occurrences {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (choice : V → Fin 3) (v : V) : ∑ o : W.Occurrence v, W.chosenDifference hmin choice ↑o = 0

theorem Sabidussi.CyclicWord.Word.sum_chosenDifference {V : Type u_1} [DecidableEq V] (W : Word) [Finite V] (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (choice : V → Fin 3) : ∑ i : W.Pos, W.chosenDifference hmin choice i = 0

def Sabidussi.CyclicWord.Word.prefixColor {V : Type u_1} (W : Word) (y : W.Pos → Color) (i : W.Pos) : Color

Prefix integration of differences, with the cut placed immediately before position zero.

Equations

• W.prefixColor y i = ∑ j ∈ Finset.Iic i, y j

theorem Sabidussi.CyclicWord.Word.prefixColor_transition {V : Type u_1} (W : Word) (y : W.Pos → Color) (htotal : ∑ i : W.Pos, y i = 0) (i : W.Pos) : W.prefixColor y (W.prev i) + W.prefixColor y i = y i

theorem Sabidussi.CyclicWord.Word.prefixColor_prev_eq_strictPrefix {V : Type u_1} (W : Word) (y : W.Pos → Color) (htotal : ∑ i : W.Pos, y i = 0) (i : W.Pos) : W.prefixColor y (W.prev i) = ∑ j ∈ Finset.Iio i, y j

def Sabidussi.CyclicWord.Word.orderedLetterInteraction {V : Type u_1} [DecidableEq V] (W : Word) (y : W.Pos → Color) (v u : V) : F₂

Contribution of all earlier occurrences of u to occurrences of v.

Equations

• W.orderedLetterInteraction y v u = ∑ i : W.Occurrence v, ∑ j : W.Occurrence u, if ↑j < ↑i then Sabidussi.bracket (y ↑i) (y ↑j) else 0

theorem Sabidussi.CyclicWord.Word.sum_orderedLetterInteraction {V : Type u_1} [Fintype V] [DecidableEq V] (W : Word) (y : W.Pos → Color) (v : V) : ∑ u : V, W.orderedLetterInteraction y v u = ∑ i : W.Occurrence v, ∑ j ∈ Finset.Iio ↑i, bracket (y ↑i) (y j)

Partitioning earlier word positions according to their letter.

theorem Sabidussi.CyclicWord.Word.orderedLetterInteraction_chosen_eq_interaction {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (choice : V → Fin 3) {v u : V} (hvu : v ≠ u) : W.orderedLetterInteraction (W.chosenDifference hmin choice) v u = W.interaction hmin v u (choice v) (choice u)

theorem Sabidussi.CyclicWord.Word.chosen_localQuadratic {V : Type u_1} [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (choice : V → Fin 3) (v : V) : ∑ i : W.Occurrence v, quadratic (W.chosenDifference hmin choice ↑i) + W.orderedLetterInteraction (W.chosenDifference hmin choice) v v = 0

theorem Sabidussi.CyclicWord.Word.chosen_externalInteraction_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (choice : V → Fin 3) (hbalanced : ∀ (v : V), OddBalance.obstruction (W.interaction hmin) choice v = 0) (v : V) : ∑ u ∈ Finset.univ.erase v, W.orderedLetterInteraction (W.chosenDifference hmin choice) v u = 0

theorem Sabidussi.CyclicWord.Word.quadratic_prefix_pair {V : Type u_1} (W : Word) (y : W.Pos → Color) (htotal : ∑ i : W.Pos, y i = 0) (i : W.Pos) : quadratic (W.prefixColor y (W.prev i)) + quadratic (W.prefixColor y i) = quadratic (y i) + bracket (y i) (W.prefixColor y (W.prev i))

theorem Sabidussi.CyclicWord.Word.quadratic_incident_sum_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (W : Word) (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (choice : V → Fin 3) (hbalanced : ∀ (v : V), OddBalance.obstruction (W.interaction hmin) choice v = 0) (v : V) : have y := W.chosenDifference hmin choice; have x := W.prefixColor y; ∑ os : W.Occurrence v × Fin 2, quadratic (W.incidentColor x os.1 os.2) = 0

The balanced interaction equations are exactly the missing quadratic moment at each letter.

theorem Sabidussi.CyclicWord.Word.incident_sum_eq_zero {V : Type u_1} [DecidableEq V] (W : Word) [Finite V] (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) (choice : V → Fin 3) (v : V) : have y := W.chosenDifference hmin choice; have x := W.prefixColor y; ∑ os : W.Occurrence v × Fin 2, W.incidentColor x os.1 os.2 = 0

theorem Sabidussi.CyclicWord.Word.exists_coloring {V : Type u_1} [DecidableEq V] (W : Word) [Finite V] (hmin : ∀ (v : V), 2 ≤ Fintype.card (W.Occurrence v)) : Nonempty W.Coloring

Every nonempty cyclic word in which each letter occurs at least twice has the required four-colouring of its gaps.