TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Special trees are exactly rationally special

Statement

For every set-theoretic tree $T$ , the following are equivalent:

$T$ is a countable union of antichains;
there is a map $q : T \to Q$ such that $s <_{T} t$ implies $q (s) < q (t)$ .

Thus the antichain-cover and strictly increasing rational-label conventions for a special tree agree. The equivalence includes empty and singleton trees and is provable in ZF.

Facts & Assumptions

Given: A set-theoretic tree $(T, <_{T})$ .

[F1]

A tree is special exactly when it is a countable union of antichains; a strictly increasing rational labeling implies specialness. Empty and singleton trees are special. Aronszajn, Suslin and special trees

[F2]

A nonempty set is at most countable exactly when it is the range of a surjection from $N$ , and every subset of an at most countable set is at most countable. Finite, countably infinite, countable, uncountable, A nonempty set is at most countable iff it is a surjective image of $N$ , Every subset of an at most countable set is at most countable

[F3]

Natural recursion and induction construct and verify finite lists and their length-by-length enumeration. The recursion theorem, The principle of mathematical induction

[F4]

Every nonempty subset of $N$ has a least element. The well-ordering principle

[F5]

Every at most countable linear order has a strictly order-preserving injection into $Q$ . Every countable linear order embeds in the rationals

[F6]

A linear order is a partial order in which every two elements are comparable. Partial order and partially ordered set

Proof

technique · direct

1.1

Assume first that $q : T \to Q$ is strictly increasing on comparable nodes. By [F1] it witnesses that $T$ is special, and the same fact gives a countable antichain cover. This also covers $T = \emptyset$ and a singleton.

assume-hypF1

1.2

Conversely suppose $T = ⋃_{n \in N} A_{n}$ with every $A_{n}$ an antichain. Put $c (t) = \min {n : t \in A_{n}}$ ; [F4] makes this a function, its fibers $B_{n} = {t : c (t) = n}$ are antichains, and they partition $T$ . For $t \in T$ define $g_{t} : N \to {0, 1}$ by $g_{t} (k) = 1$ exactly when $k \leq c (t)$ and some $u \leq_{T} t$ has $c (u) = k$ . Thus $g_{t} (k) = 0$ for $k > c (t)$ , so $g_{t}$ has finite support.

assume-hypF1F4construct

1.3

Let $G = {g_{t} : t \in T}$ and lexicographically order distinct members at their least differing coordinate, with $0 < 1$ . The least coordinate exists by [F4], and the usual first-difference argument proves trichotomy and transitivity, so [F6] makes this a linear order. The set of all finite-support binary sequences has a specified surjective enumeration: list the finite binary words by increasing length and lexicographically within each finite block, using recursion and induction, and extend each word by zeros. Every finite-support sequence occurs, including the all-zero sequence from the empty word. Hence that set is at most countable by [F2], and so is its subset $G$ .

F2F3F4F6

2.1

Fix $s <_{T} t$ and write $m = c (s)$ and $n = c (t)$ ; the antichain fibers give $m \neq n$ . At coordinate $n$ , $g_{t} (n) = 1$ . If $n > m$ then $g_{s} (n) = 0$ by its cutoff; if $n < m$ and $g_{s} (n) = 1$ , some $u \leq_{T} s <_{T} t$ has color $n = c (t)$ , contradicting that $B_{n}$ is an antichain. Hence $g_{s} (n) = 0$ in either case. Let $p$ be the least coordinate where $g_{s}$ and $g_{t}$ differ; [F4] gives it and the coordinate $n$ just found gives $p \leq n$ . If $g_{s} (p) = 1$ and $g_{t} (p) = 0$ , some $u \leq_{T} s$ has color $p$ , while $p \leq n = c (t)$ and $u \leq_{T} t$ would make $g_{t} (p) = 1$ , a contradiction. Therefore $g_{s} (p) = 0 < 1 = g_{t} (p)$ .

step 1.2F4

3.1

By [F5] choose a strict order embedding $h : G \to Q$ and define $q (t) = h (g_{t})$ . If $s <_{T} t$ , step 2.1 says $g_{s}$ is lexicographically below $g_{t}$ , so $q (s) < q (t)$ . This proves the reverse implication; together with step 1.1 it proves the equivalence. All minima and enumerations used specified least or recursive rules, so no choice principle is used.

step 1.1step 2.1step 1.3F5∎

Remarks

The required first-difference bound is $p \leq c (t)$ , not in general $p \leq \min (c (s), c (t))$ . For example, if $c (s) = 0 < c (t) = 1$ and there are no earlier colors, the first difference can occur at coordinate $1$ . The proof above supplies the missing derivation of $p \leq c (t)$ in Monk's second case.
Injectivity of $t \mapsto g_{t}$ is neither claimed nor needed: step 2.1 proves distinct codes precisely for comparable distinct nodes, which is exactly what the rational specialization requires.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Monk, Set theory following Jech, Proposition 9.37 and complete proof, printed pp. 86-87 (standard reference, not scraped)