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.

The integers are countably infinite: $Z \approx N$

Example

$Z \approx N$ (Equinumerous sets, $A \approx B$ and $A ⪯ B$ ): the integers are countably infinite (Finite, countably infinite, countable, uncountable). The argument is the two-injection route of The Schröder-Bernstein theorem rather than a closed formula. The map $n \mapsto [(n, 0)]$ is injective (The naturals embed in the integers), and the quotient map $π (a, b) = [(a, b)]$ is a surjective function $N \times N \to Z$ (Let $\sim$ be an equivalence relation on $A$ with quotient map $π : A \to A / \sim$ , and let $f : A \to B$ . There is a function $g : A / \sim \to B$ with $g \circ π = f$ if and only if $a \sim a^{'}$ implies $f (a) = f (a^{'})$ ; and such a $g$ is then unique, The integers as equivalence classes of pairs of naturals); composing $π$ with the bijection $β$ of $N \times N \approx N$ exhibits $Z$ as a surjective image of $N$ , and A nonempty set is at most countable iff it is a surjective image of $N$ then supplies an injection $Z \to N$ explicitly as $j (x) = \min {k \in N : π (β (k)) = x}$ . Every ingredient is a definition or a canonical least element, so no choice principle is used; A product of two at most countable sets is at most countable then gives that $Z \times Z$ is at most countable as well.

Facts & Assumptions

Given: The naturals $N$ (The natural numbers $N$ (von Neumann)), the integers $Z = (N \times N) / \sim$ with classes $[(a, b)]$ for the equivalence relation $(a, b) \sim (c, d) ⟺ a + d = b + c$ (The integers as equivalence classes of pairs of naturals, The integer-defining relation is an equivalence relation), the embedding $n \mapsto [(n, 0)]$ of $N$ in $Z$ (The naturals embed in the integers), and the quotient map $π = {((a, b), C) : C = [(a, b)]}$ (Let $\sim$ be an equivalence relation on $A$ with quotient map $π : A \to A / \sim$ , and let $f : A \to B$ . There is a function $g : A / \sim \to B$ with $g \circ π = f$ if and only if $a \sim a^{'}$ implies $f (a) = f (a^{'})$ ; and such a $g$ is then unique).

[F1]

The map $n \mapsto [(n, 0)]$ is injective (The naturals embed in the integers).

[F2]

$π$ is a surjective function $N \times N \to Z$ with $π (a, b) = [(a, b)]$ (Let $\sim$ be an equivalence relation on $A$ with quotient map $π : A \to A / \sim$ , and let $f : A \to B$ . There is a function $g : A / \sim \to B$ with $g \circ π = f$ if and only if $a \sim a^{'}$ implies $f (a) = f (a^{'})$ ; and such a $g$ is then unique, The integers as equivalence classes of pairs of naturals).

[F3]

$N \times N \approx N$ : there is a bijection $β : N \to N \times N$ , the inverse of the exhibited bijection $N \times N \to N$ ( $N \times N \approx N$ , Equinumerous sets, $A \approx B$ and $A ⪯ B$ , Injection, surjection, bijection).

[F4]

For a nonempty set $A$ : $A$ is at most countable if and only if there is a surjection $s : N \to A$ , and from such an $s$ the rule $j (a) = \min {k \in N : s (k) = a}$ defines an injection $A \to N$ (A nonempty set is at most countable iff it is a surjective image of $N$ ).

[F5]

If $A ⪯ B$ and $B ⪯ A$ then $A \approx B$ (The Schröder-Bernstein theorem); if $A$ and $B$ are at most countable then so is $A \times B$ (A product of two at most countable sets is at most countable).

[F6]

$A$ is countably infinite when $A \approx N$ and at most countable when it is finite or countably infinite (Finite, countably infinite, countable, uncountable); $A ⪯ B$ means an injection $A \to B$ exists (Equinumerous sets, $A \approx B$ and $A ⪯ B$ ); a composite of surjections is a surjection (Injection, surjection, bijection, 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).

Verification

technique · direct

1.1F2

$π$ is a surjective function $N \times N \to Z$ : this is the general quotient map statement applied to the equivalence relation of The integers as equivalence classes of pairs of naturals, whose equivalence-class property is The integer-defining relation is an equivalence relation.

1.2F3

$β : N \to N \times N$ is a bijection, and in particular a surjection.

1.3F1F6

The map $n \mapsto [(n, 0)]$ is an injection $N \to Z$ , so $N ⪯ Z$ .

2.1step 1.1step 1.2F6

The composite $π \circ β : N \to Z$ is a surjection, as a composite of the surjections $β$ and $π$ ; hence $Z$ is a surjective image of $N$ , and $Z \neq \emptyset$ because $[(0, 0)] \in Z$ .

3.1step 2.1F4

Applying [F4] to the nonempty set $Z$ and the surjection $π \circ β$ of step 2.1 gives an injection $j : Z \to N$ , explicitly $j (x) = \min {k \in N : π (β (k)) = x}$ ; hence $Z ⪯ N$ .

4.1step 1.3step 3.1F5F6

Since $N ⪯ Z$ by step 1.3 and $Z ⪯ N$ by step 3.1, Schröder-Bernstein gives $Z \approx N$ , so the integers are countably infinite.

5.1step 4.1F4F5∎

With step 4.1, both $Z$ and $Z$ are at most countable, so their product $Z \times Z$ is at most countable by [F5]. The injection $j$ is defined by the least element of a nonempty set of naturals and $β$ is the inverse of an exhibited bijection, so no choice principle is used.

Remarks

The route through $N \times N$ is the same device that will enumerate $Q$ : $Z$ is a quotient of $N \times N$ , the pairing $β$ lists pairs, and the least-index rule turns a list with repetitions into an injection. Nothing here needs a closed formula for a bijection $Z \to N$ .
For each fixed positive integer $k$ , the product of $k$ copies of $Z$ is at most countable, by $k - 1$ applications of A product of two at most countable sets is at most countable.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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, 307 pp.) (standard reference, not scraped)
Jiri Lebl, Basic Analysis I: Introduction to Real Analysis, Volume I (author-hosted complete book PDF) (standard reference, not scraped)

The integers are countably infinite: Z≈NZ≈N