Alphabeta Math
TheoremStatement: 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.

The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges

Statement

Every Cauchy sequence of reals converges to a real (Limits and Cauchy sequences of reals).

More carefully, this is a statement about the axioms: in a complete ordered field, that is in an ordered field with the least-upper-bound property (Complete ordered field (least-upper-bound property)), every Cauchy sequence converges. The proof below uses nothing about R\mathbb{R} except that property, through Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence.

This library already knows the conclusion by a different route. It is proved on the Cauchy-construction page, where R\mathbb{R} is built out of Cauchy sequences of rationals and completeness is read off the construction. That proof is about a particular construction; this one is about the axioms, and it is what tells us the statement holds in any complete ordered field, however it was obtained.

Facts & Assumptions

Given: A Cauchy sequence (xk)(x_k) of reals, R\mathbb{R} being a complete ordered field.

[L1]

Every Cauchy sequence of reals is bounded (Every Cauchy sequence of reals is bounded).

[L2]

Bolzano-Weierstrass: every bounded sequence of reals has a convergent subsequence, that is a strictly increasing nn and a real LL with xnjLx_{n_j} \to L (Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence).

[L3]

A Cauchy sequence with a subsequence converging to LL converges to LL (A Cauchy sequence with a convergent subsequence converges, to that subsequence’s limit).

[L4]

Convergence of a sequence of reals to a real (Limits and Cauchy sequences of reals).

[L5]

R\mathbb{R} is a complete ordered field, and this is the only property of it used, through [L2] (Complete ordered field (least-upper-bound property)).

Proof

technique · direct
1.1

The Cauchy sequence (xk)(x_k) is bounded.

givenL1
2.1

Being bounded, (xk)(x_k) has a convergent subsequence: fix a strictly increasing n:NNn : \mathbb{N} \to \mathbb{N} and a real LL with xnjLx_{n_j} \to L.

step 1.1L2L5choose
3.1

The sequence (xk)(x_k) is Cauchy and has a subsequence converging to LL, so it converges to LL.

step 2.1L3
4.1

An arbitrary Cauchy sequence of reals has therefore been shown to converge to a real, so every Cauchy sequence of reals converges, and this was derived from the least-upper-bound property alone.

step 3.1L4L5

Remarks

Depends on

Used by

Dependency tree · next 3 levels

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