In the previous post, we established the following recursive bound on the Ramsey number:

1
2
3
4

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

This post aims to formalize the proof of the explicit bound \(R(k,k) \leq 2^{2k-3}\) given in the book:

Explicit Bound for Ramsey Numbers. (...) with the starting values \(R(m, 2) = m\) and \(R(2, n) = n\), we obtain from the familiar recursion for binomial coefficients \[R(m,n) \leq \binom{m+n-1}{m-1},\] and, in particular, \[R(k,k) \leq \binom{2k-2}{k-1} = \binom{2k-3}{k-1} + \binom{2k-3}{k-2} \leq 2^{2k-3}.\]
Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 296.

An induction principle

The “familiar recursion for binomial coefficients” is proven by induction. However, it is not standard induction, proving a property of one natural number by providing proofs for zero and successor. This kind of proof would be straightforward to do in Lean, e.g. using the induction tactic. Instead, we encounter a proof about two natural numbers, using two base cases, and not even starting from zero! Luckily, Lean allows us to express abstract induction principles for more involved proofs, as we have discussed in a previous blog post on this topic. We will now see this technique in action!

First, let us figure out the shape of our motive, namely the statement we would like to prove by induction. There are two variables (\(m\) and \(n\)) of type ℕ, and both are required to be larger or equal 2. Our goal is to prove \(R(m,n) \leq \binom{m+n-1}{m-1}\), which translated to Lean will be of type Prop. Therefore, the type of our motive is

1

P : ∀ (m n : ℕ) , 2 ≤ m → 2 ≤ n → Prop

and the thing we would like to prove with our inductive proof is

1

∀ m n leₘ leₙ, P m n leₘ leₙ

Next, we examine the assumptions under which the proof will work out. We observe two base cases,

1
2

(baseₙ : ∀ m leₘ, P m 2 leₘ (AtLeastTwo.prop))
(baseₘ : ∀ n leₙ, P 2 n (AtLeastTwo.prop) leₙ)

as well as a recursive statement giving us a proof about \(R(m,n)\) from \(R(m−1, n)\) and \(R(m, n−1)\), which abstracted to P reads as

1
2
3

(succ  : ∀ m n leₘ leₙ, P (m + 1) n (le_succ_of_le leₘ) leₙ →
                        P m (n + 1) leₘ (le_succ_of_le leₙ) →
                        P (m + 1) (n + 1) (le_succ_of_le leₘ) (le_succ_of_le leₙ))

With these, we can write down the signature of our induction principle:

1
2
3
4
5
6
7

lemma two_le_orth_induction {P : ∀ m n, 2 ≤ m → 2 ≤ n → Prop}
    (baseₙ : ∀ m leₘ,       P m 2 leₘ (AtLeastTwo.prop))
    (baseₘ : ∀ n leₙ,       P 2 n (AtLeastTwo.prop) leₙ)
    (succ  : ∀ m n leₘ leₙ, P (m + 1) n (le_succ_of_le leₘ) leₙ →
                            P m (n + 1) leₘ (le_succ_of_le leₙ) →
                            P (m + 1) (n + 1) (le_succ_of_le leₘ) (le_succ_of_le leₙ)) :
    ∀ m n leₘ leₙ, P m n leₘ leₙ

If we can prove this lemma, for a general P, we will have a tool that allows us to perform inductive proofs of the shape described here, and we will be able to easily formalize our desired result!

We pattern-match on m and n, actually starting at zero and deriving a contradiction from the requirement that they be larger or equal 2:

1
2

| 0, _, le₀, _     => (two_ne_zero (eq_zero_of_le_zero le₀)).elim
| _, 0, _, le₀     => (two_ne_zero (eq_zero_of_le_zero le₀)).elim

For the successor pattern we either apply the base assumptions, if m or n are 2, or apply the recursive proof.

1
2
3
4
5
6
7
8

| m + 1, n + 1, le_sucₘ, le_sucₙ => by
   cases' le_sucₘ with _ leₘ
   · exact (baseₘ _ _)
   · cases' le_sucₙ with _ leₙ
     · exact (baseₙ _ _)
     · have Pₘ := two_le_orth_induction baseₙ baseₘ succ (m + 1) n (le_succ_of_le leₘ) leₙ
       have Pₙ := two_le_orth_induction baseₙ baseₘ succ m (n + 1) leₘ (le_succ_of_le leₙ)
       exact (succ m n _ _ Pₘ Pₙ)

The existence proof

So far, we have only proven a recursive statement about the Ramsey numbers. To prove our goal, we need a universal statement about existence:

1
2

theorem exists_N_ramseyProp {m n : ℕ} (leₘ : 2 ≤ m) (leₙ : 2 ≤ n) :
    (∃ N, ramseyProp N m n) := by

We can use our new induction principle to go from one to the other:

1

