ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Cantor diagonal construction misses every prescribed list of binary sequences

Example

Given any function $s : N \to {0, 1}^{N}$ , write $s_{n} = s (n)$ and define $d : N \to {0, 1}$ by $d (n) = 1$ if $s_{n} (n) = 0$ and $d (n) = 0$ if $s_{n} (n) = 1$ . Then $d$ differs from $s_{n}$ at coordinate $n$ for every $n$ , so $d$ is outside the range of $s$ . In particular no prescribed list of binary sequences is onto, and since ${0, 1}^{N}$ is nonempty this gives once more that it is uncountable (Finite, countably infinite, countable, uncountable, A nonempty set is at most countable iff it is a surjective image of $N$ ). This is a direct choice-free diagonal construction, not a decimal expansion argument; no sum, limit or real digit convention is required.

Facts & Assumptions

Given: The naturals $N$ with $0 = \emptyset$ and $1 = σ (0)$ (The natural numbers $N$ (von Neumann)), the unordered pair ${0, 1}$ (The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ ), the set of binary sequences ${0, 1}^{N}$ (The set $B^{A}$ of all functions $A \to B$ , For sets $A$ and $B$ the collection of all functions $A \to B$ is a set, being a subset of $P (A \times B)$ ), and an arbitrary function $s : N \to {0, 1}^{N}$ .

[F1]

$s (n)$ is a function $N \to {0, 1}$ , so $s (n) (n) \in {0, 1}$ and the expression $s_{n} (n)$ is meaningful; $t \in {0, 1}$ exactly when $t = 0$ or $t = 1$ (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain, The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ ).

[F2]

$0 \neq 1$ (The von Neumann naturals form a Peano system).

[F3]

Separation: for a set $X$ and a property of its elements, ${z \in X : φ (z)}$ is a set whose elements are exactly those $z \in X$ with the property (The Axiom Schema of Separation: for each formula $φ$ , $\forall \overset{ˉ}{p} \forall x \exists y \forall z (z \in y \leftrightarrow (z \in x \land φ (z, \overset{ˉ}{p})))$ ); ordered pairs lie in $X \times Y$ (The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ ).

[F4]

Two functions with the same domain are equal exactly when they take the same value at every point of that domain; and a function $s$ is onto its codomain when every element of the codomain is a value of $s$ (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain, Injection, surjection, bijection).

[F5]

A nonempty at most countable set has a surjection from $N$ (A nonempty set is at most countable iff it is a surjective image of $N$ , Finite, countably infinite, countable, uncountable); ${0, 1}^{N}$ is nonempty, for instance the constant function $n \mapsto 0$ is an element of it.

Verification

technique · direct

1.1F1F2F3givenconstruct

The set $D : = {(n, v) \in N \times {0, 1} : (s (n) (n) = 0 \land v = 1) \lor (s (n) (n) = 1 \land v = 0)}$ exists by Separation and is a function $d : N \to {0, 1}$ with $d (n) = 1$ when $s (n) (n) = 0$ and $d (n) = 0$ when $s (n) (n) = 1$ . Indeed, for each $n$ the value $s (n) (n)$ is $0$ or $1$ by [F1], the alternatives $s (n) (n) = 0$ and $s (n) (n) = 1$ are mutually exclusive by [F2], and each branch assigns exactly one value; both values lie in ${0, 1}$ .

2.1step 1.1F1F2

For every $n \in N$ one has $d (n) \neq s (n) (n)$ . If $s (n) (n) = 0$ then $d (n) = 1 \neq 0$ by [F2]; if $s (n) (n) = 1$ then $d (n) = 0 \neq 1$ by [F2]. These are the only two cases by [F1].

3.1step 2.1F4

For every $n$ the functions $d$ and $s (n)$ differ, because at the point $n$ their values differ by step 2.1; hence $d$ is not a value of $s$ , that is, $d$ is outside the range of $s$ . So $s$ is not onto ${0, 1}^{N}$ , and no prescribed list of binary sequences is onto.

4.1step 3.1F5

Consequently ${0, 1}^{N}$ is uncountable: it is nonempty by [F5], so if it were at most countable, [F5] would produce a surjection $N \to {0, 1}^{N}$ , which step 3.1 forbids.

5.1step 3.1step 4.1∎

Therefore every list of binary sequences omits at least the complementary diagonal sequence $d$ constructed above, and the set of binary sequences is uncountable. The only set introduced is $D$ , separated from $N \times {0, 1}$ by a condition that determines each value uniquely; no element is selected from a nonempty family, so no choice principle is used.

Remarks

The construction complements the diagonal entry: at coordinate $n$ it looks at the $n$ -th value of the $n$ -th listed sequence and writes the other symbol. Every listed sequence is contradicted at its own index, so the resulting sequence cannot be on the list.
This is the literal diagonal argument that accompanies the characteristic-function bijection of The set of binary sequences is equinumerous with $P (N)$ , hence uncountable; there the uncountability was transferred from $P (N)$ , here it is produced directly from the diagonal sequence, with no appeal to decimal expansions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

35 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

John K. Hunter, An Introduction to Real Analysis (complete author-hosted lecture notes) (standard reference, not scraped)