Ramsey graphs for the triangle

DefinitionRamsey graphs for the triangle#✓fully proved

A graph $G$ on the vertex set $\{0, \dots, n - 1\}$ is $r$-Ramsey for the triangle when every colouring $c$ of the ordered pairs of vertices with $r$ colours that is symmetric ($c(a, b) = c(b, a)$) admits three distinct vertices $u, v, w$ that form a triangle in $G$ with $c(u, v) = c(v, w) = c(w, u)$.

For $r \ge 1$ this says that every colouring of the edges of $G$ with $r$ colours has a monochromatic triangle.

def IsTriangleRamsey (n : ℕ) (G : SimpleGraph (Fin n)) (r : ℕ) : Prop :=
  ∀ c : Fin n → Fin n → Fin r,
    (∀ a : Fin n, ∀ b : Fin n, c a b = c b a) →
      ∃ u : Fin n, ∃ v : Fin n, ∃ w : Fin n,
        u ≠ v ∧ v ≠ w ∧ w ≠ u ∧ G.Adj u v ∧ G.Adj v w ∧ G.Adj w u ∧
          c u v = c v w ∧ c v w = c w u

Sources

[AIM-COMBINATORICS-0060], aim-combinatorics-notes.json notes[59], Source item 13, Section Ramsey minimal graphs, Workshop Graph Ramsey theory.

Used by 1

Used byRamsey-minimal graphs for the triangle

DefinitionRamsey property for the triangle after deleting a vertex#✓fully proved

Let $G$ be a graph on the vertex set $\{0, \dots, n - 1\}$, $r$ a natural number and $x$ a vertex. The property holds when every colouring $c$ of the ordered pairs of vertices with $r$ colours that is symmetric ($c(a, b) = c(b, a)$) admits three distinct vertices $u, v, w$, all different from $x$, that form a triangle in $G$ with $c(u, v) = c(v, w) = c(w, u)$.

def IsTriangleRamseyDeleteVertex (n : ℕ) (G : SimpleGraph (Fin n)) (r : ℕ)
    (x : Fin n) : Prop :=
  ∀ c : Fin n → Fin n → Fin r,
    (∀ a : Fin n, ∀ b : Fin n, c a b = c b a) →
      ∃ u : Fin n, ∃ v : Fin n, ∃ w : Fin n,
        u ≠ x ∧ v ≠ x ∧ w ≠ x ∧
          u ≠ v ∧ v ≠ w ∧ w ≠ u ∧ G.Adj u v ∧ G.Adj v w ∧ G.Adj w u ∧
          c u v = c v w ∧ c v w = c w u

Sources

[AIM-COMBINATORICS-0060], aim-combinatorics-notes.json notes[59], Source item 13, Section Ramsey minimal graphs, Workshop Graph Ramsey theory.

Used by 1

Used byRamsey-minimal graphs for the triangle

DefinitionRamsey-minimal graphs for the triangle#✓fully proved

A graph $G$ on the vertex set $\{0, \dots, n - 1\}$ is $r$-Ramsey-minimal for the triangle when $G$ is $r$-Ramsey for the triangle, no proper spanning subgraph of $G$ (a graph on the same vertices whose edges are edges of $G$, missing at least one of them) is $r$-Ramsey for the triangle, and for every vertex $x$ it is false that every symmetric colouring of the ordered pairs of vertices with $r$ colours admits a triangle of $G$ avoiding $x$ whose three edges have the same colour.

Given the first two conditions, the last one says exactly that $G$ has no isolated vertices.

def IsRamseyMinimal (n : ℕ) (G : SimpleGraph (Fin n)) (r : ℕ) : Prop :=
  IsTriangleRamsey n G r ∧
    (∀ H : SimpleGraph (Fin n),
      (∀ u : Fin n, ∀ v : Fin n, H.Adj u v → G.Adj u v) →
        (∃ u : Fin n, ∃ v : Fin n, G.Adj u v ∧ ¬ H.Adj u v) →
          ¬ IsTriangleRamsey n H r) ∧
    ∀ x : Fin n, ¬ IsTriangleRamseyDeleteVertex n G r x

