An upper bound on the Ramsey numbers, Part II - The Main Result

In the previous post, we introduced definitions and established prerequisites for proving an upper bound on the Ramsey numbers. We can now proceed with the central statement that will lead to our final proof. It reads as follows:

Recursive Bound for Ramsey Numbers. Suppose \(R(m −1, n)\) and \(R(m, n −1)\) exist. We then prove that \(R(m, n)\) exists and that \[R(m, n) \leq R(m−1, n) + R(m, n−1).\]

Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 296.

Recall that we defined the Ramsey number as the infimum over the naturals that have the Ramsey property:

noncomputable def R (m n : ℕ) : ℕ := sInf { N | ramseyProp N m n}

The statement

We note a couple of adjustments we need to make to the statement before we can usefully formalize it in Lean. In our case, “existence of the Ramsey number” means the existence of a natural number that has the Ramsey property. If we show that \(R(m−1, n) + R(m, n−1)\) has the \((m,n)\)-Ramsey property, the stated inequality directly follows from the definition of the infimum. The inequality also does not actually hold for \(m=0\) or \(n=0\), since \(R(0,m) = 0\) and \(R(1,m) = 1\), but \[R(1,1) = 1 > 0 = 0 + 0 = R(0,1) + R(1,0),\] so we require both parameters to be strictly positive. Finally, dealing with subtraction of natural numbers in Lean is tiresome, so we shift everything by \(1\). Given these considerations, we can state the theorem we are going to prove as follows:

theorem R_bounded_recursive (m n : ℕ) (posₘ : 0 < m) (posₙ : 0 < n) (rₘ : ∃ N, ramseyProp N (m + 1) n) (rₙ : ∃ N, ramseyProp N m (n + 1)) : ramseyProp (R(m, n + 1) + R(m + 1, n)) (m + 1) (n + 1) := by

Establishing definitions

The first few sentences of the proof translate nicely into Lean. “ Suppose \(N = R(m − 1, n) + R(m, n − 1)\)…” We shift by 1, and use set instead of the usual let to name the definition.

set N := R(m, n + 1) + R(m + 1, n) with Neq

Next, “consider an arbitrary red-blue coloring of \(K_N\).” The definition of the Ramsey property already quantifies over an arbitrary coloring, so we can use the intro tactic to make it explicit from the goal.

intro V _ _ cardV C _

Now, “for a vertex \(v\), let \(A\) be the set of vertices joined to \(v\) by a red edge, and \(B\) the vertices joined by a blue edge.” We need to ensure that we’re not talking about the empty graph so that we can pick a vertex – we do this by proving the vertex set of our coloring is nonempty, since its cardinality is N and we have already proven the lemma R_pos the prerequisites, stating that 0 < R(m,n) for strictly positive m and n.

have V_nonempty : Nonempty V := by rw [← card_pos_iff, cardV] exact add_pos (R_pos m (n+1) posₘ (zero_lt_succ n) rₙ) (R_pos (m+1) n (zero_lt_succ m) posₙ rₘ)

Now we can define v and A. Recall that in our encoding of edge colorings, an edge (v,w) is colored red if m an n are nonadjacent in the encoding graph C. Hence, we define A as the neighbor set of v in the complement graph, which is all vertices with an edge to v in Cᶜ and therefore nonadjacent in C (a fact we will have to establish explicitly later).

let v : V := V_nonempty.some let A := Cᶜ.neighborFinset v

Now, “we find that either \(|A| ≥ R(m − 1, n)\) or \(|B| ≥ R(m, n − 1)\). Suppose |A| ≥R(m −1, n), the other case being analogous.” We again shift by 1 and use the wlog tactic to get two cases:

wlog R_le_cardA : R(m, n + 1) ≤ #A with h

The goal of the first case is to prove that if our theorem statement follows from |A| ≥ R(m − 1, n) and we assume |A| < R(m − 1, n) (that is, |B| ≥ R(m, n − 1)), the theorem statement also follows. The goal of the second case is to prove that if our theorem statement follows from |A| ≥ R(m − 1, n).

