CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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)\le R(s-1,t)+R(s,t-1)$ for $s,t\ge2$ , and $R(k,k)\le\binom{2k-2}{k-1}\le2^{2k-2}$

Statement

For $s,t\ge2$ ,

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

For every positive $k$ ,

$R(k,k)\le\binom{2k-2}{k-1}\le2^{2k-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} := \lvert [n]^{k}\rvert$ ; 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\ge2$ 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\ge2$ (If $m\to(s-1,t)^2$ and $n\to(s,t-1)^2$ , then $m+n\to(s,t)^2$ for $s,t\ge2$ ).

[L2]

For all $x, y \in \mathbb{R}$ and every $n \in \mathbb{N}$ , the binomial theorem expands $(x+y)^n$ as the sum of its binomial terms (The binomial theorem in $\mathbb{R}$ : $(x+y)^{n} = \sum_{k<n+1} \iota\!\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)\le\binom{2k-2}{k-1}$ . In [L2] put $x=y=1$ and $n=2k-2$ ; every summand is nonnegative, so the single central coefficient is at most their sum $2^{2k-2}$ .

L2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 79 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)\le R(s-1,t)+R(s,t-1)R(s,t)≤R(s−1,t)+R(s,t−1) for s,t≥2s,t\ge2s,t≥2, and R(k,k)≤(2k−2k−1)≤22k−2R(k,k)\le\binom{2k-2}{k-1}\le2^{2k-2}R(k,k)≤(k−12k−2​)≤22k−2