Monochromatic-edge propagation (Lemma 2.1)

The graph argument concerns possible rounds, independently of numerical weights. A monochromatic edge supplies a color that can be kept while its region grows.

def Voter.Possible {V : Type u_1} {C : Type u_2} (G : SimpleGraph V) (s t : Config V C) : Prop

A possible simultaneous copying round on a graph.

Equations

• Voter.Possible G s t = ∃ (r : V → V), (∀ (i : V), G.Adj i (r i)) ∧ Voter.step s r = t

theorem Voter.monochromatic_edge {V : Type u_1} (G : SimpleGraph V) (hn : ¬G.Colorable 2) (s : Config V Bool) : ∃ (i : V) (j : V), G.Adj i j ∧ s i = s j

A nonbipartite graph has a monochromatic edge in every Boolean configuration.

theorem Voter.boundary_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (hc : G.Connected) (S : Finset V) (hne : S.Nonempty) (hproper : S ≠ Finset.univ) : ∃ i ∈ S, ∃ j ∉ S, G.Adj i j

Every nonempty proper vertex set in a connected graph has an edge leaving it.

theorem Voter.propagate_region {V : Type u_1} {C : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (hc : G.Connected) (neighbors : ∀ (i : V), ∃ (j : V), G.Adj i j) (s : Config V C) (S : Finset V) (c : C) (hne : S.Nonempty) (hcolor : ∀ i ∈ S, s i = c) (hinternal : ∀ i ∈ S, ∃ j ∈ S, G.Adj i j) : Relation.ReflTransGen (Possible G) s fun (x : V) => c

A monochromatic region with an internal neighbor at each vertex can grow to consensus along a finite sequence of possible rounds.

theorem Voter.possible_consensus {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (hc : G.Connected) (hn : ¬G.Colorable 2) (neighbors : ∀ (i : V), ∃ (j : V), G.Adj i j) (s : Config V Bool) : ∃ (c : Bool), Relation.ReflTransGen (Possible G) s fun (x : V) => c

Every Boolean configuration can reach consensus on a connected nonbipartite graph.