Local difference patterns

For every number n + 2 of transition occurrences we construct three admissible local patterns. The construction is the degree-splitting step of the manuscript written without changing the graph: remove pairs of occurrences recursively, ending with a pair or a triple.

def Sabidussi.choiceColor (c : Fin 3) : Color

A fixed enumeration of the three nonzero colours.

Equations

• Sabidussi.choiceColor c = Sabidussi.tripleDifference (1, 0) c

theorem Sabidussi.choiceColor_ne_zero (c : Fin 3) : choiceColor c ≠ 0

theorem Sabidussi.sum_choiceColor : ∑ c : Fin 3, choiceColor c = 0

theorem Sabidussi.sum_tripleDifference_choice (i : Fin 3) : ∑ c : Fin 3, tripleDifference (choiceColor c) i = 0

def Sabidussi.localDifference (n : ℕ) : Fin 3 → Fin (n + 2) → Color

Three local patterns on n + 2 occurrences. For 2 occurrences the difference is constant; for 3 it is the anisotropic triple; every additional pair receives the same nonzero colour and is then removed recursively.

Equations

• One or more equations did not get rendered due to their size.
• Sabidussi.localDifference 0 x✝ = Sabidussi.doubleDifference (Sabidussi.choiceColor x✝)
• Sabidussi.localDifference 1 x✝ = Sabidussi.tripleDifference (Sabidussi.choiceColor x✝)

@[simp]

theorem Sabidussi.localDifference_zero (c : Fin 3) : localDifference 0 c = doubleDifference (choiceColor c)

@[simp]

theorem Sabidussi.localDifference_one (c : Fin 3) : localDifference 1 c = tripleDifference (choiceColor c)

theorem Sabidussi.localDifference_ne_zero (n : ℕ) (c : Fin 3) (i : Fin (n + 2)) : localDifference n c i ≠ 0

theorem Sabidussi.sum_localDifference_occurrences (n : ℕ) (c : Fin 3) : ∑ i : Fin (n + 2), localDifference n c i = 0

theorem Sabidussi.sum_localDifference_choices (n : ℕ) (i : Fin (n + 2)) : ∑ c : Fin 3, localDifference n c i = 0