Pipeline-generated

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.

✓ 1 result · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 1 also cleared it.

Dependent Choice and the Complete-Metric Baire Theorem — Examples

1 · Prerequisites

2 · Summary

A natural-successor relation makes the sequence-space converse concrete. A finite-prefix extension meets an open dense set, and an explicit sequence lies in every successor-occurrence set while failing the adjacent-chain condition. Computing its least witness indices yields the required successor chain in ZF.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09Open item page →

Blair's sequence space for a serial relation

Example

Work in ZF with $A = ω$ and $i R j$ meaning $j = i + 1$ . On the complete sequence space $Y = ω^{ω}$ use the reciprocal first-difference metric. Then $U_{n} = {g : (\exists m) g (m) = g (n) + 1}$ .

Starting with the prefix $(2, 0, 2)$ , appending $3$ at coordinate $3$ and then a constant zero tail produces a point of $U_{0}$ in that cylinder. Define a second sequence by $f (0) = 2$ , $f (1) = 0$ , $f (2) = 2$ , $f (3) = 1$ , and $f (n) = n - 1$ for $n \geq 4$ . Thus $f = (2, 0, 2, 1, 3, 4, 5, \dots)$ belongs to every $U_{n}$ but is not an adjacent $R$ -chain. Least-index extraction from coordinate $0$ gives indices $0, 4, 5, 6, \dots$ and values $2, 3, 4, 5, \dots$ .

Facts & Assumptions

Given: The explicit $A, R, f$ and prefix in the example; coordinates start at zero.

[F1]

The reciprocal metric on $ω^{ω}$ is complete and its finite-prefix cylinders are nonempty clopen basic sets (Discrete sequence spaces are complete in ZF).

[F2]

For a serial relation the sets $U_{n}$ encode occurrence of a successor somewhere in the range and are open dense (Successor-occurrence sets of a serial relation are open and dense).

[F3]

The converse Baire-to-DC theorem uses least witness indices followed by natural recursion to extract a chain from a point in all $U_{n}$ (The complete-metric Baire principle implies Dependent Choice over ZF).

Verification

1.1F1F2given

The relation is serial because for each $i \in ω$ , $i + 1 \in ω$ and $i R (i + 1)$ . Thus the sequence-space and open-dense conclusions apply. Let $g = (2, 0, 2, 3, 0, 0, \dots)$ and $h = (2, 0, 2, 0, 0, 0, \dots)$ . They extend the prefix, their first disagreement is at coordinate $3$ , and $d (g, h) = 1 / (3 + 1) = 1 / 4$ . Since $g (3) = 3 = g (0) + 1$ , $g \in U_{0}$ .

1.2F2given

For $f$ the successor witnesses are explicit: at $n = 0$ or $n = 2$ , use $m = 4$ since $f (4) = 3 = 2 + 1$ ; at $n = 1$ , use $m = 3$ since $f (3) = 1 = 0 + 1$ ; at $n = 3$ , use $m = 0$ since $f (0) = 2 = 1 + 1$ ; and at every $n \geq 4$ , use $m = n + 1$ since $f (n + 1) = n = f (n) + 1$ . These cases cover all naturals, proving $f \in ⋂_{n} U_{n}$ . But $f (1) = 0 \neq 3 = f (0) + 1$ , so $f (0) R f (1)$ fails.

2.1F3step 1.2algebra

Let $q (i) = \min {j : f (j) = f (i) + 1}$ . The displayed values give $q (0) = q (2) = 4$ , $q (1) = 3$ , and $q (3) = 0$ : the first occurrences of $3, 1, 2$ are at $4, 3, 0$ , respectively. For $i \geq 4$ , $f (i) + 1 = i \geq 4$ cannot occur among coordinates $0, 1, 2, 3$ , whose values are $2, 0, 2, 1$ , and in the tail $f (j) = j - 1$ it occurs only at $j = i + 1$ . Thus $q (i) = i + 1$ for $i \geq 4$ . Recursing from $k (0) = 0$ gives $k (1) = 4$ and $k (t) = t + 3$ for every $t \geq 1$ , because $q (t + 3) = t + 4$ . Hence $f (k (0)) = 2$ and $f (k (t)) = t + 2$ for $t \geq 1$ , so successive extracted values differ by exactly one.

3.1F2step 1.2step 2.1∎

For arbitrary serial $R$ , membership in every $U_{n}$ says exactly that each coordinate value has an $R$ -successor somewhere among the sequence's values. It does not specify the next coordinate. The explicit failure at coordinates zero and one demonstrates that distinction, and the computed least-index extraction demonstrates how to obtain a chain. The backward witness $q (3) = 0$ also shows why unrestricted witness indices need not increase. These computations required no CM-Baire assumption to produce this particular $f$ .