Generalized Ramsey numbers

Definition\((4, 5)\)-colourings of \(K_n\)#✓fully proved

For natural numbers \(n\) and \(k\), the complete graph \(K_n\) on the vertices \(0, 1, \dots, n - 1\) has a \((4, 5)\)-colouring with \(k\) colours if there is a map \(c\) assigning to every ordered pair \((x, y)\) of vertices one of \(k\) colours, with \(c(x, y) = c(y, x)\) for all \(x, y\), such that for any four distinct vertices the six edges between them receive at least five distinct colours.

def HasFourFiveColouring (n k : ℕ) : Prop :=
  ∃ c : Fin n → Fin n → Fin k, (∀ x y, c x y = c y x) ∧ ∀ v : Fin 4 ↪ Fin n,
    5 ≤ ((Finset.univ : Finset (Fin 4)).offDiag.image fun q => c (v q.1) (v q.2)).card

Used by 1

Used byThe \((4, 5)\)-colouring number \(f(n)\)

DefinitionThe \((4, 5)\)-colouring number \(f(n)\)#✓fully proved

For a natural number \(n\), \(f(n)\) is the least natural number \(k\) such that \(K_n\) has a \((4, 5)\)-colouring with \(k\) colours; such a \(k\) always exists.

noncomputable def fourFiveColourNumber (n : ℕ) : ℕ :=
  sInf {k : ℕ | HasFourFiveColouring n k}

def HasFourFiveColouring (n k : ℕ) : Prop :=
  ∃ c : Fin n → Fin n → Fin k, (∀ x y, c x y = c y x) ∧ ∀ v : Fin 4 ↪ Fin n,
    5 ≤ ((Finset.univ : Finset (Fin 4)).offDiag.image fun q => c (v q.1) (v q.2)).card

WantedExt/Combinatorics/FourCliqueFiveColoursErdosProblem136Wanted.lean:39

Uses 1 · Used by 1

Statement uses\((4, 5)\)-colourings of \(K_n\)

Used byThe asymptotic of the \((4, 5)\)-colouring number (Erdős Problem 136)

DefinitionThe asymptotic of the \((4, 5)\)-colouring number (Erdős Problem 136)#✓fully proved

Let \(f(n)\) be the least number of colours in a \((4, 5)\)-colouring of \(K_n\). This is the proposition that \(f(n)/n\) tends to \(5/6\) as \(n \to \infty\); equivalently, \(f(n) = (5/6 + o(1))\, n\).

def fourFiveColourNumberAsymptotic : Prop :=
  Tendsto (fun n : ℕ => (fourFiveColourNumber n : ℝ) / n) atTop (nhds (5 / 6))

Uses 1 · Used by 1

Statement usesThe \((4, 5)\)-colouring number \(f(n)\)

Used byErdős Problem 136: the \((4, 5)\)-colouring number of \(K_n\) is asymptotically \(5n/6\)

TheoremErdős Problem 136: the \((4, 5)\)-colouring number of \(K_n\) is asymptotically \(5n/6\)#●ready to prove

Let \(f(n)\) be the least number of colours in a \((4, 5)\)-colouring of \(K_n\), that is, a symmetric colouring of the pairs of vertices of \(K_n\) in which the six edges of every \(K_4\) receive at least five distinct colours. Then \(f(n)/n \to 5/6\) as \(n \to \infty\).

Erdős and Gyárfás proved \(f(n) > 5(n - 1)/6\), and Bennett, Cushman, Dudek and Prałat constructed \((4, 5)\)-colourings of \(K_n\) with \(5n/6 + o(n)\) colours (Joos and Mubayi gave a shorter proof).

public theorem_wanted fourFiveColourNumberAsymptotic_holds : fourFiveColourNumberAsymptotic

def fourFiveColourNumberAsymptotic : Prop :=
  Tendsto (fun n : ℕ => (fourFiveColourNumber n : ℝ) / n) atTop (nhds (5 / 6))

WantedExt/Combinatorics/FourCliqueFiveColoursErdosProblem136Wanted.lean:48

Sources

T. F. Bloom, Erdős Problems, Problem #136, https://www.erdosproblems.com/136 (status SOLVED); resolution: P. Bennett, R. Cushman, A. Dudek and P. Prałat, The Erdős-Gyárfás function f(n, 4, 5) = 5n/6 + o(n) - so Gyárfás was right, arXiv:2207.02920 (2022); F. Joos and D. Mubayi, Ramsey theory constructions from hypergraph matchings, arXiv:2208.12563 (2022), abstract: (4, 5)-colourings of K_n with 5n/6 + o(n) colours; with the Erdős-Gyárfás lower bound f(n) > 5(n - 1)/6 this gives f(n) ~ 5n/6 (erdosproblems.com/136), https://arxiv.org/abs/2207.02920.

Uses 1

Statement usesThe asymptotic of the \((4, 5)\)-colouring number (Erdős Problem 136)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.