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

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.

Every Cauchy sequence of rationals is bounded

Statement

Every Cauchy sequence $(a_n)_{n \ge 1}$ of rational numbers (Cauchy sequence of rationals) is bounded: there exists a rational $M \ge 0$ such that $|a_n| \le M$ for all $n \ge 1$ .

Facts & Assumptions

Given: A Cauchy sequence $(a_n)_{n \ge 1}$ of rational numbers.

[A1]

For every rational $\varepsilon > 0$ there exists $N \in \mathbb{N}$ with $|a_m - a_n| < \varepsilon$ for all $m, n \ge N$ .

[L1]

Triangle inequality on $\mathbb{Q}$ : $|x| \le |x - y| + |y|$ (Absolute value and the triangle inequality).

Proof

technique · direct

1.1

Apply [A1] with $\varepsilon = 1$ : fix $N \in \mathbb{N}$ such that $|a_m - a_n| < 1$ for all $m, n \ge N$ .

1.2

For every $n \ge N$ : $|a_n| \le |a_n - a_N| + |a_N|$ .

2.1

For every $n \ge N$ : $|a_n| < |a_N| + 1$ .

step 1.1step 1.2algebra

2.2

Define $M = \max\{|a_1|, |a_2|, \dots, |a_{N-1}|, |a_N| + 1\}$ , a maximum of finitely many rationals, hence rational and $\ge 0$ .

step 1.1choose

3.1

For every $n < N$ : $|a_n| \le M$ , since $|a_n|$ appears in the maximum.

step 2.2algebra

3.2

For every $n \ge N$ : $|a_n| < |a_N| + 1 \le M$ .

step 2.1step 2.2algebra

4.1

For every $n \ge 1$ : $|a_n| \le M$ , so $(a_n)$ is bounded.

step 3.1step 3.2∎

Depends on

Used by

Null sequences form an ideal Lemma
Cauchy sequences form a commutative ring Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 10 results over 8 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.1 (standard reference, not scraped)
Cauchy sequence (Wikipedia) (standard reference, not scraped)