def IsTriangleRamsey (n : ℕ) (G : SimpleGraph (Fin n)) (r : ℕ) : Prop :=
  ∀ c : Fin n → Fin n → Fin r,
    (∀ a : Fin n, ∀ b : Fin n, c a b = c b a) →
      ∃ u : Fin n, ∃ v : Fin n, ∃ w : Fin n,
        u ≠ v ∧ v ≠ w ∧ w ≠ u ∧ G.Adj u v ∧ G.Adj v w ∧ G.Adj w u ∧
          c u v = c v w ∧ c v w = c w u

WantedExt/Combinatorics/TriangleRamseyMinimalThetaWanted.lean:30

def IsTriangleRamseyDeleteVertex (n : ℕ) (G : SimpleGraph (Fin n)) (r : ℕ)
    (x : Fin n) : Prop :=
  ∀ c : Fin n → Fin n → Fin r,
    (∀ a : Fin n, ∀ b : Fin n, c a b = c b a) →
      ∃ u : Fin n, ∃ v : Fin n, ∃ w : Fin n,
        u ≠ x ∧ v ≠ x ∧ w ≠ x ∧
          u ≠ v ∧ v ≠ w ∧ w ≠ u ∧ G.Adj u v ∧ G.Adj v w ∧ G.Adj w u ∧
          c u v = c v w ∧ c v w = c w u

WantedExt/Combinatorics/TriangleRamseyMinimalThetaWanted.lean:38

Sources

[AIM-COMBINATORICS-0060], aim-combinatorics-notes.json notes[59], Source item 13, Section Ramsey minimal graphs, Workshop Graph Ramsey theory.

Uses 2 · Used by 1

Statement usesRamsey graphs for the triangle · Ramsey property for the triangle after deleting a vertex

Used byLeast minimum degree of Ramsey-minimal graphs for the triangle

DefinitionMinimum degree of a finite graph#✓fully proved

A graph $G$ on the vertex set $\{0, \dots, n - 1\}$ has minimum degree $d$ when every vertex of $G$ has at least $d$ neighbours and some vertex of $G$ has exactly $d$ neighbours; in particular $n \ge 1$.

def HasMinDegree (n : ℕ) (G : SimpleGraph (Fin n)) (d : ℕ) : Prop :=
  (∀ v : Fin n, d ≤ Set.ncard { w : Fin n | G.Adj v w }) ∧
    ∃ v : Fin n, Set.ncard { w : Fin n | G.Adj v w } = d

Sources

[AIM-COMBINATORICS-0060], aim-combinatorics-notes.json notes[59], Source item 13, Section Ramsey minimal graphs, Workshop Graph Ramsey theory.

Used by 1

Used byLeast minimum degree of Ramsey-minimal graphs for the triangle

DefinitionLeast minimum degree of Ramsey-minimal graphs for the triangle#✓fully proved

For a natural number $r$, $s_r(K_3)$ is the least natural number $d$ such that, for some $n$, some graph on the vertex set $\{0, \dots, n - 1\}$ is $r$-Ramsey-minimal for the triangle and has minimum degree $d$; if no such graph exists, $s_r(K_3) = 0$.

noncomputable def sRamsey (r : ℕ) : ℕ := by
  classical
  exact if h : ∃ d : ℕ, ∃ n : ℕ, ∃ G : SimpleGraph (Fin n),
      IsRamseyMinimal n G r ∧ HasMinDegree n G d then Nat.find h else 0

Sources

[AIM-COMBINATORICS-0060], aim-combinatorics-notes.json notes[59], Source item 13, Section Ramsey minimal graphs, Workshop Graph Ramsey theory, Conjecture $s_r(3) = \Theta(r^2 \log r)$ .

Uses 2 · Used by 1

Statement usesMinimum degree of a finite graph · Ramsey-minimal graphs for the triangle

Used byMinimum-degree conjecture for minimal Ramsey graphs of the triangle

DefinitionMinimum-degree conjecture for minimal Ramsey graphs of the triangle#✓fully proved

