TheoremStatement: 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.

For positive $k,c,r$ there is an $N$ such that every $c$ -colouring of $[N]^k$ has a monochromatic $r$ -element set

Statement

For all positive natural numbers $k,c,r$ , some natural number $N$ satisfies

$N\to(r)^k_c.$

Equivalently, every $c$ -colouring of $[N]^k$ has a monochromatic $r$ -element set in the sense of Finite colourings of $k$ -element subsets, monochromatic sets, and the arrow notations $N\to(s,t)^2$ and $N\to(r)^k_c$ . Finite cardinalities and the induction are those of The cardinality $\lvert A\rvert$ of a finite set and The principle of mathematical induction.

Facts & Assumptions

Given: Positive natural numbers $k,c,r$ ; finite pigeonhole is available from If $\lvert A\rvert > k\lvert B\rvert$ then every $f : A \to B$ has a fibre with more than $k$ elements, and for nonempty $B$ some fibre has at least $\lceil \lvert A\rvert / \lvert B\rvert\rceil$ elements.

[L1]

For all positive $s,t$ , $\binom{s+t-2}{s-1}\to(s,t)^2$ (Finite graph Ramsey theorem: $\binom{s+t-2}{s-1}\to(s,t)^2$ for all positive $s,t$ ).

[L2]

If $A$ and $B$ are finite, then $A^{B}$ is finite and $\lvert A\rvert^{\lvert B\rvert}=\lvert A^{B}\rvert$ (The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}$ ).

Proof

technique · induction

1.1

If $r=1$ or $c=1$ , any sufficiently large finite set works. For $k=1$ , $N=c(r-1)+1$ works by finite pigeonhole. For $k=2$ , repeatedly group one colour against all remaining colours and apply [L1]; induction on $c$ gives a finite multicolour graph witness for every target $r$ .

baseL1

1.2

Assume $k\ge3$ and that the theorem is known for $(k-1)$ -subsets with every finite colour and target parameter. Put $M=c(r-1)+1$ . Choose finite reservoir sizes backwards by $q_M=1$ and, for $i<M$ , let $q_i$ be one more than a $(k-1)$ -uniform Ramsey witness for target $q_{i+1}$ and $c$ colours, which exists by the induction hypothesis.

2.1

Starting with a $q_0$ -element set, choose its least vertex $x_0$ . Colour each $(k-1)$ -subset $A$ of the remaining reservoir by the colour of $A\cup\{x_0\}$ , and restrict to a homogeneous $q_1$ -element reservoir. Repeat. After $M$ stages there are vertices $x_0,\ldots,x_{M-1}$ and colours $d_0,\ldots,d_{M-1}$ such that every $k$ -set of chosen vertices whose least member is $x_i$ has colour $d_i$ .

step 1.2L2construct

3.1

Finite pigeonhole gives indices $i_1<\cdots<i_r$ for which $d_{i_1}=\cdots=d_{i_r}$ . Every $k$ -subset of $\{x_{i_1},\ldots,x_{i_r}\}$ has least element $x_{i_j}$ for some $j$ , hence has this common colour by step 2.1. This is a monochromatic $r$ -set.

step 2.1

4.1

The bases and the step from $(k-1)$ to $k$ prove the assertion for every positive $k,c,r$ .

step 1.1step 3.1discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 70 results over 24 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

R. Diestel, Graph Theory, 6th ed., Theorem 9.1.3 (standard reference, not scraped)
I. B. Leader, Ramsey Theory, Corollary 3 (standard reference, not scraped)

For positive k,c,rk,c,rk,c,r there is an NNN such that every ccc-colouring of [N]k[N]^k[N]k has a monochromatic rrr-element set