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 have the least-upper-bound property: every nonempty that is bounded above has a least upper bound . Hence, together with The reals form a totally ordered field, is a complete ordered field (Complete ordered field (least-upper-bound property)).
Statement references
Facts & Assumptions
Given: A nonempty set bounded above by .
Upper bound, least upper bound, and the least-upper-bound property (Complete ordered field (least-upper-bound property)).
Every Cauchy sequence of reals converges to a real (The reals are complete).
Convergence and the Cauchy condition for real sequences are quantified over positive rational (Limits and Cauchy sequences of reals).
is Archimedean, so the reals are cofinal and (The Cauchy-sequence reals are Archimedean).
is a totally ordered field: midpoints , halving, and order arithmetic (The reals form a totally ordered field, Order on the reals).
The rationals embed densely; below any real lies a rational (The rationals embed densely in the reals).
Proof
Fix (possible as ); by [L6] choose a real , so is not an upper bound of , and put , an upper bound of .
Define by bisection: given (not an upper bound) and (an upper bound), let ; if is an upper bound set , otherwise set .
An induction on shows each is an upper bound of , each is not, , and .
Given rational , by [L4] choose with ; then for all , .
For both lie in the nested interval , so and likewise ; hence and are Cauchy sequences of reals.
By [L2], converges to a real and to a real . If , choose by [L6] a positive rational with . For all large , convergence and step 4.1 give , and , whence , a contradiction. If , choose ; for all large , and the two convergence bounds give , again a contradiction. Thus . For fixed and every , step 3.1 gives . If , choose and use ; if , choose and use . Each choice contradicts the displayed inequalities for all large , so .
Every satisfies for all , since each is an upper bound. If , choose by [L6] a positive rational with . Since , eventually , hence , contradicting . Therefore , so is an upper bound of .
If is any upper bound of , then for each some element of exceeds , because is not an upper bound; hence . If , choose by [L6] a positive rational with . Since , eventually , so , a contradiction. Thus , and is the least upper bound.
Hence exists in ; as was an arbitrary nonempty bounded-above set, has the least-upper-bound property and is a complete ordered field.