Five-wheel like graphs

This file defines an IsFiveWheelLike structure in a graph, and describes properties of these structures as well as graphs which avoid this structure. These have two key uses:

• We use them to prove that a maximally Kᵣ₊₁-free graph is r-colorable iff it is complete-multipartite: colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree.
• They play a key role in Brandt's proof of the Andrásfai-Erdős-Sós theorem, which is where they first appeared. We give this proof below, see colorable_of_cliqueFree_lt_minDegree.

If G is maximally Kᵣ₊₂-free and ¬ G.Adj x y (with x ≠ y) then there exists an r-set s such that s ∪ {x} and s ∪ {y} are both r + 1-cliques.

If ¬ G.IsCompleteMultipartite then it contains a G.IsPathGraph3Compl v w₁ w₂ consisting of an edge w₁w₂ and a vertex v such that vw₁ and vw₂ are non-edges.

Hence any maximally Kᵣ₊₂-free graph that is not complete-multipartite must contain distinct vertices v, w₁, w₂, together with r-sets s and t, such that {v, w₁, w₂} induces the single edge w₁w₂, s ∪ t is disjoint from {v, w₁, w₂}, and s ∪ {v}, t ∪ {v}, s ∪ {w₁} and t ∪ {w₂} are all r + 1-cliques.

This leads to the definition of an IsFiveWheelLike structure which can be found in any maximally Kᵣ₊₂-free graph that is not complete-multipartite (see exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite).

One key parameter in any such structure is the number of vertices common to all of the cliques: we denote this quantity by k = #(s ∩ t) (and we will refer to such a structure as Wᵣ,ₖ below.)

The first interesting cases of such structures are W₁,₀ and W₂,₁: W₁,₀ is a 5-cycle, while W₂,₁ is a 5-cycle with an extra central hub vertex adjacent to all other vertices (i.e. W₂,₁ resembles a wheel with five spokes).

             `W₁,₀`       v                 `W₂,₁`      v
                       /     \                       /  |  \
                      s       t                     s ─ u ─ t
                       \     /                       \ / \ /
                       w₁ ─ w₂                       w₁ ─ w₂

Main definitions

• SimpleGraph.IsFiveWheelLike: predicate for v w₁ w₂ s t to form a 5-wheel-like subgraph of G with r-sets s and t, and vertices v w₁ w₂ forming an IsPathGraph3Compl and #(s ∩ t) = k.

• SimpleGraph.FiveWheelLikeFree: predicate for G to have no IsFiveWheelLike r k subgraph.

Implementation notes

The definitions of IsFiveWheelLike and IsFiveWheelLikeFree in this file have r shifted by two compared to the definitions in Brandt On the structure of graphs with bounded clique number

The definition of IsFiveWheelLike does not contain the facts that #s = r and #t = r but we deduce these later as card_left and card_right.

Although #(s ∩ t) can easily be derived from s and t we include the IsFiveWheelLike field card_inter : #(s ∩ t) = k to match the informal / paper definitions and to simplify some statements of results and match our definition of IsFiveWheelLikeFree.

The vertex set of an IsFiveWheel structure Wᵣ,ₖ is {v, w₁, w₂} ∪ s ∪ t : Finset α. We will need to refer to this consistently and choose the following formulation: {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) which is definitionally equal to insert v <| insert w₁ <| insert w₂ <| s ∪ t.

References

• B. Andrasfái, P Erdős, V. T. Sós On the connection between chromatic number, maximal clique, and minimal degree of a graph https://doi.org/10.1016/0012-365X(74)90133-2

• S. Brandt On the structure of graphs with bounded clique number https://doi.org/10.1007/s00493-003-0042-z

structure SimpleGraph.IsFiveWheelLike {α : Type u_1} [DecidableEq α] (G : SimpleGraph α) (r k : ℕ) (v w₁ w₂ : α) (s t : Finset α) : Prop

An IsFiveWheelLike r k v w₁ w₂ s t structure in G consists of vertices v w₁ w₂ and r-sets s and t such that {v, w₁, w₂} induces the single edge w₁w₂ (i.e. they form an IsPathGraph3Compl), v, w₁, w₂ ∉ s ∪ t, s ∪ {v}, t ∪ {v}, s ∪ {w₁}, t ∪ {w₂} are all (r + 1)- cliques and #(s ∩ t) = k. (If G is maximally (r + 2)-cliquefree and not complete multipartite then G will contain such a structure : see exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite.)

• isPathGraph3Compl : G.IsPathGraph3Compl v w₁ w₂

  {v, w₁, w₂} induces the single edge w₁w₂

• notMem_left : v ∉ s
• notMem_right : v ∉ t
• fst_notMem : w₁ ∉ s
• snd_notMem : w₂ ∉ t
• isNClique_left : G.IsNClique (r + 1) (insert v s)
• isNClique_fst_left : G.IsNClique (r + 1) (insert w₁ s)
• isNClique_right : G.IsNClique (r + 1) (insert v t)
• isNClique_snd_right : G.IsNClique (r + 1) (insert w₂ t)
• card_inter : (s ∩ t).card = k

theorem SimpleGraph.exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite {α : Type u_1} {G : SimpleGraph α} {r : ℕ} [DecidableEq α] (h : Maximal (fun (H : SimpleGraph α) => H.CliqueFree (r + 2)) G) (hnc : ¬G.IsCompleteMultipartite) : ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (s ∩ t).card v w₁ w₂ s t

def SimpleGraph.FiveWheelLikeFree {α : Type u_1} [DecidableEq α] (G : SimpleGraph α) (r k : ℕ) : Prop

