LemmaStatement: Literature-sourcedProof: AI-generatedSession-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.

Every finite colouring of $\mathbb N$ has an infinite colour class, in ZF

Statement

Every colouring of $\mathbb N$ (The natural numbers $\mathbb{N}$ (von Neumann)) by a nonempty finite set of colours has an infinite colour class in the sense of Finite, countably infinite, countable, uncountable. The finite notions are those of The cardinality $\lvert A\rvert$ of a finite set, and the result is stronger than any fixed finite pigeonhole conclusion 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.

Facts & Assumptions

Given: A function $c:\mathbb N\to C$ with $C$ nonempty and finite.

[L1]

A finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ (The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , and a sum over a finite index set splits along a partition).

[L2]

A subset of $\mathbb N$ is finite if it is bounded and countably infinite if it is unbounded (Every subset of an at most countable set is at most countable).

Proof

technique · contradiction

1.1

Suppose every fibre $c^{-1}(\{i\})$ , for $i\in C$ , is finite. These fibres are pairwise disjoint and their union is $\mathbb N$ .

assume-contra

2.1

Iterating [L1] over the finite set $C$ makes their union finite. This contradicts the infinitude of $\mathbb N$ , so at least one fibre is not finite. That fibre is a subset of $\mathbb N$ , and [L2] therefore makes it countably infinite.

step 1.1L1L2discharge-contradiction∎

Depends on

Used by

Infinite Ramsey theorem on ℕ: every finite colouring of [ℕ]ᵏ has an infinite monochromatic set, in ZF Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 67 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

I. B. Leader, Ramsey Theory, proof of Theorem 1 (standard reference, not scraped)

Every finite colouring of N\mathbb NN has an infinite colour class, in ZF