Erdős–Szekeres 1935 upper bound for the diagonal Ramsey number

Statement (Erdős–Szekeres 1935): For every k : ℕ, the diagonal Ramsey number satisfies Combinatorics.hypergraphRamsey 2 k ≤ 4 ^ k.

Proof sketch. Use the symmetric recursion R(s, t) ≤ R(s-1, t) + R(s, t-1) with base cases R(0, t) = R(s, 0) = 1. Induction on s + t then gives R(s, t) ≤ C(s+t, s); for s = t = k this is R(k, k) ≤ C(2k, k) ≤ 4 ^ k (the Catalan-like central binomial coefficient bound).

The whole argument is phrased directly on the Mathlib-style coloring data c : Finset (Fin m) → Bool of 2-element subsets — no auxiliary "edge colouring" structure is introduced.

Reference: [ES35] Erdős, P. and Szekeres, G. (1935). "A combinatorial problem in geometry." Compositio Math. 2, pp. 463–470.

theorem Combinatorics.Diagonal.central_binomial_le_four_pow (n : ℕ) : (2 * n).choose n ≤ 4 ^ n

Central binomial bound (Mathlib wrapper). C(2n, n) ≤ 4 ^ n.

This specialises Nat.choose_middle_le_pow : (2n+1).choose n ≤ 4^n by observing that (2n).choose n ≤ (2n+1).choose n via the monotonicity lemma Nat.choose_le_succ.

Off-diagonal Ramsey via a subset-indexed predicate

Rather than introduce an auxiliary edge-colouring structure, we phrase the off-diagonal Ramsey statement as a property of an arbitrary Finset (Fin m) of sufficient cardinality inside a Bool-valued coloring of all subsets of Fin m. We only ever query the coloring on 2-element subsets. This setup matches the shape of Combinatorics.hypergraphRamsey 2 directly.

def Combinatorics.Diagonal.HasRamseyProperty (N s t : ℕ) : Prop

HasRamseyProperty N s t asserts: for every m, every coloring c : Finset (Fin m) → Bool, and every V : Finset (Fin m) with V.card ≥ N, the subset V contains either a subset of size s whose 2-element subsets are all false-coloured, or a subset of size t whose 2-element subsets are all true-coloured.

This is the "off-diagonal Ramsey number does not exceed N" form of the classical Erdős–Szekeres Ramsey recurrence, packaged in the same shape used by Combinatorics.hypergraphRamsey.

Equations

• One or more equations did not get rendered due to their size.

theorem Combinatorics.Diagonal.HasRamseyProperty.mono {N N' s t : ℕ} (hNN' : N ≤ N') (h : HasRamseyProperty N s t) : HasRamseyProperty N' s t

Monotonicity. If N ≤ N' then HasRamseyProperty N s t → HasRamseyProperty N' s t.

theorem Combinatorics.Diagonal.hasRamseyProperty_zero_left (N t : ℕ) : HasRamseyProperty N 0 t

Base case s = 0. Any V contains an empty false-monochromatic set.

theorem Combinatorics.Diagonal.hasRamseyProperty_zero_right (N s : ℕ) : HasRamseyProperty N s 0

Base case t = 0. Any V contains an empty true-monochromatic set.

theorem Combinatorics.Diagonal.forall_two_subset_singleton {m : ℕ} (v : Fin m) (b : Bool) (c : Finset (Fin m) → Bool) (e : Finset (Fin m)) : e ⊆ {v} → e.card = 2 → c e = b

A singleton has no 2-element subsets, hence is monochromatic of any colour.

theorem Combinatorics.Diagonal.hasRamseyProperty_one_left (t : ℕ) : HasRamseyProperty 1 1 t

Base case s = 1. Any nonempty V contains a singleton false-monochromatic set.

theorem Combinatorics.Diagonal.hasRamseyProperty_one_right (s : ℕ) : HasRamseyProperty 1 s 1

Base case t = 1. Any nonempty V contains a singleton true-monochromatic set.

theorem Combinatorics.Diagonal.card_false_true_split {m : ℕ} (c : Finset (Fin m) → Bool) (V : Finset (Fin m)) {v : Fin m} (hv : v ∈ V) : {u ∈ V.erase v | c {v, u} = false}.card + {u ∈ V.erase v | c {v, u} = true}.card = V.card - 1

Pigeonhole step: splitting V \ {v} by colour. For any vertex v ∈ V, the set V.erase v partitions into false-neighbours of v and true-neighbours of v, and the cardinalities sum to V.card - 1.

theorem Combinatorics.Diagonal.HasRamseyProperty.step {Ns Nt s t : ℕ} (hs : HasRamseyProperty Ns s (t + 1)) (ht : HasRamseyProperty Nt (s + 1) t) (hNs : 1 ≤ Ns) : HasRamseyProperty (Ns + Nt) (s + 1) (t + 1)

Recurrence. If HasRamseyProperty Ns s (t+1) and HasRamseyProperty Nt (s+1) t hold, then HasRamseyProperty (Ns + Nt) (s+1) (t+1) holds.

This is the core Erdős–Szekeres 1935 pigeonhole step: pick any vertex v ∈ V, split V.erase v into false-neighbours R_v and true-neighbours B_v; by pigeonhole |R_v| ≥ Ns or |B_v| ≥ Nt. In the first case, invoke HasRamseyProperty Ns s (t+1) on R_v: either we get a false-mono K_s on R_v (extend by v to a false-mono K_{s+1} on V), or a true-mono K_{t+1} on R_v ⊆ V (done). The second case is symmetric.

theorem Combinatorics.Diagonal.hasRamseyProperty_choose (s t : ℕ) : HasRamseyProperty ((s + t).choose s) s t

Binomial bound via Erdős–Szekeres induction. HasRamseyProperty (Nat.choose (s + t) s) s t for all s, t.

theorem Combinatorics.hypergraphRamsey_two_le_four_pow (k : ℕ) : hypergraphRamsey 2 k ≤ 4 ^ k

Erdős–Szekeres 1935 in hypergraphRamsey form: Combinatorics.hypergraphRamsey 2 k ≤ 4 ^ k for all k.

Proof. Diagonal.hasRamseyProperty_choose applied at s = t = k and the full vertex set V = Finset.univ of Fin (C(2k, k)) shows that C(2k, k) is a member of the defining set of hypergraphRamsey 2 k, hence by Nat.sInf_le we get hypergraphRamsey 2 k ≤ C(2k, k); the central binomial bound C(2k, k) ≤ 4 ^ k closes the result.