CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$R (s, t) \leq R (s - 1, t) + R (s, t - 1)$ for $s, t \geq 2$ , and $R (k, k) \leq (\binom{2 k - 2}{k - 1}) \leq 2^{2 k - 2}$

Statement

For $s, t \geq 2$ ,

$R (s, t) \leq R (s - 1, t) + R (s, t - 1) .$

For every positive $k$ ,

$R (k, k) \leq (\binom{2 k - 2}{k - 1}) \leq 2^{2 k - 2} .$

Here $R$ is The off-diagonal Ramsey number $R (s, t)$ as the least $N$ with $N \to (s, t)^{2}$ , for positive $s, t$ and the binomial coefficient is The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ; the first diagonal inequality is the specialization of Finite graph Ramsey theorem: $(\binom{s + t - 2}{s - 1}) \to (s, t)^{2}$ for all positive $s, t$ .

Facts & Assumptions

Given: Positive naturals $s, t, k$ , with $s, t \geq 2$ for the recursion.

[L1]

If $m \to (s - 1, t)^{2}$ and $n \to (s, t - 1)^{2}$ , then $m + n \to (s, t)^{2}$ for $s, t \geq 2$ (If $m \to (s - 1, t)^{2}$ and $n \to (s, t - 1)^{2}$ , then $m + n \to (s, t)^{2}$ for $s, t \geq 2$ ).

[L2]

For all $x, y \in R$ and every $n \in N$ , the binomial theorem expands $(x + y)^{n}$ as the sum of its binomial terms (The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ ).

Proof

technique · direct

1.1

The numbers $R (s - 1, t)$ and $R (s, t - 1)$ satisfy the two hypotheses of [L1]. Hence their sum arrows to $(s, t)$ , and leastness in the definition of $R (s, t)$ gives the recursion inequality.

2.1

The finite binomial theorem gives $R (k, k) \leq (\binom{2 k - 2}{k - 1})$ . In [L2] put $x = y = 1$ and $n = 2 k - 2$ ; every summand is nonnegative, so the single central coefficient is at most their sum $2^{2 k - 2}$ .

L2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. Fox et al., Graph Ramsey Theory, Section 2.1 (standard reference, not scraped)

R(s,t)≤R(s−1,t)+R(s,t−1)R(s,t)≤R(s−1,t)+R(s,t−1) for s,t≥2s,t≥2, and R(k,k)≤(2k−2k−1)≤22k−2R(k,k)≤(k−12k−2​)≤22k−2