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.

König's infinity lemma: an ordered finitely branching tree with a node at every level has an infinite branch, in ZF

Statement

Let $T$ be an ordered finitely branching tree of finite sequences (Rooted trees of finite sequences, levels, branches, and finite branching, with ordered finite successor sets). If every level $T_{n}$ is nonempty, then $T$ has an infinite branch. The branch is constructed in ZF by least successors and natural recursion (The recursion theorem); no choice principle is used. Its natural indexing agrees with the convention of Finite, countably infinite, countable, uncountable, and the elementary induction below uses The principle of mathematical induction.

Facts & Assumptions

Given: An ordered finitely branching tree $T$ with a node at every level.

[L1]

Every nonempty subset $S \subseteq N$ has a least element (The well-ordering principle).

[L2]

Given a set $A$ , an element $a \in A$ , and a function $f : A \to A$ , natural recursion supplies a unique sequence beginning at $a$ and iterating $f$ (The recursion theorem).

Proof

technique · constructive

1.1

Call a node viable if it has descendants at arbitrarily high levels. The root is viable: if each of its finitely many successors had descendants only up to some level, the maximum of those finitely many bounds would bound the whole tree, contrary to the existence of a node at every level.

givenconstruct

2.1

Every viable node has a viable immediate successor. Otherwise all its finitely many successors would have bounded descendant height, and the maximum of their bounds would contradict viability. The viable successor labels form a nonempty set of naturals, so [L1] gives a unique least one.

step 1.1L1

3.1

On the set of viable nodes, send each node to its least viable successor from step 2.1. Apply [L2] from the root. Every finite initial segment produced is a node of $T$ , and at stage $n$ it has length $n$ . Thus the recursive sequence is an infinite branch.

step 2.1L2discharge-construct∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 36 results over 17 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, compactness proof after Corollary 3 (standard reference, not scraped)