Subcubic Brooks theorem: CutColouring

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

theorem BrooksSubcubic.induce_degree_le {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Set V) [DecidablePred fun (x : V) => x ∈ S] [DecidableRel (SimpleGraph.induce S G).Adj] (w : ↑S) : (SimpleGraph.induce S G).degree w ≤ G.degree ↑w

Induced degree never exceeds the ambient degree.

theorem BrooksSubcubic.colorable_of_cut_partition {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hreg : ∀ (v : V), G.degree v = 3) (x : V) (A₀ B₀ : Finset V) (hAne : A₀.Nonempty) (hBne : B₀.Nonempty) (hxnA : x ∉ A₀) (hxnB : x ∉ B₀) (hdisj : Disjoint A₀ B₀) (hcov : insert x (A₀ ∪ B₀) = Finset.univ) (hnocross : ∀ a ∈ A₀, ∀ b ∈ B₀, ¬G.Adj a b) (hAconn : (SimpleGraph.induce (↑(insert x A₀)) G).Connected) (hBconn : (SimpleGraph.induce (↑(insert x B₀)) G).Connected) : G.Colorable 3

B, cut-vertex reduction (structural half). Given a 3-regular G, a vertex x, and a partition of V∖{x} into nonempty A₀,B₀ with no edge crossing between them, such that both G[{x}∪A₀] and G[{x}∪B₀] are connected, G is 3-colourable: each side has x at degree < 3 (it has a neighbour on the other side), so the non-regular case colours it, and the glue lemma merges them at x. This discharges everything downstream of the Lovász cut-existence step.