The statement that $s_r(K_3) = \Theta(r^2 \log r)$ as the natural number $r$ tends to infinity, where $s_r(K_3)$ is the least minimum degree of a graph that is $r$-Ramsey-minimal for the triangle ($0$ if there is none) and $\log$ is the natural logarithm: there are constants $c, C > 0$ such that $c \, r^2 \log r \le s_r(K_3) \le C \, r^2 \log r$ for all sufficiently large $r$.

def conjecture : Prop :=
  Asymptotics.IsTheta Filter.atTop
    (fun r : ℕ => (sRamsey r : ℝ))
    (fun r : ℕ => (r : ℝ) ^ 2 * Real.log (r : ℝ))

noncomputable def sRamsey (r : ℕ) : ℕ := by
  classical
  exact if h : ∃ d : ℕ, ∃ n : ℕ, ∃ G : SimpleGraph (Fin n),
      IsRamseyMinimal n G r ∧ HasMinDegree n G d then Nat.find h else 0

WantedExt/Combinatorics/TriangleRamseyMinimalThetaWanted.lean:62

Sources

[AIM-COMBINATORICS-0060], aim-combinatorics-notes.json notes[59], Source item 13, Section Ramsey minimal graphs, Workshop Graph Ramsey theory, Canonical tag conjecture.

Uses 1 · Used by 1

Statement usesLeast minimum degree of Ramsey-minimal graphs for the triangle

Used byMinimum degree of minimal Ramsey graphs for the triangle (Guo–Warnke)

TheoremMinimum degree of minimal Ramsey graphs for the triangle (Guo–Warnke)#●ready to prove

Let $s_r(K_3)$ be the least minimum degree of a graph that is $r$-Ramsey-minimal for the triangle, with $s_r(K_3) = 0$ if there is no such graph, as defined for the conjecture. Then $s_r(K_3) = \Theta(r^2 \log r)$ as the natural number $r$ tends to infinity, where $\log$ is the natural logarithm: there are constants $c, C > 0$ such that $c \, r^2 \log r \le s_r(K_3) \le C \, r^2 \log r$ for all sufficiently large $r$.

Resolved true: Guo and Warnke (Packing nearly optimal Ramsey R(3,t) graphs, arXiv:1711.05877) prove this, confirming the conjecture of Fox, Grinshpun, Liebenau, Person and Szabó.

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  Asymptotics.IsTheta Filter.atTop
    (fun r : ℕ => (sRamsey r : ℝ))
    (fun r : ℕ => (r : ℝ) ^ 2 * Real.log (r : ℝ))

WantedExt/Combinatorics/TriangleRamseyMinimalThetaWanted.lean:68

Sources

H. Guo and L. Warnke, Packing nearly optimal Ramsey R(3,t) graphs, arXiv:1711.05877, https://arxiv.org/abs/1711.05877.

Uses 1

Statement usesMinimum-degree conjecture for minimal Ramsey graphs of the triangle

InductiveTrees of triangles#✓fully proved

The trees of triangles on a vertex set $V$ are the graphs on $V$ built recursively as follows. A graph whose edges are exactly the three edges of a triangle on distinct vertices $a, b, c$ is a tree of triangles. If $H_0$ is a tree of triangles, $xy$ is an edge of $H_0$, and $z$ is a vertex different from $x$ and $y$ with no neighbours in $H_0$, then the graph obtained from $H_0$ by joining $z$ to $x$ and to $y$ is a tree of triangles.

MathlibExt.Combinatorics.TriangleTreeLocalRamseyWanted.IsTriangleTree · 17 lines

