Subcubic Brooks theorem: CutVertex

Part of the proof that a finite subcubic K₄-free graph is three-colourable.

def BrooksSubcubic.IsCutVertex {V : Type u_1} (G : SimpleGraph V) (x : V) : Prop

x is a cut vertex of G when deleting it disconnects G.

Equations

• BrooksSubcubic.IsCutVertex G x = ¬(SimpleGraph.induce {x}ᶜ G).Connected

theorem BrooksSubcubic.exists_unreachable_of_cutVertex {V : Type u_1} (G : SimpleGraph V) (x w : V) (hw : w ≠ x) (hcut : IsCutVertex G x) : ∃ (d : V) (e : V) (hd : d ≠ x) (he : e ≠ x), ¬(SimpleGraph.induce {x}ᶜ G).Reachable ⟨d, hd⟩ ⟨e, he⟩

A cut vertex with nonempty complement yields two mutually unreachable vertices.

theorem BrooksSubcubic.exists_unreachable_of_notConnected {V : Type u_1} (G : SimpleGraph V) (S : Set V) (w : V) (hw : w ∉ S) (hdis : ¬(SimpleGraph.induce Sᶜ G).Connected) : ∃ (d : V) (e : V) (hd : d ∉ S) (he : e ∉ S), ¬(SimpleGraph.induce Sᶜ G).Reachable ⟨d, hd⟩ ⟨e, he⟩

If deleting a set S disconnects G (and Sᶜ is nonempty via w ∉ S), there are two vertices outside S that are mutually unreachable in G − S. The 2-cut case S = {a₀, y} feeds the endblock analysis of Lovász Case 2.

theorem BrooksSubcubic.class_touches_cut {V : Type u_1} (G : SimpleGraph V) (hconn : G.Connected) (S : Set V) {d : V} (hd : d ∉ S) {s0 : V} (hs0 : s0 ∈ S) : ∃ (w : ↑Sᶜ), ∃ s ∈ S, G.Adj (↑w) s ∧ (SimpleGraph.induce Sᶜ G).connectedComponentMk w = (SimpleGraph.induce Sᶜ G).connectedComponentMk ⟨d, hd⟩

Component touches the cut. In a connected G, for any separating set S (nonempty, witness s0 ∈ S) and any d ∉ S, the G−S-component of d contains a vertex adjacent to some cut vertex s ∈ S. (Else that component is closed under all G-adjacency, hence unreachable from S, contradicting connectedness.) With S = {a₀, y} this says every component of G−{a₀,y} touches a₀ or y — the entry point to Lovász's endblock analysis.

theorem BrooksSubcubic.a0_adj_component {V : Type u_1} (G : SimpleGraph V) {a0 y : V} (hay : a0 ≠ y) (hHconn : (SimpleGraph.induce {y}ᶜ G).Connected) {d : V} (hd : d ∈ {a0, y}ᶜ) : ∃ (z : V) (hz : z ∈ {a0, y}ᶜ), G.Adj a0 z ∧ (SimpleGraph.induce {a0, y}ᶜ G).connectedComponentMk ⟨d, hd⟩ = (SimpleGraph.induce {a0, y}ᶜ G).connectedComponentMk ⟨z, hz⟩

a₀ reaches every component of G−{a₀,y}. If G−y is connected and a₀ ≠ y, then for every d ∉ {a₀,y}, a₀ has a neighbour in d's G−{a₀,y}-component. (In H = G−y, a₀ is a cut vertex and every component of H−a₀ = G−{a₀,y} hangs off a₀.) This yields the candidate pair a,b ∈ N(a₀) in two distinct components for Lovász Case 2.

theorem BrooksSubcubic.exists_cut_candidate_pair {V : Type u_1} (G : SimpleGraph V) {a0 y : V} (hay : a0 ≠ y) (hHy : (SimpleGraph.induce {y}ᶜ G).Connected) (w : V) (hw : w ∉ {a0, y}) (hcut : ¬(SimpleGraph.induce {a0, y}ᶜ G).Connected) : ∃ (a : V) (b : V), G.Adj a0 a ∧ G.Adj a0 b ∧ a ≠ b ∧ ¬G.Adj a b

Candidate pair for Lovász Case 2. If {a₀,y} is a 2-cut (G−{a₀,y} disconnected, witnessed by w ∉ {a₀,y}) and G−y is connected, then a₀ has two neighbours a,b in distinct G−{a₀,y}-components — hence a ≠ b and ¬ G.Adj a b. Everything of Lovász Case 2 except G−{a,b} connected (the leaf/non-cut refinement).