Ordered Ramsey numbers

DefinitionOrdered embedding#✓fully proved

Let \(\lt _H\) be a strict total order on \(\{0, \dots, n - 1\}\). A map \(f \colon \{0, \dots, n - 1\} \to \{0, \dots, N - 1\}\) is an ordered embedding when it is injective and \(a \lt _H b\) implies \(f(a) < f(b)\) for all \(a\) and \(b\), where \(\{0, \dots, N - 1\}\) carries its natural order.

def IsOrderedEmbedding {n N : Nat} (ordH : MathlibExt.Order.StrictTotalOrder (Fin n))
    (f : Fin n → Fin N) : Prop :=
  Function.Injective f ∧ ∀ a b : Fin n, ordH.lt a b → f a < f b

Sources

• [AIM-COMBINATORICS-0079] Order-robust ordered Ramsey numbers of regular graphs (aim-combinatorics-notes.json notes[78], Source item 32, Section: Ordered Ramsey numbers, Workshop: Graph Ramsey theory, https://www.overleaf.com/read/mnvcscjjysvg).

Uses 1 · Used by 2

Statement usesStrict total order

Used byBlue ordered copy · Red ordered copy

DefinitionRed ordered copy#✓fully proved

Let \(H\) be a simple graph on \(\{0, \dots, n - 1\}\) with a strict total order \(\lt _H\) on its vertices, and let \(G\) be a simple graph on \(\{0, \dots, N - 1\}\), the red graph. Then \(G\) contains a red ordered copy of \((H, \lt _H)\) when there is an ordered embedding \(f\) of \((\{0, \dots, n - 1\}, \lt _H)\) into \(\{0, \dots, N - 1\}\) such that \(f(a)\) and \(f(b)\) are adjacent in \(G\) whenever \(a\) and \(b\) are adjacent in \(H\). The copy need not be induced.

def HasRedOrderedCopy {n N : Nat} (H : SimpleGraph (Fin n))
    (ordH : MathlibExt.Order.StrictTotalOrder (Fin n)) (G : SimpleGraph (Fin N)) : Prop :=
  ∃ f : Fin n → Fin N, IsOrderedEmbedding ordH f ∧
    ∀ a b : Fin n, H.Adj a b → G.Adj (f a) (f b)

Sources

• [AIM-COMBINATORICS-0079] Order-robust ordered Ramsey numbers of regular graphs (aim-combinatorics-notes.json notes[78], Source item 32, Section: Ordered Ramsey numbers, Workshop: Graph Ramsey theory, https://www.overleaf.com/read/mnvcscjjysvg).

Uses 2 · Used by 1

Statement usesOrdered embedding · Strict total order

Used byOrdered Ramsey property

DefinitionBlue ordered copy#✓fully proved

Let \(H\) be a simple graph on \(\{0, \dots, n - 1\}\) with a strict total order \(\lt _H\) on its vertices, and let \(G\) be a simple graph on \(\{0, \dots, N - 1\}\), the red graph. Then \(G\) admits a blue ordered copy of \((H, \lt _H)\) when there is an ordered embedding \(f\) of \((\{0, \dots, n - 1\}, \lt _H)\) into \(\{0, \dots, N - 1\}\) such that \(f(a)\) and \(f(b)\) are not adjacent in \(G\) whenever \(a\) and \(b\) are adjacent in \(H\). Since \(f\) is injective, these pairs are edges of the blue graph, the complement of \(G\). The copy need not be induced.

def HasBlueOrderedCopy {n N : Nat} (H : SimpleGraph (Fin n))
    (ordH : MathlibExt.Order.StrictTotalOrder (Fin n)) (G : SimpleGraph (Fin N)) : Prop :=
  ∃ f : Fin n → Fin N, IsOrderedEmbedding ordH f ∧
    ∀ a b : Fin n, H.Adj a b → ¬ G.Adj (f a) (f b)

Sources

• [AIM-COMBINATORICS-0079] Order-robust ordered Ramsey numbers of regular graphs (aim-combinatorics-notes.json notes[78], Source item 32, Section: Ordered Ramsey numbers, Workshop: Graph Ramsey theory, https://www.overleaf.com/read/mnvcscjjysvg).

Uses 2 · Used by 1

Statement usesOrdered embedding · Strict total order

Used byOrdered Ramsey property

DefinitionOrdered Ramsey property#✓fully proved

Let \(H\) be a simple graph on \(\{0, \dots, n - 1\}\) with a strict total order \(\lt _H\) on its vertices. A natural number \(N\) has the ordered Ramsey property for \((H, \lt _H)\) when every simple graph \(G\) on \(\{0, \dots, N - 1\}\) contains a red ordered copy of \((H, \lt _H)\) or admits a blue ordered copy of \((H, \lt _H)\). Equivalently, every red/blue colouring of the edges of the complete graph on \(\{0, \dots, N - 1\}\) with its natural order, with red edges those of \(G\), contains a monochromatic ordered copy of \((H, \lt _H)\).

def OrderedRamseyProp {n : Nat} (H : SimpleGraph (Fin n))
    (ordH : MathlibExt.Order.StrictTotalOrder (Fin n)) (N : Nat) : Prop :=
  ∀ G : SimpleGraph (Fin N),
    HasRedOrderedCopy H ordH G ∨ HasBlueOrderedCopy H ordH G

Sources

• [AIM-COMBINATORICS-0079] Order-robust ordered Ramsey numbers of regular graphs (aim-combinatorics-notes.json notes[78], Source item 32, Section: Ordered Ramsey numbers, Workshop: Graph Ramsey theory, https://www.overleaf.com/read/mnvcscjjysvg).

Uses 3 · Used by 1

Statement usesBlue ordered copy · Red ordered copy · Strict total order

Used byOrdered Ramsey number

DefinitionOrdered Ramsey number#✓fully proved

For a simple graph \(H\) on \(\{0, \dots, n - 1\}\) with a strict total order \(\lt _H\) on its vertices, the ordered Ramsey number \(r_<(H, \lt _H)\) is the least natural number \(N\) with the ordered Ramsey property for \((H, \lt _H)\), that is, such that every red/blue colouring of the edges of the complete graph on \(\{0, \dots, N - 1\}\) with its natural order contains a monochromatic ordered copy of \((H, \lt _H)\). It is \(0\) if no such \(N\) exists.

noncomputable def orderedRamseyNumber {n : Nat} (H : SimpleGraph (Fin n))
    (ordH : MathlibExt.Order.StrictTotalOrder (Fin n)) : Nat :=
  sInf { N : Nat | OrderedRamseyProp H ordH N }

Sources

• [AIM-COMBINATORICS-0079] Order-robust ordered Ramsey numbers of regular graphs (aim-combinatorics-notes.json notes[78], Source item 32, Section: Ordered Ramsey numbers, Workshop: Graph Ramsey theory, https://www.overleaf.com/read/mnvcscjjysvg).

Uses 2 · Used by 1

Statement usesOrdered Ramsey property · Strict total order

Used byOrder-robust ordered Ramsey conjecture for 100-regular graphs

DefinitionOrder-robust ordered Ramsey conjecture for 100-regular graphs#✓fully proved

There are a real number \(c > 0\) and a natural number \(N_0\) such that for every \(n \ge N_0\) there is a \(100\)-regular simple graph \(H\) on \(\{0, \dots, n - 1\}\) such that \(r_<(H, \lt _H) \ge n^{1+c}\) for every strict total order \(\lt _H\) on its vertices, where \(r_<(H, \lt _H)\) is the ordered Ramsey number of \(H\) with the order \(\lt _H\).

This is the AIM question asking whether such a \(c\) exists, stated as a claim.

def conjecture : Prop :=
  ∃ c : Real, 0 < c ∧ ∃ N0 : Nat, ∀ n : Nat, N0 ≤ n →
    ∃ H : SimpleGraph (Fin n), letI : H.LocallyFinite := fun _ ↦ Fintype.ofFinite _;
      H.IsRegularOfDegree 100 ∧
      ∀ ordH : MathlibExt.Order.StrictTotalOrder (Fin n),
        Real.rpow (n : Real) ((1 : Real) + c) ≤
          (orderedRamseyNumber H ordH : Real)

Sources

• [AIM-COMBINATORICS-0079] Order-robust ordered Ramsey numbers of regular graphs (aim-combinatorics-notes.json notes[78], Source item 32, Section: Ordered Ramsey numbers, Workshop: Graph Ramsey theory, https://www.overleaf.com/read/mnvcscjjysvg).

Uses 2 · Used by 1

Statement usesOrdered Ramsey number · Strict total order

Used byThe order-robust ordered Ramsey conjecture holds

TheoremThe order-robust ordered Ramsey conjecture holds#●ready to prove

There are a real number \(c > 0\) and a natural number \(N_0\) such that for every \(n \ge N_0\) there is a \(100\)-regular simple graph \(H\) on \(\{0, \dots, n - 1\}\) such that \(r_<(H, \lt _H) \ge n^{1+c}\) for every strict total order \(\lt _H\) on its vertices. Here \(r_<(H, \lt _H)\) is the least \(N\) such that every red/blue colouring of the edges of the complete graph on \(\{0, \dots, N - 1\}\) with its natural order contains a monochromatic copy of \(H\) (not necessarily induced) under an injective map sending \(\lt _H\) into the natural order, and \(0\) if there is no such \(N\).

Balko, Jelínek and Valtr prove that for every \(d \ge 3\) almost every \(d\)-regular \(n\)-vertex graph has ordered Ramsey number at least \(n^{3/2-1/d}/(4 \log n \log \log n)\) under every vertex ordering; for \(d = 100\) this exceeds \(n^{1+c}\) for any \(c < 49/100\) and all large \(n\).

public theorem_wanted conjecture_holds : conjecture

Sources

• M. Balko, V. Jelínek and P. Valtr, On ordered Ramsey numbers of bounded-degree graphs, arXiv:1606.05628, https://arxiv.org/abs/1606.05628.

Uses 1

Statement usesOrder-robust ordered Ramsey conjecture for 100-regular graphs

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.