Subcubic Brooks theorem: CandidatePair

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

theorem BrooksSubcubic.exists_dist2_pair {V : Type u_1} (G : SimpleGraph V) (hconn : G.Connected) {x w : V} (hwx : w ≠ x) (hxw : ¬G.Adj x w) : ∃ (u : V) (b : V), G.Adj x u ∧ G.Adj u b ∧ ¬G.Adj x b ∧ b ≠ x

P2 (distance-2 candidate). In a connected G, if x has a non-neighbour w ≠ x, then x has a neighbour u which has a neighbour b with ¬ G.Adj x b and b ≠ x. (I.e. a vertex b at distance 2 from x, with common neighbour u.) Proof: the set {x} ∪ N(x) is not closed under adjacency (it omits w yet x reaches w), so some neighbour of x has an edge leaving it.

theorem BrooksSubcubic.exists_nonneighbor_of_ne_top {V : Type u_1} (G : SimpleGraph V) (hne : G ≠ ⊤) : ∃ (x : V) (w : V), w ≠ x ∧ ¬G.Adj x w

G ≠ ⊤ ⇒ some vertex has a non-neighbour (≠ itself).

theorem BrooksSubcubic.exists_candidate_of_ne_top {V : Type u_1} (G : SimpleGraph V) (hconn : G.Connected) (hne : G ≠ ⊤) : ∃ (v₀ : V) (a : V) (b : V), G.Adj v₀ a ∧ G.Adj v₀ b ∧ a ≠ b ∧ ¬G.Adj a b

Reduction of the bad-graph lemma to its kernel. Contrapositive shape: if G is connected, G ≠ ⊤, and G has no good triple, then every good-triple candidate (v₀,a,b) has G−{a,b} disconnected. In particular a candidate exists (via exists_dist2_pair), so the residual content is purely: "every distance-2 pair is a 2-cut ⇒ G is 2-regular".