LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

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 Cauchy-sequence reals are Archimedean

Statement

The Cauchy-sequence reals $\mathbb{R}_C$ (The reals form a totally ordered field) are Archimedean (Archimedean ordered field): for every $x \in \mathbb{R}_C$ there is a natural number $n$ with $x < n \cdot 1$ , where the canonical natural $n \cdot 1$ is the class $\hat n$ of the constant rational sequence $n$ . Equivalently, the canonical naturals $(\hat n)_{n \ge 1}$ are cofinal.

Facts & Assumptions

Given: A real $x \in \mathbb{R}_C$ .

[L1]

Rational approximation: for any real $z$ and rational $\varepsilon > 0$ there is $q \in \mathbb{Q}$ with $|z - \hat q| < \hat\varepsilon$ , and the embedding $q \mapsto \hat q$ preserves and reflects order and arithmetic (The rationals embed densely in the reals).

[L2]

The rationals are Archimedean: for every rational $y$ there is a natural $n$ with $y < n$ (The rationals are Archimedean).

[L3]

$\mathbb{R}_C$ is a totally ordered field, and $\hat q + \hat r = \widehat{q + r}$ , $\hat 1 = 1$ (The reals form a totally ordered field, Order on the reals).

[L4]

$\mathbb{R}_C$ is Archimedean iff for every real there is a natural $n$ with the real below the canonical natural $n \cdot 1 = \hat n$ (Archimedean ordered field).

Proof

technique · direct

1.1

By [L1] with $\varepsilon = 1$ choose a rational $q$ with $|x - \hat q| < \hat 1$ .

L1choose

1.2

By [L2] applied to the rational $q + 1$ choose a natural $n$ with $q + 1 < n$ .

L2choose

2.1

From step 1.1, $x - \hat q < \hat 1$ , so $x < \hat q + \hat 1 = \widehat{q + 1}$ .

step 1.1L3

2.2

From step 1.2, since the embedding preserves order, $\widehat{q + 1} < \hat n = n \cdot 1$ .

step 1.2L1L3L4

3.1

Combining, $x < \widehat{q + 1} < n \cdot 1$ , so $x < n \cdot 1$ for this canonical natural.

step 2.1step 2.2L3

4.1

As $x \in \mathbb{R}_C$ was arbitrary, every real lies below some canonical natural: $\mathbb{R}_C$ is Archimedean.

step 3.1L4∎

Depends on

Used by

The Cauchy-sequence reals have the least-upper-bound property Corollary

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 42 results over 19 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

T. Tao, Analysis I, 3rd ed., §5.4 (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
California State University San Marcos notes: Construction of the real numbers (standard reference, not scraped)