The first case: reducing to symmetry

Proving the first case, only shrugged off as “analogous” in the text, is a bit technical. We examine the infoview to find our new state to be the following:

(...) h : ∀ (m n : ℕ), 0 < m → 0 < n → (∃ N, ramseyProp N (m + 1) n) → (∃ N, ramseyProp N m (n + 1)) → let N := R(m,n + 1) + R(m + 1,n); N = R(m,n + 1) + R(m + 1,n) → ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V], Fintype.card V = N → ∀ (C : SimpleGraph V) [inst_2 : DecidableRel C.Adj] (V_nonempty : Nonempty V), let v := V_nonempty.some; let A := Cᶜ.neighborFinset v; R(m,n + 1) ≤ #A → ∃ s, C.IsNIndepSet (m + 1) s ∨ C.IsNClique (n + 1) s R_le_cardA : ¬R(m,n + 1) ≤ #A ⊢ ∃ s, C.IsNIndepSet (m + 1) s ∨ C.IsNClique (n + 1) s

That’s quite a mouthful, but in essence we need to prove that given the previous context and R(m,n + 1) ≤ #A (this is the assumption called h here), and a proof that ¬R(m,n + 1) ≤ #A (this is the assumption R_le_cardA), we can prove the theorem statement, namely that ramseyProp (R(m, n + 1) + R(m + 1, n)) (m + 1) (n + 1), the definition of is already unfolded in the above infoview.

According to lemma R_symm from the prerequisites, the Ramsey number is symmetric. Also, we know that an N-independent set in a graph is an N-clique in the complement graph, and vice versa. These two facts will be sufficient to provide all the conditions of the hypothesis h! We start by defining B and establishing that |B| ≥ R(m, n − 1) indeed follows from the wlog assumption that |A| < R(m − 1, n).

let B := C.neighborFinset v have R_le_cardB : R(n, m + 1) ≤ #B := by have : Fintype.card V - 1 = Cᶜ.degree v + C.degree v := by simp [degree_compl, degree_lt_card_verts, le_sub_one_of_lt] have := calc (R(m, n + 1) + R(n, m + 1)) - 1 _ = #A + #B := by rw [@R_symm n, ← Neq, ← cardV, card_neighborFinset_eq_degree]; exact this _ < R(m, n + 1) + #B := by simp [lt_of_not_le R_le_cardA] exact le_of_add_le_add_left (le_of_pred_lt this)

Next, we rewrite the required things in our context to match the signature of h.

have ex m n := Exists.imp (ramseyProp_symm m n) apply ex at rₘ; apply ex at rₙ rw [Neq, @R_symm m, @R_symm (m + 1), add_comm] at cardV have : #B = Cᶜᶜ.degree v := by simp [B]; congr!; exact (compl_compl C).symm rw [this] at R_le_cardB

We can now use h to obtain a monochromatic vertex subset of the complement graph Cᶜ.

simp only [forall_const, Nonempty.forall] at h obtain ⟨s, rs⟩ := h n m posₙ posₘ rₙ rₘ V cardV Cᶜ v R_le_cardB

Rewriting with the mentioned facts about cliques and complements show that the obtained subset is monochromatic with the other color in C.

simp_rw [isNIndepSet_compl, ← isNIndepSet_compl Cᶜ, compl_compl] at rs exact ⟨s, rs.symm⟩

This concludes the fist case, and lets us continue with the paper proof.

The second case: following the text

Before we continue with the proof, let us establish that the edges connecting v to the vertices in A are indeed colored red.

have A_all_red : ∀ {u}, u ∈ A → ¬ C.Adj v u := by intro u a simp_all only [mem_neighborFinset, compl_adj, not_false_eq_true, A, v]

The paper proof continues by stating that “(…) by the definition of \(R(m − 1, n)\), there either exists in \(A\) a subset \(A_R\) of size \(m − 1\) all of whose edges are colored red which together with \(v\) yields a red \(K_m\), or there is a subset \(A_B\) of size \(n\) with all edges colored blue.” Recall that we proved the following monotonicity property in the prerequisites:

