LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26

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 reals is bounded

Statement

Every Cauchy sequence of reals is bounded: if $(x_k)$ is a Cauchy sequence (Limits and Cauchy sequences of reals) then there is $M \in \mathbb{R}$ with $|x_k| \le M$ for every $k \in \mathbb{N}$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

This is the real-number counterpart of the lemma proving the same statement for Cauchy sequences of rationals inside $\mathbb{Q}$ , and the argument is the same one: the Cauchy condition at a single value of $\varepsilon$ confines all but finitely many terms, and the finitely many exceptions are handled by a maximum.

Facts & Assumptions

Given: A Cauchy sequence $(x_k)$ of reals.

[A1]

Cauchy condition: for every rational $\varepsilon > 0$ there is $K \in \mathbb{N}$ with $|x_k - x_l| < \varepsilon$ for all $k, l \ge K$ (Limits and Cauchy sequences of reals).

[L1]

Triangle inequality: $|x| = |(x - y) + y| \le |x - y| + |y|$ for all reals $x, y$ (The triangle inequality).

[L2]

Every nonempty finite list of reals has a maximum, so $\max\{a_0, \dots, a_n\}$ is a well-determined real that dominates each listed value (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L3]

The rational $1$ is positive, and the embedding of $\mathbb{Q}$ in $\mathbb{R}$ carries it to $1 \in \mathbb{R}$ , so $\varepsilon = 1$ is an admissible test value in [A1] (The rationals embed densely in the reals).

[L4]

Order arithmetic in $\mathbb{R}$ : translation invariance, $a < b \Rightarrow a + c < b + c$ (Order is preserved by adding a constant and by adding inequalities); and the mixed transitivity $a \le b < c \Rightarrow a < c$ , immediate from the reading of $a \le b$ as " $a < b$ or $a = b$ " together with transitivity of $<$ (Complete ordered field (least-upper-bound property), Ordered field).

[L5]

The order on $\mathbb{N}$ is total, so every index satisfies $k \le K$ or $k \ge K$ ( $\le$ is a linear order on $\mathbb{N}$ ).

[L6]

A sequence of reals is bounded when some $M \in \mathbb{R}$ satisfies $|x_k| \le M$ at every index (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

Proof

technique · direct

1.1

Apply [A1] with the rational test value $\varepsilon = 1$ : fix $K \in \mathbb{N}$ such that $|x_k - x_l| < 1$ for all $k, l \ge K$ .

A1L3choose

1.2

For all reals $x_k$ and $x_K$ the triangle inequality gives $|x_k| \le |x_k - x_K| + |x_K|$ .

2.1

For every $k \ge K$ : $|x_k - x_K| < 1$ by step 1.1, and adding $|x_K|$ to both sides then combining with step 1.2 gives $|x_k| < |x_K| + 1$ .

step 1.1step 1.2L4

2.2

Define $M := \max\{\,|x_0|, |x_1|, \dots, |x_K|, |x_K| + 1\,\}$ , the maximum of a nonempty finite list of reals, which exists by [L2].

step 1.1L2choose

3.1

For every $k \le K$ : $|x_k|$ is one of the listed values, so $|x_k| \le M$ .

step 2.2L2

3.2

For every $k \ge K$ : $|x_k| < |x_K| + 1 \le M$ , since $|x_K| + 1$ is one of the listed values.

step 2.1step 2.2L2

4.1

Every index satisfies $k \le K$ or $k \ge K$ , so $|x_k| \le M$ for every $k \in \mathbb{N}$ and $(x_k)$ is bounded.

step 3.1step 3.2L5L6∎

Remarks

One value of $\varepsilon$ suffices, and $\varepsilon = 1$ is not special. Any single positive rational would do; what matters is that the Cauchy condition confines all terms from some index onward to within a fixed distance of one term, after which only finitely many terms remain, and a finite list of reals has a maximum (Every nonempty finite set of reals has a maximum and a minimum). This is the same division of labour as in Every convergent sequence is bounded.
The converse is false. A bounded sequence need not be Cauchy: the alternating sequence of FALSE: every bounded sequence converges is bounded and, being divergent, is not Cauchy (Every convergent sequence is Cauchy would otherwise make it convergent by The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges). Boundedness is strictly weaker, and what it does yield is a convergent subsequence (Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence).
No completeness is used. The argument runs in any ordered field, and it is used here as the first of the three steps by which the least-upper-bound property is converted into Cauchy completeness in The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges.
The rational counterpart, proved on the Cauchy-construction page, is Every Cauchy sequence of rationals is bounded. It is the house-style exemplar for this argument, and nothing here depends on it, since the two lemmas live in different fields.

Depends on

Used by

xₖ = √k has xₖ₊₁ - xₖ → 0 and is not Cauchy Counterexample
FALSE: if |xₖ₊₁ - xₖ| → 0 then (xₖ) is Cauchy False statement
The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges Theorem

Dependency tree · next 3 levels

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

Cauchy sequence (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (Thm 3.11(a)) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.1 (Prop. 6.1.17) (standard reference, not scraped)