Erdős Problem 567

Let $G$ be either $Q_3$ or $K_{3,3}$ or $H_5$ (the last formed by adding two vertex-disjoint chords to $C_5$). Is it true that, if $H$ has $m$ edges and no isolated vertices, then $$ \hat{r}(G,H) \ll m? $$

In other words, is $G$ Ramsey size linear? A special case of Problem 566.

Reference: erdosproblems.com/567

[EFRS93] Erdős, Faudree, Rousseau and Schelp, Ramsey size linear graphs. Combin. Probab. Comput. (1993), 389-399.

def Erdos567.Q3 : SimpleGraph (Fin 3 → Bool)

$Q_3$ is the 3-dimensional hypercube graph (8 vertices, 12 edges). Vertices are 3-bit vectors. Two vertices are adjacent iff they differ in exactly one bit.

Equations

• Erdos567.Q3 = { Adj := fun (u v : Fin 3 → Bool) => {i : Fin 3 | u i ≠ v i}.card = 1, symm := Erdos567.Q3._proof_1, loopless := Erdos567.Q3._proof_2 }

def Erdos567.K33 : SimpleGraph (Fin 3 ⊕ Fin 3)

$K_{3,3}$ is the complete bipartite graph with partition sizes 3, 3 (6 vertices, 9 edges).

Equations

• Erdos567.K33 = completeBipartiteGraph (Fin 3) (Fin 3)

def Erdos567.H5 : SimpleGraph (Fin 5)

$H_5$ is $C_5$ with two vertex-disjoint chords (5 vertices, 7 edges). Also known as $K_4^*$ (the graph obtained from $K_4$ by subdividing one edge).

Equations

• Erdos567.H5 = SimpleGraph.cycleGraph 5 ⊔ SimpleGraph.edge 0 2 ⊔ SimpleGraph.edge 1 3

theorem Erdos567.erdos_567_Q3 : sorry ↔ Q3.IsRamseySizeLinear

Erdős Problem 567 (Q3)

Is $Q_3$ (the 3-dimensional hypercube) Ramsey size linear?

theorem Erdos567.erdos_567_K33 : sorry ↔ K33.IsRamseySizeLinear

Erdős Problem 567 (K33)

Is $K_{3,3}$ Ramsey size linear?

theorem Erdos567.erdos_567_H5 : sorry ↔ H5.IsRamseySizeLinear

Erdős Problem 567 (H5)

Is $H_5$ ($C_5$ with two vertex-disjoint chords) Ramsey size linear?