Subcubic Brooks theorem: CubicColouring

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

def BrooksSubcubic.deleteStar {V : Type u_1} (G : SimpleGraph V) (v₀ : V) : SimpleGraph V

G with all edges incident to v₀ removed (same vertex set).

Equations

• BrooksSubcubic.deleteStar G v₀ = G.deleteIncidenceSet v₀

theorem BrooksSubcubic.deleteStar_adj {V : Type u_1} (G : SimpleGraph V) (v₀ x y : V) : (deleteStar G v₀).Adj x y ↔ G.Adj x y ∧ x ≠ v₀ ∧ y ≠ v₀

Adjacency in the graph with the edges at v₀ removed.

@[instance_reducible]

instance BrooksSubcubic.instDecidableRelAdjDeleteStar {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v₀ : V) : DecidableRel (deleteStar G v₀).Adj

Equations

• BrooksSubcubic.instDecidableRelAdjDeleteStar G v₀ x y = decidable_of_iff (G.Adj x y ∧ x ≠ v₀ ∧ y ≠ v₀) ⋯

theorem BrooksSubcubic.deleteStar_neighborFinset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v₀ x : V) (hx : x ≠ v₀) : (deleteStar G v₀).neighborFinset x = (G.neighborFinset x).erase v₀

Neighbours of x ≠ v₀ in deleteStar G v₀ are exactly N_G(x) with v₀ erased.

theorem BrooksSubcubic.exists_brooks_rank_of_descent {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v₀ a b : V) (hab : a ≠ b) (hnadj : ¬G.Adj a b) (hva : G.Adj v₀ a) (hvb : G.Adj v₀ b) (hreg : ∀ (v : V), G.degree v = 3) (lvl : V → ℕ) (hlvl_lt : ∀ (x : V), lvl x < Fintype.card V) (hdesc : ∀ (u : V), u ≠ v₀ → u ≠ a → u ≠ b → ¬G.Adj v₀ u → ∃ (w : V), G.Adj u w ∧ w ≠ v₀ ∧ w ≠ a ∧ w ≠ b ∧ lvl w < lvl u) : ∃ (rank : V → ℕ), Function.Injective rank ∧ (∀ (u : V), {w ∈ (deleteStar G v₀).neighborFinset u | rank w < rank u}.card < 3) ∧ {w ∈ (deleteStar G v₀).neighborFinset a | rank w < rank a}.card = 0 ∧ {w ∈ (deleteStar G v₀).neighborFinset b | rank w < rank b}.card = 0

A2 (rank from a descent function). Given v₀ with non-adjacent neighbours a,b, a 3-regular G, and a level function lvl (think: BFS distance in G−{a,b} from v₀) with lvl x < |V| and the descent property (every non-v₀ non-neighbour of v₀, other than a,b, has a G-neighbour ≠ v₀,a,b of strictly smaller level), there is an injective rank giving the deleteStar G v₀ greedy conditions with a,b as sinks. This is the crux-INDEPENDENT mechanical core of the Lovász ordering; producing lvl from 2-connectivity is the (A1) kernel.

theorem BrooksSubcubic.colorable_of_good_triple {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v₀ a b : V) (hreg : ∀ (v : V), G.degree v = 3) (hva : G.Adj v₀ a) (hvb : G.Adj v₀ b) (hab : a ≠ b) (hnadj : ¬G.Adj a b) (hgood : (SimpleGraph.induce {a, b}ᶜ G).Connected) : G.Colorable 3

A1 completion: good triple ⇒ 3-colourable. If v₀ has non-adjacent neighbours a,b with G−{a,b} (the induced subgraph on {a,b}ᶜ) connected, then G is 3-colourable: BFS from v₀ in G−{a,b} yields a level function whose descent feeds exists_brooks_rank_of_descent (A2); colour-controlled greedy gives c(a)=c(b)=0, so v₀ sees ≤2 colours and a free colour extends the colouring. The (A1) kernel — the BFS level construction — is carried out below from the graph distance in G−{a,b}, so this theorem is proved unconditionally (no gap remains).

theorem BrooksSubcubic.colorable_three_cubic_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) : G.Colorable 3

B (reduction, non-2-connected case). A connected cubic K₄-free graph with no good triple has a cut vertex and is three-colourable by a cut-vertex/block reduction. The mechanical and structural halves are fully proved by hand: colorable_of_cut_partition (each component-plus-x has x at degree < 3, so the non-regular case colours it, and colorable_glue_at_vertex merges at x), with Lovász cut-existence providing the cut witness from ¬ ∃ good triple.

theorem BrooksSubcubic.connected_colorable_three_of_degree_eq_three {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) : G.Colorable 3

B8 (3-regular case). A connected 3-regular graph with no 4-clique is 3-colourable. Case split on the existence of a Lovász "good triple" (v₀,a,b) with G−{a,b} connected: present ⇒ colorable_of_good_triple (A1); absent ⇒ colorable_three_cubic_no_good_triple (B).