lemma ramseyProp_mono {m n : ℕ} (N s : ℕ) (h : N ≤ s) (ramseyProp_N : ramseyProp N m n) : ramseyProp s m n := by

By assumption, |A| ≥ R m (n + 1), so the coloring A induces also has the Ramsey property according to this lemma. Hence, there exists a monochromatic subset of A. We call it Aₘ.

let ⟨Aₘ, monochrom⟩ := ramseyProp_mono R_le_cardA (sInf_mem rₙ) _ (card_coe A) C[A].coe

Aₘ is a subtype of the induced graph’s vertices A. We need to embed it into V to talk about corresponding vertices in the big graph C:

set AₘV : Finset V := (Finset.map ⟨Subtype.val, Subtype.val_injective⟩ Aₘ) with AVe have AₘV_subset_A : AₘV ⊆ A := by intro _ memAV simp_all exact memAV.1

We are now ready to examine the two cases proposed in the paper proof.

cases' monochrom with all_red all_blue

Case one: AₘV has size m with all edges colored red, which together with v yields a red K_(m+1). We define the candidate set:

let Aᵥ := insert v AₘV

It indeed describes an all-red subgraph of C, which we show by establishing pairwise redness of some u, w ∈ Aᵥ.

have C_red : C.IsIndepSet Aᵥ := by intro u u_elem_Aᵥ w w_elem_Aᵥ unw

We need to handle the case that u or w happen to be v. It follows from the definition of A.

by_cases uvw : (u = v) ∨ (w = v) · have elem_A {x : V} (xnv : v ≠ x) (x_elem_Aᵥ : x ∈ Aᵥ) : x ∈ A := by cases' mem_insert.mp x_elem_Aᵥ with xeqv x_elem_AV · simp_all only [ne_eq, not_true_eq_false] · exact AₘV_subset_A x_elem_AV cases uvw all_goals simp_all [A] intro a exact (elem_A (Ne.symm unw) u_elem_Aᵥ) (C.adj_symm a)

Now for the interesting case: two members of Aᵥ that are not v have a red edge. We project them to A…

push_neg at uvw obtain ⟨wₐ, ⟨wₐelem_Aₘ, cw⟩⟩ := mem_map.mp (mem_of_mem_insert_of_ne w_elem_Aᵥ uvw.right) obtain ⟨uₐ, ⟨uₐelem_Aₘ, cu⟩⟩ := mem_map.mp (mem_of_mem_insert_of_ne u_elem_Aᵥ uvw.left) rw [← cw, ← cu]

…and show that the projections are indeed red in the induced coloring.

have : uₐ ≠ wₐ := by intro a; simp_all only [ne_eq] have := all_red.1 uₐelem_Aₘ wₐelem_Aₘ this simp [Subgraph.coe_adj, Subgraph.induce_adj] at this assumption

It remains to show the size of Aᵥ is m+1.

refine ⟨Aᵥ, (Or.inl ⟨C_red, ?_⟩)⟩ have : v ∉ AₘV := fun a => (not_mem_neighborFinset_self Cᶜ v) (AₘV_subset_A a) simp_all [isNIndepSet_iff, Aᵥ, AₘV]

Case two: if Aₘ is all blue and of size n + 1, we’re done. We chose its embedding as the monochromatic set…

exists AₘV

…and prove it’s an (n + 1)-clique.

have : C.IsNClique (n + 1) AₘV := have isClique : C.IsClique AₘV := by simp [AVe, coe_map] exact C.induce_isClique all_blue.1 have card_eq : #AₘV = n + 1 := by rw [card_map] exact all_blue.2 {isClique, card_eq} exact Or.inr this

This concludes the proof of the central statement. It remains to resolve this recurrence and use some basic properties of the binomial coefficient to show that the Ramsey number is bounded above by \(2^{2k-3}\) in the next post.