Erdős Problem 61 -- Erdős–Hajnal Conjecture

Reference: erdosproblems.com/61

def Erdos61.IsErdosHajnalLowerBound {α : Type u_1} [Fintype α] [DecidableEq α] (H : SimpleGraph α) (f : ℕ → ℝ) : Prop

Equations

• Erdos61.IsErdosHajnalLowerBound H f = ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (¬∃ (g : α ↪ Fin n), H = SimpleGraph.comap (⇑g) G) → ↑G.indepNum ≥ f n ∨ ↑G.cliqueNum ≥ f n

theorem Erdos61.erdos_61 : sorry ↔ ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (H : SimpleGraph α), ∃ c > 0, IsErdosHajnalLowerBound H fun (n : ℕ) => ↑n ^ c

The Erdős–Hajnal Conjecture states that there is a constant $c(H) > 0$ for each $H$ such that we can take $f(n) = n^{c(H)}$ in the above formulation.

theorem Erdos61.erdos_61.variants.erha89 {α : Type u_1} [Fintype α] [DecidableEq α] (H : SimpleGraph α) : ∃ c > 0, IsErdosHajnalLowerBound H fun (n : ℕ) => Real.exp (c * √(Real.log ↑n))

Erdős and Hajnal [ErHa89] proved that we can take $f(n) = \exp(c_H \sqrt{\log n})$ for some constant $c_H > 0$ dependending on $H$.

[ErHa89] Erdős, P. and Hajnal, A., Ramsey-type theorems. Discrete Appl. Math. (1989), 37-52.

theorem Erdos61.erdos_61.variants.bnss23 {α : Type u_1} [Fintype α] [DecidableEq α] (H : SimpleGraph α) : ∃ c > 0, IsErdosHajnalLowerBound H fun (n : ℕ) => Real.exp (c * √(Real.log ↑n * Real.log (Real.log ↑n)))

Bucić, Nguyen, Scott, and Seymour [BNSS23] improved this to $f(n) = \exp(c_H \sqrt{\log n \log \log n})$ for some constant $c_H > 0$ dependending on $H$.

[BNSS23] Bucić, M. and Nguyen, T. and Scott, A. and Seymour, P., A loglog step towards Erdos-Hajnal

theorem Erdos61.erdos_61.variants.p5 : ∃ c > 0, IsErdosHajnalLowerBound (SimpleGraph.pathGraph 5) fun (n : ℕ) => ↑n ^ c

Nguyen, Scott, and Seymour [NSS23] proved the conjecture for $H = P_5$, the path on five vertices: every $P_5$-free graph on $n$ vertices has a clique or independent set of polynomial size.

[NSS23] Nguyen, T., Scott, A. and Seymour, P., Induced subgraph density. VII. The five-vertex path. arXiv:2312.15333

theorem Erdos61.erdos_61.variants.c5 : ∃ c > 0, IsErdosHajnalLowerBound (SimpleGraph.cycleGraph 5) fun (n : ℕ) => ↑n ^ c

Chudnovsky, Scott, Seymour, and Spirkl [CSSS23] proved the conjecture for $H = C_5$, the cycle on five vertices: every graph with no induced five-cycle has a clique or independent set of polynomial size.

[CSSS23] Chudnovsky, M., Scott, A., Seymour, P. and Spirkl, S., Erdős–Hajnal for graphs with no 5-hole. Proc. Lond. Math. Soc. (3) 126 (2023), 997–1014.