Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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 (xk) is a Cauchy sequence (Limits and Cauchy sequences of reals) then there is M∈R with ∣xk∣≤M for every k∈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 Q, and the argument is the same one: the Cauchy condition at a single value of ε confines all but finitely many terms, and the finitely many exceptions are handled by a maximum.

Facts & Assumptions

Given: A Cauchy sequence (xk) of reals.

[A1]

Cauchy condition: for every rational ε>0 there is K∈N with ∣xk−xl∣<ε for all k,l≥K (Limits and Cauchy sequences of reals).

[L1]

Triangle inequality: ∣x∣=∣(x−y)+y∣≤∣x−y∣+∣y∣ for all reals x,y (The triangle inequality).

[L2]

Every nonempty finite list of reals has a maximum, so max⁡{a0,…,an} 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 Q in R carries it to 1∈R, so ε=1 is an admissible test value in [A1] (The rationals embed densely in the reals).

[L4]

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

[L5]

The order on N is total, so every index satisfies k≤K or k≥K (≤ is a linear order on N).

[L6]

A sequence of reals is bounded when some M∈R satisfies ∣xk∣≤M at every index (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

Proof

technique · direct
1.1

Apply [A1] with the rational test value ε=1: fix K∈N such that ∣xk−xl∣<1 for all k,l≥K.

A1L3choose
1.2

For all reals xk and xK the triangle inequality gives ∣xk∣≤∣xk−xK∣+∣xK∣.

L1
2.1

For every k≥K: ∣xk−xK∣<1 by step 1.1, and adding ∣xK∣ to both sides then combining with step 1.2 gives ∣xk∣<∣xK∣+1.

step 1.1step 1.2L4
2.2

Define M:=max⁡{ ∣x0∣,∣x1∣,…,∣xK∣,∣xK∣+1 }, the maximum of a nonempty finite list of reals, which exists by [L2].

step 1.1L2choose
3.1

For every k≤K: ∣xk∣ is one of the listed values, so ∣xk∣≤M.

step 2.2L2
3.2

For every k≥K: ∣xk∣<∣xK∣+1≤M, since ∣xK∣+1 is one of the listed values.

step 2.1step 2.2L2
4.1

Every index satisfies k≤K or k≥K, so ∣xk∣≤M for every k∈N and (xk) is bounded.

step 3.1step 3.2L5L6∎

Remarks

Depends on

Used by

Dependency tree · two levels

30 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