LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

Bolzano-Weierstrass alone forces the Archimedean property, so it needs no separate Archimedean hypothesis

Statement

Let $F$ be an ordered field with the Bolzano-Weierstrass property (BW) of The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness. Then $F$ is Archimedean (Archimedean ordered field).

Consequently (BW) needs no Archimedean hypothesis attached to it, in contrast with the nested interval property and with Cauchy completeness, which do (FALSE: the nested interval property alone implies the least-upper-bound property, FALSE: an ordered field in which every Cauchy sequence converges has the least-upper-bound property).

Facts & Assumptions

Given: An ordered field $F$ with (BW).

[L1]

The property (BW): every bounded sequence in $F$ has a subsequence converging in $F$ (The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness).

[L2]

Sequences in an ordered field: a sequence is a function $\mathbb{N} \to F$ ; it is bounded when $|x_k| \le M$ for every $k$ and some $M \in F$ ; a subsequence is taken along a strictly increasing $n : \mathbb{N} \to \mathbb{N}$ ; convergence and Cauchyness in $F$ are as fixed there (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).

[L3]

Archimedean property: $F$ is Archimedean when for every $x \in F$ there is a natural number $n$ with $x < n \cdot 1_F$ , where $0 \cdot 1_F = 0$ and $(n+1)\cdot 1_F = n \cdot 1_F + 1_F$ (Archimedean ordered field).

[L4]

Canonical naturals: $n \cdot 1_F > 0$ for $n \ge 1$ , the map $n \mapsto n \cdot 1_F$ is strictly increasing on $\{1,2,3,\dots\}$ , and $(m+n)\cdot 1_F = m \cdot 1_F + n \cdot 1_F$ (Canonical naturals are positive and strictly increasing).

[L5]

Absolute value: $|u| = u$ whenever $u \ge 0$ (Basic properties of the absolute value).

[L6]

A sequence converging in $F$ is Cauchy in $F$ (clause 3 of Sequence basics in an arbitrary ordered field: limits are unique, limits preserve non-strict inequalities, convergent sequences are Cauchy, Cauchy sequences are bounded, and a Cauchy sequence with a convergent subsequence converges).

[L7]

Order arithmetic: $0 < 1_F$ (The multiplicative identity is positive); the order is total, so the failure of $x < y$ is $y \le x$ ; adding a constant preserves the order (Order is preserved by adding a constant and by adding inequalities, Ordered field). Here Order is preserved by adding a constant and by adding inequalities states the STRICT forms and only those; the nonstrict forms used below are those together with the equality cases, which trichotomy settles, the order being total (Ordered field).

[L8]

Discreteness of $\mathbb{N}$ : $m < p$ if and only if $m + 1 \le p$ (Discreteness: $\sigma(n)$ is the immediate successor).

Proof

technique · contradiction

1.1

Suppose $F$ has (BW) and is not Archimedean; then there is $x \in F$ such that $x < n \cdot 1_F$ fails for every natural $n$ , that is, $n \cdot 1_F \le x$ for every $n \in \mathbb{N}$ .

L3L7assume-contra

1.2

Let $(y_k)$ be the sequence in $F$ given by $y_k := k \cdot 1_F$ , so that $y_0 = 0$ , $y_{k+1} = y_k + 1_F$ , and $y_k \ge 0$ for every $k$ .

L2L3L4

2.1

$(y_k)$ is bounded: $|y_k| = y_k \le x$ for every $k$ .

step 1.1step 1.2L2L5

3.1

By (BW) there is a strictly increasing $n : \mathbb{N} \to \mathbb{N}$ and an $L \in F$ with $y_{n_j} \to L$ in $F$ .

step 2.1L1L2

4.1

The subsequence $(y_{n_j})$ is therefore Cauchy in $F$ , so, $1_F$ being positive, there is $J \in \mathbb{N}$ with $|y_{n_j} - y_{n_i}| < 1_F$ for all $i, j \ge J$ .

step 3.1L2L6L7

5.1

But $n_J < n_{J+1}$ gives $n_J + 1 \le n_{J+1}$ and hence $y_{n_{J+1}} \ge y_{n_J + 1} = y_{n_J} + 1_F$ , so $y_{n_{J+1}} - y_{n_J} \ge 1_F > 0$ and $|y_{n_{J+1}} - y_{n_J}| \ge 1_F$ , contradicting step 4.1.

step 1.2step 4.1L4L5L7L8

6.1

The assumption of step 1.1 is therefore untenable, and an ordered field with (BW) is Archimedean.

step 5.1discharge-contradiction∎

Remarks

The witness sequence is the obstruction itself. In a non-Archimedean field the canonical naturals are bounded, so they form a bounded sequence; and no subsequence of them can converge, because consecutive terms of any subsequence stay at distance at least $1_F$ . That is the whole argument, and it shows that (BW) fails in every non-Archimedean ordered field, for instance in $\mathbb{R}(t)$ (Not every ordered field is Archimedean) and in $\mathbb{R}((t^{-1}))$ ( $\mathbb{R}((t^{-1}))$ is non-Archimedean, and the monomials $t^{-k}$ are cofinal below its positive elements).
Note which direction is being used: the sequence is bounded and has no convergent subsequence, so (BW) is contradicted. Nothing here says that $(y_k)$ fails to be Cauchy for some other reason; it is Cauchy along no subsequence at all.

Depends on

Used by

Dependency tree · next 3 levels

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

J. F. Hall, Completeness of Ordered Fields (standard reference, not scraped)
Archimedean property (Wikipedia) (standard reference, not scraped)
Bolzano-Weierstrass theorem (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §1.2 and §2.3 (standard reference, not scraped)