inductive IsTriangleTree {V : Type*} : SimpleGraph V → Prop where
  | base : ∀ (H : SimpleGraph V) (a b c : V),
      a ≠ b → b ≠ c → a ≠ c →
      H.Adj a b → H.Adj b c → H.Adj a c →
      (∀ x y : V, H.Adj x y →
        (x = a ∨ x = b ∨ x = c) ∧ (y = a ∨ y = b ∨ y = c)) →
      (∀ x y : V, (x = a ∨ x = b ∨ x = c) →
        (y = a ∨ y = b ∨ y = c) → x ≠ y → H.Adj x y) →
      IsTriangleTree H
  | step : ∀ (H₀ H : SimpleGraph V) (z x y : V),
      IsTriangleTree H₀ →
      H₀.Adj x y → x ≠ y → z ≠ x → z ≠ y →
      (¬ ∃ w : V, H₀.Adj z w) →
      H.Adj x z → H.Adj y z →
      (∀ w : V, H.Adj z w → w = x ∨ w = y) →
      (∀ u v : V, u ≠ z → v ≠ z → (H.Adj u v ↔ H₀.Adj u v)) →
      IsTriangleTree H

Sources

AIM-COMBINATORICS-0056, aim-combinatorics-notes.json notes[55]: any graph built recursively by starting with a triangle, and then adding two edges at a time that forms a single new triangle with an existing edge.

Used by 1

Used byGraphs that are locally trees of triangles

DefinitionGraphs that arrow the triangle#✓fully proved

A graph $G$ arrows the triangle in two colours, written $G \to_2 K_3$, if every colouring of the edges of $G$ with two colours contains a monochromatic triangle: three distinct pairwise adjacent vertices whose three edges all have the same colour.

def Ramseys2Triangle {V : Type*} (G : SimpleGraph V) : Prop :=
  ∀ χ : ∀ (x y : V), G.Adj x y → Fin 2,
    (∀ (x y : V) (h₁ : G.Adj x y) (h₂ : G.Adj y x), χ x y h₁ = χ y x h₂) →
    ∃ a b c : V, ∃ (hab : G.Adj a b) (hbc : G.Adj b c) (hac : G.Adj a c),
      a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ χ a b hab = χ b c hbc ∧ χ a b hab = χ a c hac

Sources

AIM-COMBINATORICS-0056, aim-combinatorics-notes.json notes[55]: G with 2 colors arrows K₃, i.e. every 2-coloring of the edges of G contains a monochromatic triangle.

Used by 1

Used byRödl's question on Ramsey graphs that are locally trees of triangles

DefinitionGraphs that are locally trees of triangles#✓fully proved

A graph $G$ on a vertex set $V$ is locally a tree of triangles on $\ell$ vertices if for every set $S$ of exactly $\ell$ vertices there is a tree of triangles on $V$ that contains every edge of $G$ with both endpoints in $S$.

@[nolint unusedArguments]
def IsLocallyTriangleTree {V : Type*} [DecidableEq V] (G : SimpleGraph V) (ℓ : ℕ) : Prop :=
  ∀ S : Finset V, S.card = ℓ →
    ∃ H' : SimpleGraph V, IsTriangleTree H' ∧
      ∀ x y : V, x ∈ S → y ∈ S → G.Adj x y → H'.Adj x y

inductive IsTriangleTree {V : Type*} : SimpleGraph V → Prop where
  | base : ∀ (H : SimpleGraph V) (a b c : V),
      a ≠ b → b ≠ c → a ≠ c →
      H.Adj a b → H.Adj b c → H.Adj a c →
      (∀ x y : V, H.Adj x y →
        (x = a ∨ x = b ∨ x = c) ∧ (y = a ∨ y = b ∨ y = c)) →
      (∀ x y : V, (x = a ∨ x = b ∨ x = c) →
        (y = a ∨ y = b ∨ y = c) → x ≠ y → H.Adj x y) →
      IsTriangleTree H
  | step : ∀ (H₀ H : SimpleGraph V) (z x y : V),
      IsTriangleTree H₀ →
      H₀.Adj x y → x ≠ y → z ≠ x → z ≠ y →
  ⋯

WantedExt/Combinatorics/TriangleTreeLocalRamseyWanted.lean:31

Sources

AIM-COMBINATORICS-0056, aim-combinatorics-notes.json notes[55]: on every ℓ vertices G induces a subgraph of a tree of triangles.

Uses 1 · Used by 1

Statement usesTrees of triangles