G.FiveWheelLikeFree r k means there is no IsFiveWheelLike r k structure in G.

Equations

• G.FiveWheelLikeFree r k = ∀ {v w₁ w₂ : α} {s t : Finset α}, ¬G.IsFiveWheelLike r k v w₁ w₂ s t

theorem SimpleGraph.IsFiveWheelLike.symm {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [DecidableEq α] {v w₁ w₂ : α} {t : Finset α} (hw : G.IsFiveWheelLike r k v w₁ w₂ s t) : G.IsFiveWheelLike r k v w₂ w₁ t s

theorem SimpleGraph.IsFiveWheelLike.fst_notMem_right {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [DecidableEq α] {v w₁ w₂ : α} {t : Finset α} (hw : G.IsFiveWheelLike r k v w₁ w₂ s t) : w₁ ∉ t

theorem SimpleGraph.IsFiveWheelLike.snd_notMem_left {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [DecidableEq α] {v w₁ w₂ : α} {t : Finset α} (hw : G.IsFiveWheelLike r k v w₁ w₂ s t) : w₂ ∉ s

theorem SimpleGraph.IsFiveWheelLike.not_colorable_succ {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [DecidableEq α] {v w₁ w₂ : α} {t : Finset α} (hw : G.IsFiveWheelLike r k v w₁ w₂ s t) : ¬G.Colorable (r + 1)

Any graph containing an IsFiveWheelLike r k structure is not (r + 1)-colorable.

theorem SimpleGraph.IsFiveWheelLike.card_left {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [DecidableEq α] {v w₁ w₂ : α} {t : Finset α} (hw : G.IsFiveWheelLike r k v w₁ w₂ s t) : s.card = r

theorem SimpleGraph.IsFiveWheelLike.card_right {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [DecidableEq α] {v w₁ w₂ : α} {t : Finset α} (hw : G.IsFiveWheelLike r k v w₁ w₂ s t) : t.card = r

theorem SimpleGraph.IsFiveWheelLike.card_inter_lt_of_cliqueFree {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [DecidableEq α] {v w₁ w₂ : α} {t : Finset α} (hw : G.IsFiveWheelLike r k v w₁ w₂ s t) (h : G.CliqueFree (r + 2)) : k < r

theorem SimpleGraph.exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite {α : Type u_1} {G : SimpleGraph α} {r : ℕ} [DecidableEq α] (h : Maximal (fun (H : SimpleGraph α) => H.CliqueFree (r + 2)) G) (hnc : ¬G.IsCompleteMultipartite) : ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j

Any maximally Kᵣ₊₂-free graph that is not complete-multipartite contains a maximal IsFiveWheelLike structure Wᵣ,ₖ for some k < r. (It is maximal in terms of k.)

theorem SimpleGraph.CliqueFree.fiveWheelLikeFree_of_le {α : Type u_1} {G : SimpleGraph α} {r k : ℕ} [DecidableEq α] (h : G.CliqueFree (r + 2)) (hk : r ≤ k) : G.FiveWheelLikeFree r k

theorem SimpleGraph.colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree {α : Type u_1} {G : SimpleGraph α} {r : ℕ} [DecidableEq α] (h : Maximal (fun (H : SimpleGraph α) => H.CliqueFree (r + 1)) G) : G.Colorable r ↔ G.IsCompleteMultipartite

A maximally Kᵣ₊₁-free graph is r-colorable iff it is complete-multipartite.

theorem SimpleGraph.IsFiveWheelLike.exists_isFiveWheelLike_succ_of_not_adj_le_two {α : Type u_1} {G : SimpleGraph α} {r k : ℕ} {x v w₁ w₂ : α} {s t : Finset α} [DecidableEq α] (hw : G.IsFiveWheelLike r k v w₁ w₂ s t) (hcf : G.CliqueFree (r + 2)) [DecidableRel G.Adj] (hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y) (h2 : {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}.card ≤ 2) : ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))

If G is Kᵣ₊₂-free and contains a Wᵣ,ₖ together with a vertex x adjacent to all but at most two vertices of Wᵣ,ₖ, including all of its common clique vertices, then G contains a Wᵣ,ₖ₊₁.

theorem SimpleGraph.IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ {α : Type u_1} {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α} [DecidableEq α] (hw : G.IsFiveWheelLike r k v w₁ w₂ s t) (hcf : G.CliqueFree (r + 2)) [DecidableRel G.Adj] [Fintype α] (hm : G.FiveWheelLikeFree r (k + 1)) : G.minDegree ≤ (2 * r + k) * Fintype.card α / (2 * r + k + 3)

If G is a Kᵣ₊₂-free graph with n vertices containing a Wᵣ,ₖ but no Wᵣ,ₖ₊₁ then G.minDegree ≤ (2 * r + k) * n / (2 * r + k + 3)

theorem SimpleGraph.colorable_of_cliqueFree_lt_minDegree {α : Type u_1} {G : SimpleGraph α} {r : ℕ} [DecidableEq α] [Fintype α] [DecidableRel G.Adj] (hf : G.CliqueFree (r + 1)) (hd : (3 * r - 4) * Fintype.card α / (3 * r - 1) < G.minDegree) : G.Colorable r

Andrasfái-Erdős-Sós theorem

If G is a Kᵣ₊₁-free graph with n vertices and (3 * r - 4) * n / (3 * r - 1) < G.minDegree then G is r + 1-colorable, e.g. if G is K₃-free and 2 * n / 5 < G.minDegree then G is 2-colorable.