Alphabeta MathHow 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.
The finite uniform Ramsey theorem follows a second time from the infinite theorem by a finitely branching tree of bad finite colourings
Statement
The existence conclusion of For positive there is an such that every -colouring of has a monochromatic -element set also follows from Infinite Ramsey theorem on : every finite colouring of has an infinite monochromatic set, in ZF by applying König's lemma to the tree of bad finite colourings. The meanings of colouring and homogeneity are those of Finite colourings of -element subsets, monochromatic sets, and the arrow notations and , and finiteness of each level follows from The set of functions between finite sets is finite, with .
Facts & Assumptions
Given: Positive naturals and, for contradiction, a bad -colouring of with no monochromatic -set for every natural .
An ordered finitely branching tree with a node at every level has an infinite branch, in ZF (König's infinity lemma: an ordered finitely branching tree with a node at every level has an infinite branch, in ZF).
Every finite colouring of has an infinite monochromatic set, in ZF (Infinite Ramsey theorem on : every finite colouring of has an infinite monochromatic set, in ZF).
Proof
Suppose no finite witness exists. Form a tree whose level- nodes are the bad colourings of , ordered by extension. Restricting a bad colouring remains bad, every level is nonempty by the supposition, and every node has only finitely many one-level extensions. Order those extensions lexicographically by their finite colour tables.
By [L1] the tree has a coherent branch. The union of its compatible finite functions is a well-defined -colouring of , and every finite restriction on the branch has no monochromatic -set.
Apply [L2] to the union colouring and take the first elements of its infinite monochromatic set. They lie below some , so they form a monochromatic -set in the level- branch node, contradicting its badness. Therefore a finite witness exists.
Depends on
- König's infinity lemma: an ordered finitely branching tree with a node at every level has an infinite branch, in ZF
- Infinite Ramsey theorem on $\mathbb N$: every finite colouring of $[\mathbb N]^k$ has an infinite monochromatic set, in ZF
- For positive $k,c,r$ there is an $N$ such that every $c$-colouring of $[N]^k$ has a monochromatic $r$-element set
- Finite colourings of $k$-element subsets, monochromatic sets, and the arrow notations $N\to(s,t)^2$ and $N\to(r)^k_c$
- 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}$
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: 61 results over 19 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, Corollary 3 (standard reference, not scraped)