Used byRödl's question on Ramsey graphs that are locally trees of triangles

DefinitionRödl's question on Ramsey graphs that are locally trees of triangles#✓fully proved

This is the statement that for every natural number $\ell$ there is a finite graph $G$ with at least $\ell$ vertices such that $G \to_2 K_3$ (every colouring of the edges of $G$ with two colours contains a monochromatic triangle) and $G$ is locally a tree of triangles on $\ell$ vertices: for every set $S$ of exactly $\ell$ vertices of $G$, some tree of triangles on the vertex set of $G$ contains every edge of $G$ with both endpoints in $S$.

Posed as an open question, it has been answered in the affirmative.

def conjecture : Prop :=
  ∀ ℓ : ℕ, ∃ (V : Type), ∃ (_ : DecidableEq V), ∃ (_ : Fintype V),
    ∃ G : SimpleGraph V, ℓ ≤ Fintype.card V ∧ Ramseys2Triangle G ∧ IsLocallyTriangleTree G ℓ

def Ramseys2Triangle {V : Type*} (G : SimpleGraph V) : Prop :=
  ∀ χ : ∀ (x y : V), G.Adj x y → Fin 2,
    (∀ (x y : V) (h₁ : G.Adj x y) (h₂ : G.Adj y x), χ x y h₁ = χ y x h₂) →
    ∃ a b c : V, ∃ (hab : G.Adj a b) (hbc : G.Adj b c) (hac : G.Adj a c),
      a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ χ a b hab = χ b c hbc ∧ χ a b hab = χ a c hac

WantedExt/Combinatorics/TriangleTreeLocalRamseyWanted.lean:54

@[nolint unusedArguments]
def IsLocallyTriangleTree {V : Type*} [DecidableEq V] (G : SimpleGraph V) (ℓ : ℕ) : Prop :=
  ∀ S : Finset V, S.card = ℓ →
    ∃ H' : SimpleGraph V, IsTriangleTree H' ∧
      ∀ x y : V, x ∈ S → y ∈ S → G.Adj x y → H'.Adj x y

WantedExt/Combinatorics/TriangleTreeLocalRamseyWanted.lean:65

Sources

AIM-COMBINATORICS-0056, aim-combinatorics-notes.json notes[55]: for every ℓ, does there exist a graph G →₂ K₃ which on every ℓ vertices induces a subgraph of a tree of triangles.

Uses 2 · Used by 1

Statement usesGraphs that are locally trees of triangles · Graphs that arrow the triangle

Used byRamsey graphs for the triangle that are locally trees of triangles

TheoremRamsey graphs for the triangle that are locally trees of triangles#●ready to prove

For every natural number $\ell$ there is a finite graph $G$ with at least $\ell$ vertices such that $G \to_2 K_3$, that is, every colouring of the edges of $G$ with two colours contains a monochromatic triangle, and such that for every set $S$ of exactly $\ell$ vertices of $G$, some tree of triangles on the vertex set of $G$ contains every edge of $G$ with both endpoints in $S$.

This follows from Reiher and Rödl's girth Ramsey theorem (Theorem 1.6 with $F = K_3$, $r = 2$, $n = \ell$), which gives a graph $H$ with $H \to_2 K_3$ in which every set of at most $\ell$ vertices induces a partial $K_3$-forest; such graphs have treewidth at most $2$, hence lie in trees of triangles ($2$-trees).

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  ∀ ℓ : ℕ, ∃ (V : Type), ∃ (_ : DecidableEq V), ∃ (_ : Fintype V),
    ∃ G : SimpleGraph V, ℓ ≤ Fintype.card V ∧ Ramseys2Triangle G ∧ IsLocallyTriangleTree G ℓ

WantedExt/Combinatorics/TriangleTreeLocalRamseyWanted.lean:76

Sources

C. Reiher and V. Rödl, The girth Ramsey theorem, arXiv:2308.15589, https://arxiv.org/abs/2308.15589.

Uses 1

Statement usesRödl's question on Ramsey graphs that are locally trees of triangles

10 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.