Chromatic number of wheel-free graphs

DefinitionInduced wheels#✓fully proved

A simple graph \(G\) has an induced wheel if there are a natural number \(\ell \ge 4\), distinct vertices \(r_0, \dots, r_{\ell-1}\) of \(G\) (the rim) and a vertex \(h\) of \(G\) (the hub) with \(h \ne r_i\) for every \(i\), such that for all \(i, j < \ell\) the vertices \(r_i\) and \(r_j\) are adjacent in \(G\) exactly when \(i - j \equiv \pm 1 \pmod{\ell}\), and \(h\) is adjacent to \(r_i\), \(r_j\) and \(r_k\) for some pairwise distinct \(i, j, k < \ell\). The hub may have further neighbours on the rim.

def hasInducedWheel {V : Type*} (G : SimpleGraph V) : Prop :=
  ∃ (ℓ : ℕ) (rim : Fin ℓ ↪ V) (hub : V),
    4 ≤ ℓ ∧
    (∀ i : Fin ℓ, rim i ≠ hub) ∧
    (∀ i j : Fin ℓ, G.Adj (rim i) (rim j) ↔ (SimpleGraph.cycleGraph ℓ).Adj i j) ∧
    ∃ i j k : Fin ℓ, i ≠ j ∧ j ≠ k ∧ k ≠ i ∧
      G.Adj hub (rim i) ∧ G.Adj hub (rim j) ∧ G.Adj hub (rim k)

Sources

• James Davies, Triangle-free graphs with large chromatic number and no induced wheel, arXiv:2104.05907v3, page 1, defining paragraph, https://arxiv.org/pdf/2104.05907v3.

Used by 1

Used byWheel-free graphs

DefinitionWheel-free graphs#✓fully proved

A simple graph \(G\) is wheel-free if it has no induced wheel, that is, no induced cycle of length at least four together with a vertex outside the cycle that is adjacent to at least three vertices of the cycle.

def wheelFree {V : Type*} (G : SimpleGraph V) : Prop := ¬ hasInducedWheel G

Sources

• James Davies, arXiv:2104.05907v3, page 1, wheel definition, https://arxiv.org/pdf/2104.05907v3.

Uses 1 · Used by 1

Statement usesInduced wheels

Used byTriangle-free wheel-free graphs of large chromatic number (proposition)

DefinitionTriangle-free wheel-free graphs of large chromatic number (proposition)#✓fully proved

This is the proposition that for every positive integer \(k\) there are a natural number \(n\) and a simple graph \(G\) on the vertex set \(\{0, \dots, n - 1\}\) such that \(G\) contains no triangle, \(G\) is wheel-free (it has no induced wheel) and the chromatic number of \(G\) is at least \(k\).

Since \(G\) is finite, its chromatic number is finite.

def largeChromaticTriangleFreeWheelFree : Prop :=
  ∀ k : ℕ, 0 < k → ∃ (n : ℕ) (G : SimpleGraph (Fin n)),
    G.CliqueFree 3 ∧ wheelFree G ∧ (k : ℕ∞) ≤ G.chromaticNumber

Sources

• Davies, arXiv:2104.05907v3, Corollary 2, page 1; the finite constructions are given on pages 5 and 6, https://arxiv.org/pdf/2104.05907v3.

Uses 1 · Used by 1

Statement usesWheel-free graphs

Used byDavies's theorem on triangle-free wheel-free graphs

TheoremDavies's theorem on triangle-free wheel-free graphs#●ready to prove

For every positive integer \(k\) there are a natural number \(n\) and a simple graph \(G\) on the vertex set \(\{0, \dots, n - 1\}\) such that \(G\) contains no triangle, \(G\) is wheel-free (it has no induced wheel) and the chromatic number of \(G\) is at least \(k\).

public theorem_wanted largeChromaticTriangleFreeWheelFree_holds :
    largeChromaticTriangleFreeWheelFree

Sources

• James Davies, arXiv:2104.05907v3, Corollary 2, page 1, https://arxiv.org/pdf/2104.05907v3.

Uses 1

Statement usesTriangle-free wheel-free graphs of large chromatic number (proposition)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.