Subcubic Brooks theorem: GoodTriple

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

theorem BrooksSubcubic.next_cut_candidate {V : Type u_1} (G : SimpleGraph V) (hdel : ∀ (x : V), (SimpleGraph.induce {x}ᶜ G).Connected) (v a b : V) (hva : G.Adj v a) (hvb : G.Adj v b) (hab : a ≠ b) (hcut : ¬(SimpleGraph.induce {a, b}ᶜ G).Connected) : ∃ (c : V) (d : V), G.Adj a c ∧ G.Adj a d ∧ c ≠ d ∧ ¬G.Adj c d

A bad induced path can be moved across its first endpoint: deleting its endpoints gives a 2-cut, and exists_cut_candidate_pair supplies a new induced path centred at that endpoint.

theorem BrooksSubcubic.good_triple_of_all_vertex_deletions_connected {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) (hreg : ∀ (v : V), G.degree v = 3) (hK4 : G.CliqueFree 4) (hdel : ∀ (x : V), (SimpleGraph.induce {x}ᶜ G).Connected) : ∃ (v₀ : V) (a : V) (b : V), G.Adj v₀ a ∧ G.Adj v₀ b ∧ a ≠ b ∧ ¬G.Adj a b ∧ (SimpleGraph.induce {a, b}ᶜ G).Connected

Contrapositive form of the Lovász lemma specialized to cubic K₄-free graphs.

theorem BrooksSubcubic.cut_witness_of_no_good_triple {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) (hreg : ∀ (v : V), G.degree v = 3) (hK4 : G.CliqueFree 4) (hng : ¬∃ (v₀ : V) (a : V) (b : V), G.Adj v₀ a ∧ G.Adj v₀ b ∧ a ≠ b ∧ ¬G.Adj a b ∧ (SimpleGraph.induce {a, b}ᶜ G).Connected) : ∃ (x : V) (d : V) (e : V) (hd : d ≠ x) (he : e ≠ x), ¬(SimpleGraph.induce {x}ᶜ G).Reachable ⟨d, hd⟩ ⟨e, he⟩

Lovász cut-existence step. A connected cubic K₄-free graph with no good triple has a cut vertex, presented directly by two unreachable vertices after deletion.