TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

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 complete ordered field is Archimedean

Statement

Every complete ordered field $F$ (Complete ordered field (least-upper-bound property)) is Archimedean: for every $x \in F$ there is a natural number $n \geq 1$ with $x < n \cdot 1_{F}$ , where $n \cdot 1_{F}$ is the canonical natural of the ordered field $F$ (Ordered field). Equivalently, the canonical naturals are cofinal in $F$ .

Statement references

Complete ordered field (least-upper-bound property)

Ordered field

Facts & Assumptions

Given: A complete ordered field $F$ ; write $A = {n \cdot 1_{F} : n \geq 1}$ for the set of its canonical naturals.

[L1]

Least-upper-bound property: every nonempty $S \subseteq F$ that is bounded above has a least upper bound $\sup S \in F$ (Complete ordered field (least-upper-bound property)).

[L2]

Each canonical natural satisfies $n \cdot 1_{F} > 0$ , one has $(n + 1) \cdot 1_{F} = n \cdot 1_{F} + 1_{F}$ , and $(n + 1) \cdot 1_{F} > n \cdot 1_{F}$ (Canonical naturals are positive and strictly increasing).

[L3]

$0 < 1_{F}$ (The multiplicative identity is positive).

Proof

technique · contradiction

1.1assume-contra

Suppose, for contradiction, that $F$ is not Archimedean: there is some $x \in F$ with $n \cdot 1_{F} \leq x$ for all $n \geq 1$ , that is, $x$ is an upper bound of $A$ .

2.1step 1.1L2

The set $A$ is nonempty, since $1 \cdot 1_{F} = 1_{F} \in A$ , and it is bounded above by $x$ .

3.1step 2.1L1

By the least-upper-bound property, $A$ has a least upper bound $s = \sup A \in F$ .

4.1step 3.1L3

Since $1_{F} > 0$ , we have $s - 1_{F} < s$ ; as $s$ is the least upper bound, $s - 1_{F}$ is not an upper bound of $A$ .

5.1step 4.1

Hence there is some $m \geq 1$ with $m \cdot 1_{F} > s - 1_{F}$ .

6.1step 5.1L2

Adding $1_{F}$ to both sides, $(m + 1) \cdot 1_{F} = m \cdot 1_{F} + 1_{F} > s$ .

7.1step 6.1step 3.1L2

But $(m + 1) \cdot 1_{F} \in A$ , so $(m + 1) \cdot 1_{F} \leq s$ because $s$ is an upper bound of $A$ , contradicting 6.1.

8.1step 7.1discharge-contradiction∎

The assumption is therefore untenable, so $F$ is Archimedean.

Every complete ordered field is Archimedean

Statement

Statement references

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources