Monochromatic clique packings

DefinitionMonochromatic clique packings#✓fully proved

Let \(n\) and \(k\) be natural numbers, and view a simple graph \(G\) on the vertex set \(\{0, 1, \dots, n - 1\}\) as a two-colouring of the edges of the complete graph \(K_n\): the edges of \(G\) are red and the edges of its complement \(G^c\) are blue. A finite family \(P\) of sets of vertices is a monochromatic \(k\)-clique packing for \(G\) when the sets in \(P\) are pairwise disjoint and each of them is a \(k\)-clique of \(G\) or a \(k\)-clique of \(G^c\), that is, a set of exactly \(k\) vertices spanning a monochromatic copy of \(K_k\).

def IsMonochromaticCliquePacking {n : ℕ} (G : SimpleGraph (Fin n)) (k : ℕ)
    (P : Finset (Finset (Fin n))) : Prop :=
  (P : Set (Finset (Fin n))).PairwiseDisjoint id ∧ ∀ S ∈ P, G.IsNClique k S ∨ Gᶜ.IsNClique k S

Used by 1

Used byErdős Problem 1015 in the Burr–Erdős–Spencer form

DefinitionBurr–Erdős–Spencer leftover value#✓fully proved

For natural numbers \(k\) and \(n\), let \(r = R(k, k - 1)\) be the classical two-colour Ramsey number. The leftover value is \(r - 1 + \big((n + 1 - r) \bmod k\big)\), where subtraction is truncated at \(0\) (in particular \(n + 1 - r\) is read as \(0\) when \(n + 1 \le r\)) and \(a \bmod 0 = a\).

For \(k \ge 2\) and large \(n\), Burr, Erdős and Spencer showed that this is the least number of vertices that vertex-disjoint monochromatic copies of \(K_k\) can be guaranteed to leave uncovered in every two-colouring of the edges of \(K_n\).

noncomputable def leftoverValue (k n : ℕ) : ℕ :=
  graphRamsey k (k - 1) - 1 + (n + 1 - graphRamsey k (k - 1)) % k

Uses 1 · Used by 1

Statement usesClassical Ramsey numbers

Used byErdős Problem 1015 in the Burr–Erdős–Spencer form

DefinitionErdős Problem 1015 in the Burr–Erdős–Spencer form#✓fully proved

This is the statement that for every natural number \(k \ge 2\) there is \(n_0\) such that for every \(n \ge n_0\) the following holds. Let \(r = R(k, k - 1)\) be the classical two-colour Ramsey number and let \(L = r - 1 + \big((n + 1 - r) \bmod k\big)\), where \(n + 1 - r\) is read as \(0\) if it is negative. View a simple graph \(G\) on \(n\) vertices as a two-colouring of the edges of \(K_n\), with the edges of \(G\) red and those of its complement \(G^c\) blue. Then every such colouring admits a monochromatic \(k\)-clique packing, that is, a finite family of pairwise disjoint sets of vertices, each a \(k\)-clique of \(G\) or of \(G^c\), leaving at most \(L\) vertices uncovered; and some colouring admits no such packing leaving fewer than \(L\) vertices uncovered. In other words, for these \(n\) the least number \(f(n, k)\) such that every two-colouring of \(K_n\) admits such a packing leaving at most \(f(n, k)\) vertices uncovered equals \(L\).

def monochromaticCliquePartitionLeftover : Prop :=
  ∀ k : ℕ, 2 ≤ k → ∃ n₀ : ℕ, ∀ n ≥ n₀,
    (∀ G : SimpleGraph (Fin n), ∃ P, IsMonochromaticCliquePacking G k P ∧
        n - k * P.card ≤ leftoverValue k n) ∧
    ∃ G : SimpleGraph (Fin n), ∀ P, IsMonochromaticCliquePacking G k P →
        leftoverValue k n ≤ n - k * P.card

Uses 2 · Used by 1

Statement usesMonochromatic clique packings · Burr–Erdős–Spencer leftover value

Used byBurr–Erdős–Spencer theorem on monochromatic clique packings

TheoremBurr–Erdős–Spencer theorem on monochromatic clique packings#●ready to prove

For every natural number \(k \ge 2\) there is \(n_0\) such that for every \(n \ge n_0\) the following holds. Let \(r = R(k, k - 1)\) be the classical two-colour Ramsey number and let \(L = r - 1 + \big((n + 1 - r) \bmod k\big)\), where \(n + 1 - r\) is read as \(0\) if it is negative. View a simple graph \(G\) on \(n\) vertices as a two-colouring of the edges of \(K_n\), with the edges of \(G\) red and those of its complement \(G^c\) blue. Then every such colouring admits a finite family of pairwise disjoint sets of vertices, each a \(k\)-clique of \(G\) or of \(G^c\), that leaves at most \(L\) vertices uncovered; and some colouring admits no such family leaving fewer than \(L\) vertices uncovered.

public theorem_wanted monochromaticCliquePartitionLeftover_holds :
    monochromaticCliquePartitionLeftover

Sources

• T. F. Bloom, Erdős Problems, Problem #1015, https://www.erdosproblems.com/1015 (status SOLVED); resolution: S. A. Burr, P. Erdős and J. H. Spencer, Ramsey theorems for multiple copies of graphs, Trans. Amer. Math. Soc. 209 (1975), 87-99, §5, Theorem 6: if k is given, then for sufficiently large n, f(n, k) = r(k, k - 1) - 1 + rem(n - r(k, k - 1) + 1, k), where f(n, k) is the minimal integer such that any two-coloring of K_n admits vertex-disjoint monochromatic K_k with at most f(n, k) points left over; erdosproblems.com/1015 lists the problem as solved citing this paper, https://users.renyi.hu/~p_erdos/1975-35.pdf.

Uses 1

Statement usesErdős Problem 1015 in the Burr–Erdős–Spencer form

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.