Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)
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 have the least-upper-bound property

Statement

The Cauchy-sequence reals RC have the least-upper-bound property: every nonempty S⊆RC that is bounded above has a least upper bound sup⁡S∈RC. Hence, together with The reals form a totally ordered field, RC is a complete ordered field (Complete ordered field (least-upper-bound property)).

Facts & Assumptions

Given: A nonempty set S⊆RC bounded above by U∈RC.

[L1]

Upper bound, least upper bound, and the least-upper-bound property (Complete ordered field (least-upper-bound property)).

[L2]

Every Cauchy sequence of reals converges to a real (The reals are complete).

[L3]

Convergence and the Cauchy condition for real sequences are quantified over positive rational ε (Limits and Cauchy sequences of reals).

[L4]

RC is Archimedean, so the reals 2k are cofinal and (b0−a0)/2k→0 (The Cauchy-sequence reals are Archimedean).

[L5]

RC is a totally ordered field: midpoints (a+b)/2, halving, and order arithmetic (The reals form a totally ordered field, Order on the reals).

[L6]

The rationals embed densely; below any real lies a rational (The rationals embed densely in the reals).

Proof

technique · direct
1.1

Fix s0∈S (possible as S≠∅); by [L6] choose a real a0<s0, so a0 is not an upper bound of S, and put b0=U, an upper bound of S.

givenL6L5L1
2.1

Define (ak),(bk) by bisection: given ak (not an upper bound) and bk (an upper bound), let m=(ak+bk)/2; if m is an upper bound set ak+1=ak,bk+1=m, otherwise set ak+1=m,bk+1=bk.

step 1.1L5
3.1

An induction on k shows each bk is an upper bound of S, each ak is not, ak≤ak+1≤bk+1≤bk, and bk−ak=(b0−a0)/2k.

step 2.1L5L1
4.1

Given rational ε>0, by [L4] choose k with (b0−a0)<2kε^; then for all j≥k, bj−aj=(b0−a0)/2j≤(b0−a0)/2k<ε^.

step 3.1L4L5
5.1

For j,l≥k both aj,al,bj,bl lie in the nested interval [ak,bk], so ∣aj−al∣≤bk−ak<ε^ and likewise ∣bj−bl∣<ε^; hence (ak) and (bk) are Cauchy sequences of reals.

step 3.1step 4.1L3L5
6.1

By [L2], (ak) converges to a real s and (bk) to a real s′. If s<s′, choose by [L6] a positive rational ε with 3ε^<s′−s. For all large k, convergence and step 4.1 give ∣ak−s∣<ε^, ∣bk−s′∣<ε^ and bk−ak<ε^, whence s′−s≤∣s′−bk∣+(bk−ak)+∣ak−s∣<3ε^, a contradiction. If s′<s, choose 2ε^<s−s′; for all large k, ak≤bk and the two convergence bounds give s−s′≤∣s−ak∣+(ak−bk)+∣bk−s′∣<2ε^, again a contradiction. Thus s=s′. For fixed k and every j≥k, step 3.1 gives ak≤aj≤bj≤bk. If s<ak, choose 0<ε^<ak−s and use aj→s; if bk<s, choose 0<ε^<s−bk and use bj→s. Each choice contradicts the displayed inequalities for all large j, so ak≤s≤bk.

step 3.1step 4.1step 5.1L2L3L5L6algebra
7.1

Every t∈S satisfies t≤bk for all k, since each bk is an upper bound. If s<t, choose by [L6] a positive rational ε with ε^<t−s. Since bk→s, eventually ∣bk−s∣<ε^, hence bk<s+ε^<t, contradicting t≤bk. Therefore t≤s, so s is an upper bound of S.

step 3.1step 6.1L1L3L5L6
7.2

If v is any upper bound of S, then for each k some element of S exceeds ak, because ak is not an upper bound; hence ak<v. If v<s, choose by [L6] a positive rational ε with ε^<s−v. Since ak→s, eventually ∣ak−s∣<ε^, so ak>s−ε^>v, a contradiction. Thus s≤v, and s is the least upper bound.

step 3.1step 6.1L1L3L5L6
8.1

Hence s=sup⁡S exists in RC; as S was an arbitrary nonempty bounded-above set, RC has the least-upper-bound property and is a complete ordered field.

step 7.1step 7.2L1∎

Depends on

Used by

Dependency tree · two levels

24 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