induction' m, n, leₘ, leₙ using two_le_orth_induction with m _ n _ m n leₘ leₙ ind_assump_rₘ ind_assump_rₙ

The infoview helpfully lists the three cases we have to prove now.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

3 goals

case baseₙ
m✝ n m : ℕ
leₘ✝ : 2 ≤ m
⊢ ∃ N, ramseyProp N m 2

case baseₘ
m n✝ n : ℕ
leₙ✝ : 2 ≤ n
⊢ ∃ N, ramseyProp N 2 n

case succ
m✝ n✝ m n : ℕ
leₘ : 2 ≤ m
leₙ : 2 ≤ n
rₘ : ∃ N, ramseyProp N (m + 1) n
rₙ : ∃ N, ramseyProp N m (n + 1)
⊢ ∃ N, ramseyProp N (m + 1) (n + 1)

The first two cases follow from lemmata we proved in the previous post establishing prerequisites.

1
2

· exact ⟨m, ramseyProp_two⟩
· exact ⟨n, ramseyProp_symm _ _ _ ramseyProp_two⟩

For the last case, a simple invocation of the recursive lemma suffices!

1
2

· have := R_bounded_recursive m n (zero_lt_of_lt leₘ) (zero_lt_of_lt leₙ) ind_assump_rₘ ind_assump_rₙ
  exact ⟨R(m, n + 1) + R(m + 1, n), this⟩

The binomial bounds

Our next objective is to confirm the upper bound using the binomial coefficient:

1
2

theorem R_le_choose {m n : ℕ} (m1 : 2 ≤ m) (n1 : 2 ≤ n) :
    R(m, n) ≤ (m + n - 2).choose (m - 1) := by

It turns out we can use the same induction principle as before!

1

induction' m, n, m1, n1 using two_le_orth_induction with m rₘ n _ m n leₘ leₙ ind_assump_rₘ ind_assump_rₙ

Again, the base cases were already established in separate lemmata before.

1
2
3

· have := Nat.le_of_eq (choose_succ_left m m (zero_lt_of_lt rₘ))
  simp_all [ind_start_R_two]
· simp_all [ind_start_two_R]

For the inductive step, we use the existence proof we just made and combine it with the recursive bound.

1
2
3
4

have Rm_ex : ∃ N, ramseyProp N m (n + 1) := exists_N_ramseyProp leₘ (le_add_right_of_le leₙ)
have Rn_ex : ∃ N, ramseyProp N (m + 1) n := exists_N_ramseyProp (le_add_right_of_le leₘ) leₙ
have N_has_ramseyProp : ramseyProp (R(m,n + 1) + R(m + 1,n)) (m + 1) (n + 1) :=
  R_bounded_recursive _ _ (zero_lt_of_lt leₘ) (zero_lt_of_lt leₙ) Rn_ex Rm_ex

This allows us to write down an inequality chain using the induction hypotheses to arrive at an expression of binomial coefficients!

1
2
3
4

calc R(m + 1, n + 1)
  _ ≤ R(m, n + 1) + R(m + 1, n)                                     := Nat.sInf_le N_has_ramseyProp
  _ ≤ R(m, n + 1)  + (m + 1 + n - 2).choose (m + 1 - 1)             := by simp_all [R_symm, ind_assump_rₘ]
  _ ≤ (m + (n + 1) - 2).choose (m - 1) + (m + 1 + n - 2).choose m   := by simp [ind_assump_rₙ]

The remainder of the proof is just applications of results about the binomial coefficient.

1
2
3

  _ = (m + (n + 1) - 2).choose (m - 1) + (m + (n + 1) - 2).choose m := by simp [add_assoc, add_comm n 1]
  _ = (m + (n + 1) - 2 + 1).choose m                                := (choose_succ_left (m+(n+1)-2) m (zero_lt_of_lt leₘ)).symm
  _ = (m + 1 + (n + 1) - 2).choose m                                := by rw [add_comm, add_comm m 1, add_assoc, ← Nat.add_sub_assoc (le_add_right_of_le leₘ)]

This concludes the proof of the binomial upper bound! The bound on \(R(k,k)\) now follows by another small inequality chain, with the most important ingredient from mathlib being choose_succ_le_two_pow [20735] .

1
2
3
4
5

lemma R_le_two_pow {k : ℕ} (h : 2 ≤ k) : R(k) ≤ 2 ^ (2 * k - 3) := by
  calc R(k)
    _ ≤ (2*k - 2).choose (k - 1)               := by simp [R_le_choose, h, Nat.two_mul]
    _ = ((2 * k - 2 - 1) + 1).choose (k - 1)   := congrFun (congrArg Nat.choose ((Nat.sub_eq_iff_eq_add (le_sub_of_add_le (le_of_succ_le (Nat.mul_le_mul_left 2 h)))).mp rfl)) (k - 1)
    _ ≤ 2 ^ (2 * k - 3)                        := choose_succ_le_two_pow