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.

Canonical Ramsey theorem for pairs: on an infinite subset a colouring is constant, injective, left-dependent, or right-dependent

Statement

Let $c:[\mathbb N]^2\to C$ be a colouring by an arbitrary set of colours. There is an infinite $M\subseteq\mathbb N$ (Finite, countably infinite, countable, uncountable) on which exactly one of the following canonical descriptions holds, writing every pair as $i<j$ :

constant: all pairs have one colour;
injective: distinct pairs have distinct colours (Injection, surjection, bijection);
left-dependent: $c(\{i,j\})=c(\{k,l\})$ if and only if $i=k$ ;
right-dependent: $c(\{i,j\})=c(\{k,l\})$ if and only if $j=l$ .

The finite auxiliary colourings below use the homogeneous-set convention of Finite colourings of $k$ -element subsets, monochromatic sets, and the arrow notations $N\to(s,t)^2$ and $N\to(r)^k_c$ .

Facts & Assumptions

Given: An arbitrary colouring $c:[\mathbb N]^2\to C$ .

[L1]

Every finite colouring of $[\mathbb N]^k$ has an infinite monochromatic set, in ZF (Infinite Ramsey theorem on $\mathbb N$ : every finite colouring of $[\mathbb N]^k$ has an infinite monochromatic set, in ZF).

Proof

technique · direct

1.1

Colour each $i<j<k<l$ according as $c(ij)=c(kl)$ . By [L1], thin to an infinite set on which this answer is constant. If it is yes, any two pairs can be compared through a third pair lying to their right, so $c$ is constant. Henceforth the answer is no: separated pairs have different colours.

2.1

On the set from step 1.1, thin by [L1] for the relation $c(il)=c(jk)$ on $i<j<k<l$ . The constant answer cannot be yes: on six ordered points it would give $c(x_2x_3)=c(x_1x_6)=c(x_4x_5)$ , contradicting step 1.1. Thus every such nested pair has different colours.

step 1.1L1

2.2

Thin again for the relation $c(ik)=c(jl)$ . A constant yes answer on six points similarly gives $c(x_1x_3)=c(x_2x_5)=c(x_4x_6)$ , again contradicting step 1.1. Thus crossing pairs have different colours.

step 1.1L1

2.3

Successively thin triples so that each of the relations $c(ij)=c(ik)$ , $c(ik)=c(jk)$ and $c(ij)=c(jk)$ has a constant truth value for $i<j<k$ . The last relation cannot be always true, since four points would then make two separated pairs equal by transitivity.

step 1.1L1

3.1

If both of the first two relations were always true, the last would also be true, which step 2.3 excludes. If only the first is always true, equality of colours is exactly equality of left endpoints; if only the second is always true, it is exactly equality of right endpoints. The converse implications follow from the corresponding always-true relation, while pairs with different relevant endpoints are covered by steps 1.1, 2.1, and 2.2 and the always-false triple relations.

step 1.1step 2.1step 2.2step 2.3

4.1

If both first relations are always false, any two distinct pairs are separated, nested, crossing, or share exactly one endpoint; steps 1.1, 2.1, and 2.2 and the triple relations show their colours differ, so $c$ is injective. Together with the constant case and step 3.1, this yields one of the four canonical forms on an infinite set.

step 1.1step 2.1step 2.2step 2.3step 3.1∎

Depends on

Used by

Constant, injective, left-dependent, and right-dependent pair colourings all occur on ℕ Example

Dependency tree · next 3 levels

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

I. B. Leader, Ramsey Theory, Theorem 4 (standard reference, not scraped)