LeanPool.TwoColoringOneRound.LowerBound.LocalRule

def Distributed2Coloring.LowerBound.LocalRule.g : Bool → Bool → Bool → Bool

Local rule from the report: g(0,0,0)=1, g(1,1,1)=0, otherwise g(x,y,z)=y.

Equations

• Distributed2Coloring.LowerBound.LocalRule.g false false false = true
• Distributed2Coloring.LowerBound.LocalRule.g true true true = false
• Distributed2Coloring.LowerBound.LocalRule.g x✝² x✝¹ x✝ = x✝¹

theorem Distributed2Coloring.LowerBound.LocalRule.g_eq_iff_patterns (x y z w : Bool) : g x y z = g y z w ↔ x = false ∧ y = false ∧ z = false ∧ w = false ∨ x = true ∧ y = true ∧ z = true ∧ w = true ∨ x = true ∧ y = false ∧ z = false ∧ w = true ∨ x = false ∧ y = true ∧ z = true ∧ w = false

theorem Distributed2Coloring.LowerBound.LocalRule.monochromatic_iff_patterns {n : ℕ} {two : Sym n} (round : Sym n → Bool) (hr_true : ∀ (a : Sym n), round a = true ↔ two ≤ a) (hr_false : ∀ (a : Sym n), round a = false ↔ a < two) (e : Edge n) : Edge.monochromatic (fun (v : Vertex n) => g (round v.a) (round v.b) (round v.c)) e ↔ EdgePatterns.Pat0000 two e ∨ EdgePatterns.Pat1111 two e ∨ EdgePatterns.Pat1001 two e ∨ EdgePatterns.Pat0110 two e