Session-authored (Fable 5 assisted)

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.

✓ 35 results · all verified · 32 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Foundations of the Real Numbers for Analysis

1 · Prerequisites

2 · Summary

Objective. This page assembles the working foundation a first course in real analysis silently assumes: the arithmetic and order facts of $\mathbb{R}$ that are usually waved through as "obvious", proved in full; the existence of square roots; and the two structural theorems that justify speaking of the real numbers at all. It proves that a complete totally ordered field is unique up to a unique isomorphism, and that the two constructions of $\mathbb{R}$ , via Cauchy sequences and via Dedekind cuts, are the same ordered field seen two ways.

The two constructions are the starting point. The passage from $\mathbb{N}$ to $\mathbb{Z}$ to $\mathbb{Q}$ to $\mathbb{R}$ is carried out in full on the two sibling pages, the Cauchy-sequence construction and the Dedekind-cut construction. Each ends by proving that its $\mathbb{R}$ is a totally ordered field (The reals form a totally ordered field, The Dedekind reals form a totally ordered field) that is complete, in the Cauchy sense (The reals are complete) and in the least-upper-bound sense (Dedekind completeness: the least-upper-bound property) respectively. We take those results as given and build on top of them.

One abstract layer, two payoffs. Rather than reprove each basic fact twice, once per construction, we introduce the abstract notions of a field (Field), an ordered field (Ordered field), and a complete ordered field (Complete ordered field (least-upper-bound property)), and prove every fact from those axioms. Because both constructions are already known to satisfy the axioms, each fact holds in both at once. The same abstraction is what the uniqueness theorem needs, so the layer serves the elementary and the structural goals together.

The obvious facts, proved. From the field axioms alone come $0 \cdot a = 0$ , the sign rule $(-a)(-b) = ab$ (hence $(-1)(-1) = 1$ , $(-1)(-1) = 1$ ), and the absence of zero divisors. Adding the order axioms gives the facts an analysis course leans on constantly: every nonzero square is positive ( $a^2 > 0$ , Squares of nonzero elements are positive), so $0 < 1$ ; the sign rules for products and the behaviour of inequalities under multiplication by a factor and under reciprocals ( $0 < r < 1 \iff 1/r > 1$ , Reciprocals and order: $1/r$ against $1$ ); the absolute value and its triangle inequalities, $|x + y| \le |x| + |y|$ (The triangle inequality) and the reverse form (The reverse triangle inequality); and the full slate of product inequalities, including $0 < ab < b \iff 0 < a < 1$ for $a, b > 0$ (When $ab < b$ for positive $a, b$ ).

Square roots and the Archimedean property. Completeness does the two things $\mathbb{Q}$ could not. It makes the field Archimedean (Every complete ordered field is Archimedean), so the integers are cofinal and the rationals are dense (ℚ is dense in every Archimedean ordered field). The cofinal form is not quite the form analysis uses, so the reciprocal form is recorded separately: for every $\varepsilon > 0$ there is a natural $n \ge 1$ with $1/n < \varepsilon$ (For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ ). That is the statement every convergence proof reaches for, and having it once spares each of them the inversion step. Completeness also supplies square roots: every nonnegative element has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ ), so the positive elements are exactly the nonzero squares. That last fact is the hinge of the uniqueness proof, since a field homomorphism preserves squares and therefore preserves positivity.

Uniqueness. Every ordered field contains a canonical copy of $\mathbb{Q}$ (The unique embedding of ℚ into an ordered field), so the clause "admits $\mathbb{Q}$ as an embedding" is automatic. The theorem Uniqueness of the complete ordered field: $\mathbb{R}$ up to a unique isomorphism then shows any two complete ordered fields are isomorphic by a unique ordered-field isomorphism, built as $x \mapsto \sup\{\, \iota_G(q) : q \in \mathbb{Q},\, \iota_F(q) < x \,\}$ and pinned down by density. So there is, up to a unique isomorphism, exactly one complete totally ordered field: $\mathbb{R}$ .

Equivalence of the two constructions. Uniqueness applies the moment both models are complete ordered fields. The Cauchy model is complete in the least-upper-bound sense too (The Cauchy-sequence reals have the least-upper-bound property, bridged through its Archimedean property The Cauchy-sequence reals are Archimedean), and the Dedekind model is a complete ordered field by construction. Hence Equivalence of the Cauchy and Dedekind constructions of $\mathbb{R}$ : the Cauchy reals and the Dedekind reals are isomorphic through a unique isomorphism that preserves addition, multiplication, and order, and fixes the shared $\mathbb{Q}$ . The two constructions are one object.

Why the hypotheses are sharp. The optional items show none of the hypotheses is free. Without completeness an ordered field can fail to be Archimedean (Not every ordered field is Archimedean), and a field homomorphism between ordered fields can reverse order (A field homomorphism of ordered fields need not preserve order); the false statement FALSE: there exist two non-isomorphic complete ordered fields records that no second complete ordered field escapes the uniqueness theorem.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-07-28 (claude-fable-5)Open item page →

Field

Definition

A field is a set $F$ equipped with two binary operations $+$ (addition) and $\cdot$ (multiplication) and two distinguished elements $0 \ne 1$ of $F$ , satisfying:

(A) $(F, +)$ is an abelian group with identity $0$ : addition is associative and commutative, $x + 0 = x$ for all $x$ , and every $x$ has an additive inverse $-x$ with $x + (-x) = 0$ .
(M) Multiplication is associative and commutative on all of $F$ , and $x \cdot 1 = x$ for every $x \in F$ ; moreover $(F \setminus \{0\}, \cdot)$ is an abelian group with identity $1$ , so every $x \ne 0$ has a multiplicative inverse $x^{-1}$ with $x \cdot x^{-1} = 1$ .
(D) Multiplication distributes over addition: $x \cdot (y + z) = x\cdot y + x\cdot z$ .

We write $x - y := x + (-y)$ and $x/y := x \cdot y^{-1}$ (for $y \ne 0$ ), and abbreviate $x \cdot y$ as $xy$ .

Remarks

The rationals $\mathbb{Q}$ (The rationals form a field) and both constructions of the reals (The reals form a field, The Dedekind reals form a field) are fields. This definition states the field axioms once, abstractly, so that every field fact proved from them applies to all of these at once.
The requirement $0 \ne 1$ excludes the trivial one-element structure.
Why (M) quantifies over all of $F$ explicitly (amended 2026-07-28, owner approved). An earlier wording headed (M) with the group $(F \setminus \{0\}, \cdot)$ alone, and under that strict reading the axioms do not pin down the products $0 \cdot y$ : take $\mathbb{F}_2$ and redefine $0 \cdot y := y$ , which leaves (A) untouched, leaves $(F \setminus \{0\}, \cdot)$ the trivial group, and satisfies (D) in all eight instances, yet has $0 \cdot 1 = 1$ — making Multiplication by zero: $0 \cdot a = 0$ false in a purported model of the axioms. Associativity, commutativity and $x \cdot 1 = x$ are therefore asserted on all of $F$ , the element $0$ included. Commutativity on all of $F$ is also what turns (D) into its right-hand form $(y + z) \cdot x = y \cdot x + z \cdot x$ , which Multiplication by zero: $0 \cdot a = 0$ uses.
The identities $0, 1$ and the inverses $-x, x^{-1}$ are unique (Identities and inverses in a field are unique ↗), so writing them as single-valued notation, and the abbreviations $x - y := x + (-y)$ and $x/y := x y^{-1}$ , are legitimate.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-25Open item page →

Ordered field

Definition

An ordered field is a field $F$ (Field) together with a subset $P \subseteq F$ , the set of positive elements (the positive cone), satisfying:

(O1) Trichotomy. For each $x \in F$ , exactly one of the following holds: $x \in P$ , or $x = 0$ , or $-x \in P$ .
(O2) Closure. If $x, y \in P$ then $x + y \in P$ and $x \cdot y \in P$ .

We write $x > 0$ for $x \in P$ (read " $x$ is positive"), and define the order by

$a < b \;:\Longleftrightarrow\; b - a \in P, \qquad a \le b \;:\Longleftrightarrow\; a < b \text{ or } a = b.$

Thus $a > b$ means $b < a$ , and $a \ge b$ means $b \le a$ . An element $x$ with $-x \in P$ (equivalently $x < 0$ ) is called negative.

Remarks

By trichotomy applied to $b - a$ , for any $a, b$ exactly one of $a < b$ , $a = b$ , $a > b$ holds; this makes $\le$ a total order.
(O2) says the positives are closed under addition and multiplication: sums and products of positives are positive.
The rationals (The rationals form a totally ordered field) and both constructions of the reals (The reals form a totally ordered field, The Dedekind reals form a totally ordered field) are ordered fields, so every fact proved here from (O1)-(O2) holds in each of them.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-25Open item page →

Absolute value in an ordered field

Definition

Let $F$ be an ordered field (Ordered field). The absolute value of $x \in F$ is

$|x| \;:=\; \begin{cases} x & \text{if } x \ge 0, \\ -x & \text{if } x < 0. \end{cases}$

Remarks

The distance between $x$ and $y$ is $|x - y|$ .
The basic algebraic properties ( $|x| \ge 0$ , $|x| = 0 \iff x = 0$ , $|xy| = |x|\,|y|$ , and the characterisation $|x| < c \iff -c < x < c$ ) are established in Basic properties of the absolute value; the triangle inequality is The triangle inequality.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-25Open item page →

Archimedean ordered field

Definition

Let $F$ be an ordered field (Ordered field). For a natural number $n \ge 1$ , write $n \cdot 1_F := \underbrace{1_F + \cdots + 1_F}_{n}$ for the $n$ -fold sum of the multiplicative identity, and $0 \cdot 1_F := 0$ . These are the canonical natural numbers of $F$ .

$F$ is Archimedean if for every $x \in F$ there is a natural number $n$ with

$x < n \cdot 1_F.$

Equivalently, the canonical naturals $(n \cdot 1_F)_{n \ge 1}$ are cofinal: no single element of $F$ is an upper bound for all of them.

Remarks

Equivalently (applying the definition to $1/\varepsilon$ ): for every $\varepsilon > 0$ in $F$ there is $n$ with $1/(n \cdot 1_F) < \varepsilon$ , so the canonical fractions $1/n$ are arbitrarily small.
That the canonical naturals are well-defined, positive, and strictly increasing is Canonical naturals are positive and strictly increasing. Every complete ordered field is Archimedean (Every complete ordered field is Archimedean); an ordered field need not be (Not every ordered field is Archimedean).

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-25Open item page →

Complete ordered field (least-upper-bound property)

Definition

Let $F$ be an ordered field (Ordered field) and $S \subseteq F$ .

$u \in F$ is an upper bound of $S$ if $s \le u$ for all $s \in S$ ; $S$ is bounded above if it has an upper bound.
$u \in F$ is a least upper bound (or supremum, $\sup S$ ) of $S$ if $u$ is an upper bound of $S$ and $u \le u'$ for every upper bound $u'$ of $S$ .

$F$ is a complete ordered field (equivalently, $F$ has the least-upper-bound property, or is Dedekind complete) if every nonempty $S \subseteq F$ that is bounded above has a least upper bound in $F$ .

Remarks

A least upper bound, if it exists, is unique (two least upper bounds are each $\le$ the other, so equal by antisymmetry of the order).
Applying the property to $\{-s : s \in S\}$ yields the dual greatest lower bound (infimum) property, so the two are equivalent.
The Dedekind-cut reals have this property by construction (Dedekind completeness: the least-upper-bound property); the Cauchy-sequence reals acquire it via The Cauchy-sequence reals have the least-upper-bound property. This definition is the target for the uniqueness theorem Uniqueness of the complete ordered field: $\mathbb{R}$ up to a unique isomorphism.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-25Open item page →

Field homomorphism and embedding

Definition

Let $F$ and $G$ be fields (Field). A field homomorphism $\varphi : F \to G$ is a map satisfying, for all $x, y \in F$ ,

$\varphi(x + y) = \varphi(x) + \varphi(y), \qquad \varphi(x\, y) = \varphi(x)\,\varphi(y), \qquad \varphi(1_F) = 1_G.$

An embedding (or monomorphism) is an injective field homomorphism. An isomorphism is a bijective field homomorphism.

Remarks

From additivity, $\varphi(0_F) = 0_G$ and $\varphi(-x) = -\varphi(x)$ ; from multiplicativity, $\varphi(x^{-1}) = \varphi(x)^{-1}$ for $x \ne 0$ . These read off because $\varphi(-x)$ is an additive inverse of $\varphi(x)$ and $\varphi(x^{-1})$ a multiplicative inverse of $\varphi(x)$ , and inverses are unique (Identities and inverses in a field are unique).
Every field homomorphism is automatically injective: its kernel $\{x : \varphi(x) = 0\}$ is an ideal of $F$ , and a field has only the ideals $\{0\}$ and $F$ ; since $\varphi(1_F) = 1_G \ne 0$ , the kernel is $\{0\}$ . This injectivity is used explicitly in Homomorphisms out of a complete ordered field are order-preserving.
Order-compatible homomorphisms are the subject of Ordered-field isomorphism.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-25Open item page →

Ordered-field isomorphism

Definition

Let $F$ and $G$ be ordered fields (Ordered field). An ordered-field isomorphism $\varphi : F \to G$ is a bijective field homomorphism (Field homomorphism and embedding) that is order-preserving in both directions:

$a < b \;\Longleftrightarrow\; \varphi(a) < \varphi(b) \qquad \text{for all } a, b \in F.$

Two ordered fields are isomorphic if there exists an ordered-field isomorphism between them; we write $F \cong G$ .

Remarks

Equivalently, $\varphi$ is a field isomorphism carrying the positive cone of $F$ onto that of $G$ ( $\varphi(P_F) = P_G$ ); the inverse $\varphi^{-1}$ is then also an ordered-field isomorphism.
Because a field homomorphism preserves all of $+, -, \cdot, {}^{-1}, 0, 1$ , an ordered-field isomorphism identifies $F$ and $G$ as ordered fields completely: every field-theoretic and order-theoretic statement transfers across it.
For homomorphisms out of a complete ordered field, order-preservation is automatic (Homomorphisms out of a complete ordered field are order-preserving); this is what makes the isomorphism in Uniqueness of the complete ordered field: $\mathbb{R}$ up to a unique isomorphism unique.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Identities and inverses in a field are unique

Statement

In a field $F$ (Field) the additive identity, the multiplicative identity, each additive inverse, and each multiplicative inverse are unique. Hence the notations $0$ , $1$ , $-x$ , and $x^{-1}$ denote well-defined elements, as the field definition and its consequences assume.

Facts & Assumptions

Given: A field $F$ satisfying the axioms (A), (M), (D) (Field).

[L1]

$(F, +)$ is an abelian group with identity $0$ : addition is associative and commutative and $x + 0 = x$ for all $x$ ; and $(F \setminus \{0\}, \cdot)$ is an abelian group with identity $1$ : multiplication is associative and commutative and $x \cdot 1 = x$ for all $x \ne 0$ (Field).

Proof

technique · direct

1.1

The additive identity is unique: if $0$ and $0'$ both satisfy $x + 0 = x$ and $x + 0' = x$ for all $x$ , then $0' = 0' + 0 = 0 + 0' = 0$ , using that $0$ is an identity, commutativity, and that $0'$ is an identity.

1.2

Additive inverses are unique: if $a$ and $b$ both satisfy $x + a = 0$ and $x + b = 0$ , then $a = a + 0 = a + (x + b) = (a + x) + b = 0 + b = b$ , using associativity and commutativity.

1.3

The same two arguments in the abelian group $(F \setminus \{0\}, \cdot)$ give uniqueness of the multiplicative identity, $1' = 1' \cdot 1 = 1 \cdot 1' = 1$ , and of multiplicative inverses: if $x a = 1$ and $x b = 1$ with $x \ne 0$ , then $a = a \cdot 1 = a (x b) = (a x) b = 1 \cdot b = b$ (using $a x = x a = 1$ ).

2.1

Therefore $0$ , $1$ and, for each $x$ , its additive inverse $-x$ and (for $x \ne 0$ ) its multiplicative inverse $x^{-1}$ are the unique elements with their defining properties, so all four notations are well-defined.

step 1.1step 1.2step 1.3∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Multiplication by zero: $0 \cdot a = 0$

Statement

In any field $F$ (Field), for every $a \in F$ we have $0 \cdot a = 0$ .

Facts & Assumptions

Given: A field $F$ and an element $a \in F$ .

[L1]

Field axioms (Field): $0$ is the additive identity, so $0 + 0 = 0$ and $x + 0 = x$ for all $x$ ; multiplication distributes over addition, $(y + z) \cdot x = y \cdot x + z \cdot x$ .

[L2]

Field axioms (Field): every element has an additive inverse, so addition admits cancellation: if $x + z = y + z$ then $x = y$ .

Proof

technique · direct

1.1

Since $0 + 0 = 0$ , we have $0 \cdot a = (0 + 0) \cdot a$ .

1.2

By distributivity, $(0 + 0) \cdot a = 0 \cdot a + 0 \cdot a$ .

1.3

Since $0$ is the additive identity, $0 \cdot a = 0 \cdot a + 0$ .

2.1

Combining the two expressions for $(0 + 0) \cdot a$ gives $0 \cdot a = 0 \cdot a + 0 \cdot a$ .

step 1.1step 1.2

3.1

From steps 1.3 and 2.1, $0 \cdot a + 0 = 0 \cdot a + 0 \cdot a$ .

step 1.3step 2.1

4.1

Cancelling $0 \cdot a$ from both sides yields $0 = 0 \cdot a$ , that is $0 \cdot a = 0$ .

step 3.1L2∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Sign rules for products: $(-a)b = -(ab)$ and $(-a)(-b) = ab$

Statement

In any field $F$ (Field), for all $a, b \in F$ we have $(-a)b = -(ab)$ and $(-a)(-b) = ab$ .

Facts & Assumptions

Given: A field $F$ and elements $a, b \in F$ .

[L1]

Field axioms (Field): multiplication distributes over addition and is commutative; $x + (-x) = 0$ for every $x$ ; the additive inverse of an element is unique, so if $u + v = 0$ then $v = -u$ ; and $-(-x) = x$ .

[L2]

For every $x \in F$ , $0 \cdot x = 0$ and $x \cdot 0 = 0$ (Multiplication by zero: $0 \cdot a = 0$ , using commutativity).

Proof

technique · direct

1.1

By distributivity, $ab + (-a)b = (a + (-a)) \cdot b$ .

1.2

Since $a + (-a) = 0$ , we have $(a + (-a)) \cdot b = 0 \cdot b$ .

1.3

$0 \cdot b = 0$ .

1.4

By distributivity, $ab + a(-b) = a \cdot (b + (-b))$ .

1.5

Since $b + (-b) = 0$ , we have $a \cdot (b + (-b)) = a \cdot 0$ .

1.6

$a \cdot 0 = 0$ .

1.7

By distributivity, $(-a)(-b) + a(-b) = ((-a) + a) \cdot (-b)$ .

1.8

Since $(-a) + a = 0$ , we have $((-a) + a) \cdot (-b) = 0 \cdot (-b)$ .

1.9

$0 \cdot (-b) = 0$ .

2.1

Chaining steps 1.1, 1.2, 1.3 gives $ab + (-a)b = 0$ .

step 1.1step 1.2step 1.3

2.2

Chaining steps 1.4, 1.5, 1.6 gives $ab + a(-b) = 0$ .

step 1.4step 1.5step 1.6

2.3

Chaining steps 1.7, 1.8, 1.9 gives $(-a)(-b) + a(-b) = 0$ .

step 1.7step 1.8step 1.9

3.1

Since $ab + (-a)b = 0$ , the inverse uniqueness axiom gives $(-a)b = -(ab)$ .

step 2.1L1

3.2

Since $ab + a(-b) = 0$ , the inverse uniqueness axiom gives $a(-b) = -(ab)$ .

step 2.2L1

3.3

Since $(-a)(-b) + a(-b) = 0$ , the inverse uniqueness axiom gives $(-a)(-b) = -(a(-b))$ .

step 2.3L1

4.1

Substituting $a(-b) = -(ab)$ into $(-a)(-b) = -(a(-b))$ gives $(-a)(-b) = -(-(ab)) = ab$ .

step 3.2step 3.3L1∎

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

$(-1)(-1) = 1$

Statement

In any field $F$ , the identity $(-1)(-1) = 1$ holds.

Facts & Assumptions

Given: A field $F$ with multiplicative identity $1$ .

[L1]

For all elements $a, b$ of a field, $(-a)(-b) = ab$ (Sign rules for products: $(-a)b = -(ab)$ and $(-a)(-b) = ab$ ).

[L2]

The element $1$ is the multiplicative identity, so $1 \cdot 1 = 1$ (field axiom).

Proof

technique · direct

1.1

Setting $a = b = 1$ in the sign rule gives $(-1)(-1) = 1 \cdot 1$ .

2.1

Since $1 \cdot 1 = 1$ , we conclude $(-1)(-1) = 1$ .

step 1.1L2∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

A field has no zero divisors: $ab = 0 \Rightarrow a = 0$ or $b = 0$

Statement

In any field $F$ (Field), if $a, b \in F$ satisfy $ab = 0$ , then $a = 0$ or $b = 0$ .

Facts & Assumptions

Given: A field $F$ and elements $a, b \in F$ with $ab = 0$ .

[L1]

Field axioms (Field): if $a \ne 0$ then $a$ has a multiplicative inverse $a^{-1}$ with $a^{-1} a = 1$ ; multiplication is associative; and $1$ is the multiplicative identity, so $1 \cdot x = x$ .

[L2]

For every $x \in F$ , $x \cdot 0 = 0$ (Multiplication by zero: $0 \cdot a = 0$ , using commutativity).

Proof

technique · direct

1.1

If $a = 0$ the disjunction $a = 0$ or $b = 0$ already holds, so it suffices to assume $a \ne 0$ and derive $b = 0$ .

suffices: a ne 0 implies b = 0

1.2

Assuming $a \ne 0$ , the inverse $a^{-1}$ exists with $a^{-1} a = 1$ .

1.3

Since $1$ is the multiplicative identity, $b = 1 \cdot b$ .

1.4

By associativity, $(a^{-1} a) \cdot b = a^{-1} (a b)$ .

1.5

We are given $ab = 0$ .

given

1.6

$a^{-1} \cdot 0 = 0$ .

2.1

Substituting $1 = a^{-1} a$ into $b = 1 \cdot b$ and using associativity gives $b = (a^{-1} a) b = a^{-1}(ab)$ .

step 1.2step 1.3step 1.4

2.2

Since $ab = 0$ , we have $a^{-1}(ab) = a^{-1} \cdot 0$ .

step 1.5

3.1

Combining, $b = a^{-1}(ab) = a^{-1} \cdot 0 = 0$ .

step 2.1step 2.2step 1.6

4.1

Hence $a \ne 0$ forces $b = 0$ , so in every case $a = 0$ or $b = 0$ .

step 1.1step 3.1∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Multiplicative cancellation: $c \ne 0$ and $ac = bc \Rightarrow a = b$

Statement

In any field $F$ (Field), if $a, b, c \in F$ with $c \ne 0$ and $ac = bc$ , then $a = b$ .

Facts & Assumptions

Given: A field $F$ and elements $a, b, c \in F$ with $c \ne 0$ and $ac = bc$ .

[L1]

Field axioms (Field): since $c \ne 0$ , the inverse $c^{-1}$ exists with $c \cdot c^{-1} = 1$ ; multiplication is associative; and $1$ is the multiplicative identity, so $x \cdot 1 = x$ .

Proof

technique · direct

1.1

Since $c \ne 0$ , the inverse $c^{-1}$ exists with $c \cdot c^{-1} = 1$ .

1.2

We are given $ac = bc$ .

given

2.1

Using $c \cdot c^{-1} = 1$ and associativity, $a = a \cdot 1 = a(c \cdot c^{-1}) = (ac) c^{-1}$ .

step 1.1L1

2.2

Using $c \cdot c^{-1} = 1$ and associativity, $b = b \cdot 1 = b(c \cdot c^{-1}) = (bc) c^{-1}$ .

step 1.1L1

2.3

Since $ac = bc$ , we have $(ac) c^{-1} = (bc) c^{-1}$ .

step 1.2

3.1

Combining, $a = (ac) c^{-1} = (bc) c^{-1} = b$ .

step 2.1step 2.2step 2.3∎

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Order is preserved by adding a constant and by adding inequalities

Statement

Let $F$ be an ordered field (Ordered field) with positive cone $P$ , and let $a, b, c, d \in F$ .

Translation invariance. If $a < b$ then $a + c < b + c$ .
Adding inequalities. If $a < b$ and $c < d$ then $a + c < b + d$ .

Facts & Assumptions

Given: An ordered field $F$ with positive cone $P$ , and elements $a, b, c, d \in F$ .

[L1]

For $x, y \in F$ , the relation $x < y$ means $y - x \in P$ (Ordered field).

[L2]

$P$ is closed under addition: if $u, v \in P$ then $u + v \in P$ (axiom O2 of Ordered field).

Proof

technique · direct

1.1

Assume $a < b$ ; by the definition of the order this means $b - a \in P$ .

assume-hypL1

1.2

For every $c \in F$ the field identities give $(b + c) - (a + c) = b - a$ .

algebra

1.3

Assume moreover $c < d$ ; by the definition of the order this means $d - c \in P$ .

assume-hypL1

1.4

The field identities give $(b + d) - (a + c) = (b - a) + (d - c)$ .

algebra

2.1

Hence $(b + c) - (a + c) = b - a \in P$ , which is exactly $a + c < b + c$ , proving claim 1.

step 1.1step 1.2L1

2.2

Since $b - a \in P$ and $d - c \in P$ , closure under addition gives $(b - a) + (d - c) \in P$ .

step 1.1step 1.3L2

3.1

Therefore $(b + d) - (a + c) = (b - a) + (d - c) \in P$ , which is exactly $a + c < b + d$ , proving claim 2.

step 1.4step 2.2L1∎

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Sign rules for products and monotonicity of multiplication

Statement

Let $F$ be an ordered field (Ordered field) with positive cone $P$ , and let $a, b, c \in F$ .

If $a > 0$ and $b > 0$ then $ab > 0$ .
If $a > 0$ and $b < 0$ then $ab < 0$ .
If $a < 0$ and $b < 0$ then $ab > 0$ .
If $c > 0$ then $a < b \iff ac < bc$ .
If $c < 0$ then $a < b \iff bc < ac$ (multiplication by a negative reverses order).

Facts & Assumptions

Given: An ordered field $F$ with positive cone $P$ , and elements $a, b, c \in F$ .

[L1]

For $x, y \in F$ : $x < y \iff y - x \in P$ ; $x > 0 \iff x \in P$ ; $x < 0 \iff -x \in P$ ; and (trichotomy) for each $x$ exactly one of $x \in P$ , $x = 0$ , $-x \in P$ holds, so $0 \notin P$ and $x \in P \Rightarrow x \neq 0$ (Ordered field).

[L2]

$P$ is closed under multiplication: if $u, v \in P$ then $uv \in P$ (axiom O2 of Ordered field).

[L3]

In any field, $(-u)v = -(uv)$ and $(-u)(-v) = uv$ (Sign rules for products: $(-a)b = -(ab)$ and $(-a)(-b) = ab$ ).

[L4]

In any field, $0 \cdot u = 0$ (Multiplication by zero: $0 \cdot a = 0$ ).

Proof

technique · direct

1.1

Assume $a > 0$ and $b > 0$ , i.e. $a \in P$ and $b \in P$ ; closure gives $ab \in P$ , so $ab > 0$ , proving claim 1.

assume-hypL1L2

1.2

Assume $a > 0$ and $b < 0$ , i.e. $a \in P$ and $-b \in P$ ; closure gives $a(-b) \in P$ .

assume-hypL1L2

1.3

Assume $a < 0$ and $b < 0$ , i.e. $-a \in P$ and $-b \in P$ ; closure gives $(-a)(-b) \in P$ .

assume-hypL1L2

1.4

Assume $c > 0$ and $a < b$ , i.e. $c \in P$ and $b - a \in P$ ; closure gives $(b - a)c \in P$ .

assume-hypL1L2

1.5

Assume $c < 0$ and $a < b$ , i.e. $-c \in P$ and $b - a \in P$ ; closure gives $(b - a)(-c) \in P$ .

assume-hypL1L2

2.1

Since $a(-b) = -(ab)$ by L3, step 1.2 gives $-(ab) \in P$ , so $ab < 0$ , proving claim 2.

step 1.2L3L1

2.2

Since $(-a)(-b) = ab$ by L3, step 1.3 gives $ab \in P$ , so $ab > 0$ , proving claim 3.

step 1.3L3L1

2.3

By distributivity $(b - a)c = bc - ac$ , so step 1.4 gives $bc - ac \in P$ , i.e. $ac < bc$ : this is the forward direction of claim 4.

step 1.4algebraL1

2.4

By L3 and distributivity $(b - a)(-c) = -((b - a)c) = -(bc - ac) = ac - bc$ , so step 1.5 gives $ac - bc \in P$ , i.e. $bc < ac$ : this is the forward direction of claim 5.

step 1.5L3algebraL1

3.1

Conversely, assume $c > 0$ and $ac < bc$ ; by trichotomy exactly one of $a < b$ , $a = b$ , $b < a$ holds. If $a = b$ then $ac = bc$ , contradicting $ac < bc$ ; if $b < a$ then the argument of step 2.3 applied to the pair $b < a$ gives $bc < ac$ , so $bc - ac \in P$ (from $ac < bc$ ) while $ac - bc \in P$ (from $bc < ac$ ), putting the element $bc - ac$ and its negative $ac - bc$ both in $P$ , which trichotomy forbids; hence $a < b$ : this completes claim 4.

assume-hypstep 2.3L4L1algebra

4.1

Conversely, assume $c < 0$ and $bc < ac$ ; by trichotomy exactly one of $a < b$ , $a = b$ , $b < a$ holds. If $a = b$ then $ac = bc$ , contradicting $bc < ac$ ; if $b < a$ then the argument of step 2.4 applied to the pair $b < a$ gives $ac < bc$ , so $ac - bc \in P$ (from $bc < ac$ ) while $bc - ac \in P$ (from $ac < bc$ ), putting the element $ac - bc$ and its negative $bc - ac$ both in $P$ , which trichotomy forbids; hence $a < b$ : this completes claim 5.

assume-hypstep 2.4L4L1algebra∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Squares of nonzero elements are positive

Statement

Let $F$ be an ordered field (Ordered field) with positive cone $P$ . For every $a \in F$ with $a \neq 0$ we have $a^2 > 0$ , where $a^2 = a \cdot a$ . In particular, every nonzero square is positive.

Facts & Assumptions

Given: An ordered field $F$ with positive cone $P$ , and an element $a \in F$ with $a \neq 0$ .

[L1]

$x > 0 \iff x \in P$ , and by trichotomy for $a \neq 0$ exactly one of $a \in P$ , $-a \in P$ holds (Ordered field).

[L2]

$P$ is closed under multiplication: if $u, v \in P$ then $uv \in P$ (axiom O2 of Ordered field).

[L3]

In any field, $(-u)(-v) = uv$ (Sign rules for products: $(-a)b = -(ab)$ and $(-a)(-b) = ab$ ).

Proof

technique · cases

1.1

Since $a \neq 0$ , trichotomy leaves exactly two possibilities: $a \in P$ or $-a \in P$ .

2.1

Case $a > 0$ : then $a \in P$ , so closure gives $a \cdot a \in P$ , i.e. $a^2 > 0$ .

assume-case posstep 1.1L2L1

2.2

Case $a < 0$ : then $-a \in P$ , so closure gives $(-a)(-a) \in P$ ; since $(-a)(-a) = a \cdot a = a^2$ by L3, we get $a^2 \in P$ , i.e. $a^2 > 0$ .

assume-case negstep 1.1L2L3L1

3.1

The cases $a > 0$ and $a < 0$ exhaust all of $a \neq 0$ by trichotomy, and both yield $a^2 > 0$ .

cases-exhaustivestep 2.1step 2.2∎

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

The multiplicative identity is positive

Statement

In any ordered field $F$ with positive cone $P$ , the multiplicative identity satisfies $0 < 1$ ; that is, $1 \in P$ .

Facts & Assumptions

Given: An ordered field $F$ with positive cone $P$ and multiplicative identity $1$ (Field).

[L1]

In any field $1 \neq 0$ (Field).

[L2]

For every $x \neq 0$ the square satisfies $x^2 > 0$ (Squares of nonzero elements are positive).

[L3]

The identity axiom gives $1 = 1 \cdot 1 = 1^2$ (Field).

Proof

technique · direct

1.1

By the field axioms $1 \neq 0$ , and $1 = 1 \cdot 1 = 1^2$ .

L1L3

2.1

Since $1 \neq 0$ , applying the square lemma with $x = 1$ gives $1^2 > 0$ .

step 1.1L2

3.1

Because $1 = 1^2$ , it follows that $1 > 0$ , i.e. $0 < 1$ .

step 2.1step 1.1L3∎

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Inverses of positives are positive, and reciprocation reverses order

Statement

Let $F$ be an ordered field (Ordered field) with positive cone $P$ , and let $a, b \in F$ .

If $a > 0$ then $a^{-1} > 0$ .
If $0 < a < b$ then $0 < b^{-1} < a^{-1}$ .

Facts & Assumptions

Given: An ordered field $F$ with positive cone $P$ , and elements $a, b \in F$ .

[L1]

$x > 0 \iff x \in P$ ; $x < 0 \iff -x \in P$ ; and for $x \neq 0$ exactly one of $x \in P$ , $-x \in P$ holds (Ordered field).

[L2]

Sign rules: a product of a positive and a negative is negative, a product of two positives is positive, and for $c > 0$ one has $a < b \iff ac < bc$ (Sign rules for products and monotonicity of multiplication).

[L3]

$0 < 1$ ; in particular $1 \neq 0$ (The multiplicative identity is positive).

[L4]

$P$ is closed under addition, so $<$ is transitive (Ordered field).

Proof

technique · direct

1.1

Assume $a > 0$ , so $a \neq 0$ and its inverse $a^{-1}$ exists with $a \cdot a^{-1} = 1$ ; moreover $a^{-1} \neq 0$ , since $a^{-1}$ has $a$ as its inverse while $0$ is non-invertible ( $1 \neq 0$ by L3).

assume-hypL1L3

2.1

By trichotomy $a^{-1} \in P$ or $-a^{-1} \in P$ ; if $-a^{-1} \in P$ , then $a > 0$ and $a^{-1} < 0$ give $a \cdot a^{-1} < 0$ by the sign rules, i.e. $1 < 0$ , contradicting $0 < 1$ ; hence $a^{-1} \in P$ , i.e. $a^{-1} > 0$ , proving claim 1.

step 1.1L2L3L1

3.1

Assume $0 < a < b$ ; then $0 < b$ by transitivity, so by claim 1 both $a^{-1} > 0$ and $b^{-1} > 0$ , and the sign rules give $a^{-1} b^{-1} > 0$ .

assume-hypstep 2.1L4L2L1

4.1

Multiplying $a < b$ by the positive $a^{-1} b^{-1}$ via the sign rules gives $a (a^{-1} b^{-1}) < b (a^{-1} b^{-1})$ ; since $a a^{-1} = 1$ and $b b^{-1} = 1$ , this simplifies to $b^{-1} < a^{-1}$ .

step 3.1L2algebra

5.1

Together with $b^{-1} > 0$ from step 3.1, we conclude $0 < b^{-1} < a^{-1}$ , proving claim 2.

step 3.1step 4.1∎

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Basic properties of the absolute value

Statement

Let $F$ be an ordered field (Ordered field) and let $x, y \in F$ , with $|x|$ the absolute value (Absolute value in an ordered field). Then

$|x| \ge 0; \quad |x| = 0 \iff x = 0; \quad -|x| \le x \le |x|; \quad |-x| = |x|; \quad |xy| = |x|\,|y|;$

and, for every $c > 0$ , one has $|x| < c \iff -c < x < c$ .

Facts & Assumptions

Given: An ordered field $F$ and elements $x, y \in F$ .

[L1]

Absolute value: $|u| = u$ if $u \ge 0$ , and $|u| = -u$ if $u < 0$ (Absolute value in an ordered field).

[L2]

Ordered-field order: trichotomy holds (for each $u$ exactly one of $u > 0$ , $u = 0$ , $u < 0$ ), $a < b$ means $b - a$ is positive, and sums and products of positives are positive (Ordered field).

[L3]

Signs in products: $(-a)b = -(ab)$ and $(-a)(-b) = ab$ (Sign rules for products: $(-a)b = -(ab)$ and $(-a)(-b) = ab$ ).

[L4]

Sign rules: a product of two elements of the same sign is positive, and a product of two elements of opposite sign is negative (Sign rules for products and monotonicity of multiplication).

Proof

technique · cases

1.1

Case $x > 0$ : by [L1] $|x| = x > 0$ , so $|x| \ge 0$ and $|x| \ne 0$ ; since $-x < 0$ we get $|-x| = -(-x) = x = |x|$ by [L1], and $-|x| = -x < 0 < x = |x|$ , so $-|x| \le x \le |x|$ .

assume-case posL1L2algebra

1.2

Case $x = 0$ : then $|x| = |0| = 0$ , so $|x| \ge 0$ holds with $|x| = 0$ and $x = 0$ , while $|-x| = |0| = |x|$ and $-|x| = 0 \le 0 \le 0 = |x|$ .

assume-case zeroL1

1.3

Case $x < 0$ : by [L1] $|x| = -x$ , and [L2] gives $-x > 0$ , so $|x| > 0$ and $|x| \ne 0$ ; here $|-x| = -x = |x|$ by [L1], and $-|x| = -(-x) = x \le x$ while $x < 0 < -x = |x|$ , so $-|x| \le x \le |x|$ .

assume-case negL1L2algebra

1.4

Case $x = 0$ or $y = 0$ : then $xy = 0$ , so $|xy| = 0$ , and one of $|x|, |y|$ is $0$ , whence $|x|\,|y| = 0 = |xy|$ .

assume-case zerofactorL1

1.5

Case $x, y$ have the same sign (both positive or both negative): by [L4] $xy > 0$ , so $|xy| = xy$ , while $|x|\,|y| = xy$ by [L3] (for $x, y < 0$ this is $(-x)(-y) = xy$ ), hence $|xy| = |x|\,|y|$ .

assume-case sameL1L3L4

1.6

Case $x, y$ have opposite signs (one positive, one negative): by [L4] $xy < 0$ , so $|xy| = -(xy)$ , while $|x|\,|y| = -(xy)$ by [L3] (namely $x(-y)$ or $(-x)y$ ), hence $|xy| = |x|\,|y|$ .

assume-case oppositeL1L3L4

2.1

By trichotomy [L2] each $x$ lies in exactly one of the cases 1.1-1.3, and in each we verified $|x| \ge 0$ , that $|x| = 0 \iff x = 0$ , that $|-x| = |x|$ , and that $-|x| \le x \le |x|$ ; hence all four hold for every $x$ .

step 1.1step 1.2step 1.3cases-exhaustive

2.2

By trichotomy [L2] each pair $x, y$ lies in exactly one of the cases 1.4-1.6, and in each $|xy| = |x|\,|y|$ ; hence $|xy| = |x|\,|y|$ for all $x, y$ .

step 1.4step 1.5step 1.6cases-exhaustive

3.1

Let $c > 0$ : if $|x| < c$ then $-c < -|x| \le x \le |x| < c$ by [step 2.1] and [L2], so $-c < x < c$ ; conversely if $-c < x < c$ then both $x < c$ and $-x < c$ , and since $|x|$ equals $x$ or $-x$ by [L1], we get $|x| < c$ , so $|x| < c \iff -c < x < c$ .

step 2.1L1L2∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-25Open item page →

The triangle inequality

Statement

Let $F$ be an ordered field (Ordered field) and let $x, y \in F$ . Then

$|x + y| \le |x| + |y|.$

Facts & Assumptions

Given: An ordered field $F$ and elements $x, y \in F$ .

[L1]

For every $u \in F$ , $-|u| \le u \le |u|$ , and $|u|$ equals $u$ or $-u$ (Basic properties of the absolute value).

[L2]

Order compatible with addition: if $a \le b$ and $c \le d$ , then $a + c \le b + d$ . Order is preserved by adding a constant and by adding inequalities states the STRICT forms and only those ( $a < b \Rightarrow a + c < b + c$ , and $a < b$ with $c < d$ giving $a + c < b + d$ ); the nonstrict form used here is those two together with the cases $a = b$ and $c = d$ , settled by trichotomy, the order being total (Ordered field). Explicitly: if $a < b$ and $c < d$ the second strict form applies; if $a < b$ and $c = d$ the first gives $a + c < b + c = b + d$ ; if $a = b$ and $c < d$ the first gives $a + c < a + d = b + d$ ; and if $a = b$ and $c = d$ the two sides are equal.

[L3]

Field and order arithmetic: $-(a + b) = -a + (-b)$ , and $a \le b \iff -b \le -a$ (Ordered field).

Proof

technique · direct

1.1

By [L1], $-|x| \le x \le |x|$ and $-|y| \le y \le |y|$ .

2.1

Adding the two chains of [step 1.1] with [L2] and using $-(|x| + |y|) = -|x| + (-|y|)$ from [L3] gives $-(|x| + |y|) \le x + y \le |x| + |y|$ .

step 1.1L2L3

3.1

By [L1] the value $|x + y|$ equals $x + y$ or $-(x + y)$ ; both $x + y \le |x| + |y|$ and $-(x + y) \le |x| + |y|$ hold by [step 2.1] and [L3] (the latter from $-(|x| + |y|) \le x + y$ ), so $|x + y| \le |x| + |y|$ .

step 2.1L1L3∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

The reverse triangle inequality

Statement

Let $F$ be an ordered field (Ordered field) and let $x, y \in F$ . Then

$\bigl| |x| - |y| \bigr| \le |x - y|.$

Facts & Assumptions

Given: An ordered field $F$ and elements $x, y \in F$ .

[L1]

Triangle inequality: $|a + b| \le |a| + |b|$ for all $a, b \in F$ (The triangle inequality).

[L2]

For every $u \in F$ , $|-u| = |u|$ , and $|w|$ equals $w$ or $-w$ (Basic properties of the absolute value).

Proof

technique · direct

1.1

Applying [L1] with $a = x - y$ and $b = y$ gives $|x| = |(x - y) + y| \le |x - y| + |y|$ , so $|x| - |y| \le |x - y|$ .

1.2

Applying [L1] with $a = y - x$ and $b = x$ , and using $|y - x| = |x - y|$ from [L2], gives $|y| \le |y - x| + |x| = |x - y| + |x|$ , so $|y| - |x| \le |x - y|$ .

L1L2

2.1

By [L2] the value $\bigl| |x| - |y| \bigr|$ equals $|x| - |y|$ or $-(|x| - |y|) = |y| - |x|$ , and each of these is $\le |x - y|$ by steps 1.1 and 1.2, so $\bigl| |x| - |y| \bigr| \le |x - y|$ .

step 1.1step 1.2L2algebra∎

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Squaring is monotone on the nonnegatives

Statement

Let $F$ be an ordered field. For $a, b \ge 0$ :

$a < b \iff a^2 < b^2, \qquad a \le b \iff a^2 \le b^2.$

More generally, for arbitrary $a, b \in F$ , $a^2 < b^2 \iff |a| < |b|$ .

Facts & Assumptions

Given: Elements $a, b$ of an ordered field $F$ .

[L1]

For a positive factor $s > 0$ and any $t$ : $t > 0 \iff st > 0$ ; this is Sign rules for products and monotonicity of multiplication (the rule $c > 0 \Rightarrow (x < y \iff xc < yc)$ taken at $x = 0$ , $y = t$ , $c = s$ , using $0 \cdot s = 0$ , Multiplication by zero: $0 \cdot a = 0$ ).

[L2]

Trichotomy: for $a, b$ exactly one of $a < b$ , $a = b$ , $a > b$ holds; and a sum of two nonnegatives with at least one positive is positive (Ordered field).

[L3]

$|x| \ge 0$ and $|x|^2 = x^2$ for every $x$ (Basic properties of the absolute value).

Proof

technique · direct

1.1

The difference factors as $b^2 - a^2 = (b - a)(b + a)$ .

algebra

2.1

If $a, b \ge 0$ and $a < b$ , then $b > 0$ , so $b + a > 0$ by [L2], and $b - a > 0$ ; by [L1] with $s = b + a$ and $t = b - a$ , $(b - a)(b + a) > 0$ , i.e. $a^2 < b^2$ .

L1L2step 1.1

2.2

If $a, b \ge 0$ and $a^2 < b^2$ , then $b^2 - a^2 > 0$ , so $a, b$ are not both zero and $b + a > 0$ by [L2]; by [L1] with $s = b + a$ , from $(b - a)(b + a) = b^2 - a^2 > 0$ we get $b - a > 0$ , i.e. $a < b$ .

L1L2step 1.1

3.1

Hence for $a, b \ge 0$ , $a < b \iff a^2 < b^2$ .

step 2.1step 2.2

4.1

The $\le$ form follows by trichotomy: for $a, b \ge 0$ , applying step 3.1 to the nonnegatives $b, a$ gives $a \le b \iff \lnot(b < a) \iff \lnot(b^2 < a^2) \iff a^2 \le b^2$ .

step 3.1L2

5.1

For arbitrary $a, b$ , [L3] gives $|a|, |b| \ge 0$ with $|a|^2 = a^2$ and $|b|^2 = b^2$ ; applying step 3.1 to $|a|, |b|$ yields $a^2 < b^2 \iff |a|^2 < |b|^2 \iff |a| < |b|$ .

step 3.1L3∎

PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Reciprocals and order: $1/r$ against $1$

Statement

Let $F$ be an ordered field and let $r \in F$ with $r > 0$ . Then:

$0 < r < 1 \iff \tfrac{1}{r} > 1, \qquad r > 1 \iff 0 < \tfrac{1}{r} < 1, \qquad r = 1 \iff \tfrac{1}{r} = 1.$

Here $\tfrac{1}{r}$ denotes the multiplicative inverse $r^{-1}$ .

Facts & Assumptions

Given: An element $r > 0$ of an ordered field $F$ .

[L1]

If $x > 0$ then $x^{-1} > 0$ (Inverses of positives are positive, and reciprocation reverses order).

[L2]

If $0 < x < y$ then $0 < y^{-1} < x^{-1}$ : the reciprocal reverses order on the positives (Inverses of positives are positive, and reciprocation reverses order).

[L3]

$0 < 1$ (The multiplicative identity is positive).

[L4]

In any field, $1^{-1} = 1$ and $(x^{-1})^{-1} = x$ for $x \ne 0$ (Field).

Proof

technique · direct

1.1

Since $r > 0$ , [L1] gives $r^{-1} > 0$ , so $\tfrac{1}{r}$ is positive throughout.

1.2

In particular $1^{-1} = 1$ and $(r^{-1})^{-1} = r$ by uniqueness of inverses.

2.1

If $0 < r < 1$ , applying [L2] to $0 < r < 1$ gives $0 < 1^{-1} < r^{-1}$ , that is $1 < \tfrac{1}{r}$ .

L2step 1.2

2.2

Conversely, if $\tfrac{1}{r} > 1$ , then $0 < 1 < \tfrac{1}{r}$ by [L3], and applying [L2] gives $0 < (r^{-1})^{-1} < 1^{-1}$ , that is $0 < r < 1$ .

L2L3step 1.2

2.3

If $r > 1$ , then $0 < 1 < r$ by [L3], and applying [L2] gives $0 < r^{-1} < 1^{-1}$ , that is $0 < \tfrac{1}{r} < 1$ .

L2L3step 1.2

2.4

Conversely, if $0 < \tfrac{1}{r} < 1$ , applying [L2] to $0 < r^{-1} < 1$ gives $0 < 1^{-1} < (r^{-1})^{-1}$ , that is $1 < r$ .

L2step 1.2

2.5

If $r = 1$ then $\tfrac{1}{r} = 1^{-1} = 1$ ; conversely if $\tfrac{1}{r} = 1$ then $r = (r^{-1})^{-1} = 1^{-1} = 1$ .

step 1.2

3.1

Combining the two directions in each case: $0 < r < 1 \iff \tfrac{1}{r} > 1$ , and $r > 1 \iff 0 < \tfrac{1}{r} < 1$ , and $r = 1 \iff \tfrac{1}{r} = 1$ .

step 2.1step 2.2step 2.3step 2.4step 2.5∎

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

The sign of a product

Statement

Let $F$ be an ordered field and let $a, b \in F$ . Then:

$ab > 0 \iff a, b \text{ have the same sign}, \qquad ab < 0 \iff a, b \text{ have opposite signs},$

$ab = 0 \iff a = 0 \text{ or } b = 0.$

Here "same sign" means both positive or both negative, and "opposite signs" means one positive and one negative.

Facts & Assumptions

Given: Elements $a, b$ of an ordered field $F$ .

[L1]

Trichotomy: each $x \in F$ satisfies exactly one of $x > 0$ , $x = 0$ , $x < 0$ (Ordered field).

[L2]

Sign rules: if $x, y > 0$ then $xy > 0$ ; if $x > 0$ and $y < 0$ then $xy < 0$ ; if $x, y < 0$ then $xy > 0$ (Sign rules for products and monotonicity of multiplication).

[L3]

If $xy = 0$ then $x = 0$ or $y = 0$ (A field has no zero divisors: $ab = 0 \Rightarrow a = 0$ or $b = 0$ ).

[L4]

$0 \cdot x = 0$ and $x \cdot 0 = 0$ (Multiplication by zero: $0 \cdot a = 0$ ).

Proof

technique · cases

1.1

If $a = 0$ or $b = 0$ then $ab = 0$ by [L4], and conversely if $ab = 0$ then $a = 0$ or $b = 0$ by [L3]; hence $ab = 0 \iff a = 0$ or $b = 0$ , which is the third biconditional.

L3L4

1.2

For the first two biconditionals assume $a \ne 0$ and $b \ne 0$ ; by trichotomy [L1] each of $a, b$ is then either positive or negative, giving four sign combinations.

2.1

Case $a > 0$ and $b > 0$ (both positive, same sign): $ab > 0$ by [L2].

assume-case posposL2step 1.2

2.2

Case $a < 0$ and $b < 0$ (both negative, same sign): $ab > 0$ by [L2].

assume-case negnegL2step 1.2

2.3

Case $a > 0$ and $b < 0$ (opposite signs): $ab < 0$ by [L2].

assume-case posnegL2step 1.2

2.4

Case $a < 0$ and $b > 0$ (opposite signs): $ab < 0$ by [L2].

assume-case negposL2step 1.2

3.1

By trichotomy [L1] these four cases exhaust every sign combination of the nonzero $a, b$ and are mutually exclusive.

step 2.1step 2.2step 2.3step 2.4cases-exhaustive

4.1

For nonzero $a, b$ we have $ab \ne 0$ by step 1.1, so by trichotomy $ab$ is either $> 0$ or $< 0$ ; from the cases, $ab > 0$ occurs exactly in the same-sign cases 2.1 and 2.2, and $ab < 0$ exactly in the opposite-sign cases 2.3 and 2.4.

step 1.1step 3.1L1

5.1

Therefore $ab > 0 \iff a, b$ have the same sign, and $ab < 0 \iff a, b$ have opposite signs; with step 1.1 all three biconditionals hold.

step 1.1step 4.1∎

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Multiplying inequalities of positives

Statement

Let $F$ be an ordered field. If $0 < a < b$ and $0 < c < d$ then $ac < bd$ . If $0 \le a \le b$ and $0 \le c \le d$ then $ac \le bd$ .

Facts & Assumptions

Given: Elements $a, b, c, d$ of an ordered field $F$ .

[L1]

For a positive multiplier $c > 0$ : $x < y \iff xc < yc$ ; multiplying a strict inequality by a positive element preserves it (Sign rules for products and monotonicity of multiplication).

[L2]

For $c \ge 0$ : $x \le y \Rightarrow xc \le yc$ ; the case $c > 0$ is [L1] and the case $c = 0$ gives $0 \le 0$ (Sign rules for products and monotonicity of multiplication).

[L3]

The order is transitive: if $x < y$ and $y < z$ then $x < z$ , and likewise for $\le$ , since the positive cone is closed under addition (Ordered field).

Proof

technique · direct

1.1

Assume $0 < a < b$ and $0 < c < d$ ; since $c > 0$ , scaling $a < b$ by $c$ gives $ac < bc$ .

1.2

Since $b > 0$ (from $0 < a < b$ ), scaling $c < d$ by $b$ gives $bc < bd$ .

1.3

Assume instead $0 \le a \le b$ and $0 \le c \le d$ ; since $c \ge 0$ , from $a \le b$ we get $ac \le bc$ .

1.4

Since $b \ge 0$ (from $0 \le a \le b$ ), from $c \le d$ we get $bc \le bd$ .

2.1

By transitivity, $ac < bc < bd$ , hence $ac < bd$ , proving the strict claim.

L3step 1.1step 1.2

2.2

By transitivity of $\le$ , $ac \le bc \le bd$ , hence $ac \le bd$ , proving the nonstrict claim.

L3step 1.3step 1.4

3.1

Both the strict and the nonstrict inequalities hold.

step 2.1step 2.2∎

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

When $ab < b$ for positive $a, b$

Statement

Let $F$ be an ordered field and let $a, b \in F$ with $a > 0$ and $b > 0$ . Then:

$0 < ab < b \iff 0 < a < 1.$

Facts & Assumptions

Given: Elements $a, b$ of an ordered field $F$ with $a > 0$ and $b > 0$ .

[L1]

If $x > 0$ and $y > 0$ then $xy > 0$ : the positive cone is closed under multiplication (Ordered field).

[L2]

$x < y \iff x - y < 0 \iff y - x > 0$ (Ordered field).

[L3]

For $b > 0$ : $bz < 0 \iff z < 0$ ; the sign of $bz$ equals the sign of $z$ (Sign rules for products and monotonicity of multiplication).

[L4]

By distributivity and $b \cdot (-1) = -b$ , one has $ab - b = b(a - 1)$ (Sign rules for products: $(-a)b = -(ab)$ and $(-a)(-b) = ab$ ).

Proof

technique · direct

1.1

Since $a > 0$ and $b > 0$ , [L1] gives $ab > 0$ .

1.2

By [L4], $ab - b = b(a - 1)$ .

2.1

By [L2], $ab < b \iff ab - b < 0$ , and by step 1.2 this is $b(a - 1) < 0$ .

L2step 1.2

2.2

By [L3] with $z = a - 1$ , we have $b(a - 1) < 0 \iff a - 1 < 0$ , and by [L2] this is $a < 1$ .

L3L2step 1.2

3.1

Chaining, $ab < b \iff a < 1$ ; since $a > 0$ is given and $ab > 0$ by step 1.1, this is exactly $0 < ab < b \iff 0 < a < 1$ .

givenstep 1.1step 2.1step 2.2∎

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-27Open item page →

The canonical natural $\iota(n) = n \cdot 1_F$ of a field

Definition

Let $F$ be a field (Field) with additive identity $0_F$ and multiplicative identity $1_F$ . Define $\iota : \mathbb{N} \to F$ by recursion on $\mathbb{N}$ (The natural numbers $\mathbb{N}$ (von Neumann), The recursion theorem):

$\iota(0) \;:=\; 0_F, \qquad \iota(n+1) \;:=\; \iota(n) + 1_F .$

$\iota(n)$ is the canonical natural of $n$ in $F$ . It is also written $n \cdot 1_F$ , and for $n \ge 1$ it is $1_F$ added to itself $n$ times.

Why the notation is needed at all. A natural number in this library is a von Neumann natural, that is a set (The natural numbers $\mathbb{N}$ (von Neumann)), and a set is not an element of $F$ . So $1/n$ , $n^{\alpha}$ and $x/n$ are not expressions of $F$ when $n$ is a natural: what they mean is $1/\iota(n)$ , $\iota(n)^{\alpha}$ and $x/\iota(n)$ . The map $\iota$ is what carries a counting number into the field, and writing it is the whole reason a reader meets $1/\iota(k+1)$ where an informal text would write $1/(k+1)$ .

Remarks

Where the index shift comes from. $\mathbb{N}$ contains $0$ (The natural numbers $\mathbb{N}$ (von Neumann)) and $\iota(0) = 0_F$ , so $1/\iota(k)$ is undefined at $k = 0$ . A family of reciprocals indexed by $\mathbb{N}$ is therefore written over $\iota(k+1)$ , which is why the harmonic and telescoping families of this library run over $k+1$ rather than over $k$ . This is bookkeeping, not a restriction: the values are the usual ones.
This definition records notation; the arithmetic is proved elsewhere. That $\iota$ is strictly increasing and positive on $n \ge 1$ , and that it carries sums to sums and products to products, is Canonical naturals are positive and strictly increasing, stated for an ordered field. That lemma introduces the same element by the equivalent recursion $1 \cdot 1_F = 1_F$ , $(n+1) \cdot 1_F = n \cdot 1_F + 1_F$ , which agrees with the definition above because $\iota(1) = \iota(0) + 1_F = 1_F$ . Nothing here is new mathematics; the definition exists so that the notation has a home a reader can look up.
The symbol $\iota$ is used in this library for other canonical maps, and this definition does not govern them. It also denotes the canonical field embedding $\iota : \mathbb{Q} \to F$ (The unique embedding of ℚ into an ordered field), the isometric embedding of a metric space into a completion (A completion of a metric space: a complete metric space together with an isometric embedding onto a dense subspace ↗), and an inclusion map $\iota : S \to X$ of a subspace. Each of those is introduced where it is used and means something different from the map defined here. What the four share is only that each is the canonical map of its situation.
Fields, not just ordered fields. The recursion needs no order, so the definition is stated for a field; every use in this library is in an ordered field, and the order is what makes $\iota$ injective (Canonical naturals are positive and strictly increasing). In a field of positive characteristic $\iota$ is not injective, which is one reason the injectivity is a lemma rather than part of the definition.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Canonical naturals are positive and strictly increasing

Statement

Let $F$ be an ordered field, with field structure as in Field, and for $n \ge 1$ let $n \cdot 1_F$ denote the canonical natural number $\underbrace{1_F + \cdots + 1_F}_{n}$ , defined recursively by $1 \cdot 1_F = 1_F$ and $(n+1) \cdot 1_F = n \cdot 1_F + 1_F$ . Then for every $n \ge 1$ :

$n \cdot 1_F > 0$ and $(n+1) \cdot 1_F > n \cdot 1_F$ ;
the map $n \mapsto n \cdot 1_F$ is strictly increasing, hence injective, on $\{1, 2, 3, \dots\}$ ;
$(m+n) \cdot 1_F = m \cdot 1_F + n \cdot 1_F$ and $(mn) \cdot 1_F = (m \cdot 1_F)(n \cdot 1_F)$ for all $m, n \ge 1$ .

Facts & Assumptions

Given: An ordered field $F$ whose canonical naturals are defined recursively by $1 \cdot 1_F = 1_F$ and $(n+1) \cdot 1_F = n \cdot 1_F + 1_F$ , with $0 \cdot 1_F = 0$ .

[L1]

$0 < 1_F$ in every ordered field (The multiplicative identity is positive).

[L2]

The order is compatible with addition and positives are closed under addition: $a < b$ implies $a + c < b + c$ , and $a > 0$ , $b > 0$ imply $a + b > 0$ (Order is preserved by adding a constant and by adding inequalities).

Proof

technique · induction

1.1

Base case $n = 1$ : by definition $1 \cdot 1_F = 1_F$ , and $1_F > 0$ .

L1base

1.2

Inductive hypothesis: assume $n \cdot 1_F > 0$ for some fixed $n \ge 1$ .

1.3

By the recursion, $(n+1) \cdot 1_F - n \cdot 1_F = 1_F > 0$ , so $(n+1) \cdot 1_F > n \cdot 1_F$ .

givenL1

1.4

Additive identity: fix $m$ and induct on $n$ ; at $n = 1$ , $(m+1) \cdot 1_F = m \cdot 1_F + 1_F$ by the recursion, and if $(m+n) \cdot 1_F = m \cdot 1_F + n \cdot 1_F$ then $(m+n+1) \cdot 1_F = (m+n) \cdot 1_F + 1_F = m \cdot 1_F + n \cdot 1_F + 1_F = m \cdot 1_F + (n+1) \cdot 1_F$ .

givenalgebra

2.1

Inductive step: $(n+1) \cdot 1_F = n \cdot 1_F + 1_F$ is a sum of two positives, by the hypothesis and $1_F > 0$ , hence $(n+1) \cdot 1_F > 0$ .

step 1.2L1L2

2.2

Iterating 1.3, for $m < n$ one has $m \cdot 1_F < n \cdot 1_F$ , so $n \mapsto n \cdot 1_F$ is strictly increasing and therefore injective on $\{1, 2, 3, \dots\}$ .

step 1.3L2

2.3

Multiplicative identity: fix $m$ and induct on $n$ ; at $n = 1$ , $(m \cdot 1) \cdot 1_F = m \cdot 1_F = (m \cdot 1_F)(1 \cdot 1_F)$ , and the step $(m(n+1)) \cdot 1_F = (mn + m) \cdot 1_F = (mn) \cdot 1_F + m \cdot 1_F = (m \cdot 1_F)(n \cdot 1_F) + (m \cdot 1_F)(1_F) = (m \cdot 1_F)((n+1) \cdot 1_F)$ uses 1.4 and distributivity.

step 1.4algebra

3.1

By induction on 1.1, 1.2, 2.1, $n \cdot 1_F > 0$ for every $n \ge 1$ ; with the strict increase 2.2 and the identities 1.4, 2.3, every claim holds.

step 2.1step 2.2step 1.4step 2.3discharge-induction∎

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

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 \ge 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$ .

Facts & Assumptions

Given: A complete ordered field $F$ ; write $A = \{\, n \cdot 1_F : n \ge 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.1

Suppose, for contradiction, that $F$ is not Archimedean: there is some $x \in F$ with $n \cdot 1_F \le x$ for all $n \ge 1$ , that is, $x$ is an upper bound of $A$ .

assume-contra

2.1

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

step 1.1L2

3.1

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

step 2.1L1

4.1

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$ .

step 3.1L3

5.1

Hence there is some $m \ge 1$ with $m \cdot 1_F > s - 1_F$ .

step 4.1

6.1

Adding $1_F$ to both sides, $(m+1) \cdot 1_F = m \cdot 1_F + 1_F > s$ .

step 5.1L2

7.1

But $(m+1) \cdot 1_F \in A$ , so $(m+1) \cdot 1_F \le s$ because $s$ is an upper bound of $A$ , contradicting 6.1.

step 6.1step 3.1L2

8.1

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

step 7.1discharge-contradiction∎

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26Open item page →

For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$

Statement

Let $F$ be a complete ordered field (Complete ordered field (least-upper-bound property)) and let $\varepsilon \in F$ with $\varepsilon > 0$ . Then there is a natural number $n \ge 1$ such that

$\frac{1}{n \cdot 1_F} < \varepsilon ,$

where $n \cdot 1_F$ is the canonical natural of $F$ (Every complete ordered field is Archimedean) and $1/(n \cdot 1_F)$ is its multiplicative inverse (Field). As is standard we abbreviate $n \cdot 1_F$ to $n$ and write the conclusion $1/n < \varepsilon$ .

This is the reciprocal form of the Archimedean property. Every complete ordered field is Archimedean on its own delivers only the assertion that the canonical naturals are cofinal, $x < n \cdot 1_F$ ; the form actually used in analysis, that the reciprocals of the naturals get below every positive bound, is the statement above, and it is recorded separately so that no proof has to reconstruct the inversion step in passing.

Facts & Assumptions

Given: A complete ordered field $F$ and an element $\varepsilon \in F$ with $\varepsilon > 0$ .

[L1]

Archimedean property: for every $x \in F$ there is a natural number $n \ge 1$ with $x < n \cdot 1_F$ (Every complete ordered field is Archimedean, Complete ordered field (least-upper-bound property)).

[L2]

Inverses and order: if $a > 0$ then $a^{-1} > 0$ , and if $0 < a < b$ then $0 < b^{-1} < a^{-1}$ (Inverses of positives are positive, and reciprocation reverses order, Ordered field).

[L3]

Field arithmetic: an element $a$ with $a > 0$ is nonzero by trichotomy, hence has a multiplicative inverse $a^{-1}$ , and $(a^{-1})^{-1} = a$ (Field, Ordered field).

Proof

technique · direct

1.1

Since $\varepsilon > 0$ , trichotomy gives $\varepsilon \ne 0$ , so $\varepsilon^{-1}$ exists, and $\varepsilon^{-1} > 0$ .

givenL2L3

2.1

Apply [L1] to $x = \varepsilon^{-1}$ : fix a natural number $n \ge 1$ with $\varepsilon^{-1} < n \cdot 1_F$ .

step 1.1L1choose

3.1

Chaining the two displayed inequalities gives $0 < \varepsilon^{-1} < n \cdot 1_F$ ; in particular $n \cdot 1_F > 0$ , so $n \cdot 1_F \ne 0$ and $1/(n \cdot 1_F)$ is defined.

step 1.1step 2.1L3

4.1

Apply the second claim of [L2] with $a = \varepsilon^{-1}$ and $b = n \cdot 1_F$ : $0 < (n \cdot 1_F)^{-1} < (\varepsilon^{-1})^{-1}$ .

step 3.1L2

5.1

By [L3], $(\varepsilon^{-1})^{-1} = \varepsilon$ , so the natural number $n \ge 1$ fixed in step 2.1 satisfies $1/(n \cdot 1_F) < \varepsilon$ , which is the assertion.

step 4.1L3∎

Remarks

Monotonicity gives the eventual form for free. If $m \ge n \ge 1$ then $m \cdot 1_F \ge n \cdot 1_F > 0$ , because $k \mapsto k \cdot 1_F$ is strictly increasing on the naturals $\ge 1$ (Canonical naturals are positive and strictly increasing), and so $1/(m \cdot 1_F) \le 1/(n \cdot 1_F) < \varepsilon$ by Inverses of positives are positive, and reciprocation reverses order again. So the corollary yields not merely one index but a threshold: every $m \ge n$ satisfies $1/m < \varepsilon$ . That one extra line is what a convergence proof needs, and it is left to the caller rather than folded into the statement, because the caller usually has a threshold of its own to combine it with.
Completeness is used only through Every complete ordered field is Archimedean. Nothing here needs the least-upper-bound property directly. The corollary therefore holds verbatim in any Archimedean ordered field, in particular in $\mathbb{Q}$ , and it fails in a non-Archimedean ordered field, where an infinitesimal $\varepsilon > 0$ is below every $1/n$ by construction.
The equivalence is exact: the reciprocal form implies the cofinal form back again, since given $x > 0$ one applies it to $\varepsilon = 1/x$ . The two are the same property written on the two sides of the inversion, and only the direction proved above is used in this library.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

The unique embedding of ℚ into an ordered field

Statement

Let $F$ be an ordered field (Ordered field). There is a unique field homomorphism $\iota : \mathbb{Q} \to F$ (Field homomorphism and embedding). On the integers it is given by $n \mapsto n \cdot 1_F$ (with $-n \mapsto -(n \cdot 1_F)$ and $0 \mapsto 0$ ), and on a rational written as $p/q$ with $q \ge 1$ by $\iota(p/q) = \iota(p)\,(q \cdot 1_F)^{-1}$ . Moreover $\iota$ is injective and order-preserving, so it is an embedding of $\mathbb{Q}$ as an ordered subfield of $F$ , and it is the only field homomorphism $\mathbb{Q} \to F$ .

Facts & Assumptions

Given: An ordered field $F$ ; the field $\mathbb{Q}$ of The rationals form a totally ordered field, every element of which is $0$ or $\pm p/q$ with integers $p, q \ge 1$ . For an integer $p$ write $\iota(p)$ for $p \cdot 1_F$ if $p \ge 0$ and $-(|p| \cdot 1_F)$ if $p < 0$ .

[L1]

$\mathbb{Q}$ is an ordered field; a nonzero $p/q$ with $q \ge 1$ is positive exactly when $p \ge 1$ (The rationals form a totally ordered field).

[L2]

The canonical naturals satisfy $n \cdot 1_F > 0$ for $n \ge 1$ , $n \mapsto n \cdot 1_F$ is injective, $(m+n) \cdot 1_F = m \cdot 1_F + n \cdot 1_F$ , and $(mn) \cdot 1_F = (m \cdot 1_F)(n \cdot 1_F)$ (Canonical naturals are positive and strictly increasing).

[L3]

If $a > 0$ then $a^{-1} > 0$ (Inverses of positives are positive, and reciprocation reverses order).

[L4]

Sign rules: a product of positives is positive, and for $c > 0$ one has $a < b$ iff $ac < bc$ (Sign rules for products and monotonicity of multiplication).

[L5]

A field homomorphism preserves $+$ , $\cdot$ , and $1$ , and hence $0$ , negation, and inverses (Field homomorphism and embedding).

Proof

technique · direct

1.1

Define $\iota$ on the integers by $\iota(n) = n \cdot 1_F$ for $n \ge 0$ and $\iota(-n) = -(n \cdot 1_F)$ ; by [L2] this is additive and multiplicative on $\mathbb{Z}$ and sends $1 \mapsto 1_F$ .

1.2

For a rational $x = p/q$ with $q \ge 1$ define $\iota(x) = \iota(p)\,(q \cdot 1_F)^{-1}$ , which makes sense because $q \cdot 1_F > 0 \ne 0$ has an inverse.

2.1

Well-defined: if $p/q = p'/q'$ with $q, q' \ge 1$ , then $p q' = p' q$ in $\mathbb{Z}$ , so [L2] gives $\iota(p)(q' \cdot 1_F) = \iota(p')(q \cdot 1_F)$ , and multiplying by the positive $(q \cdot 1_F)^{-1}(q' \cdot 1_F)^{-1}$ yields $\iota(p)(q \cdot 1_F)^{-1} = \iota(p')(q' \cdot 1_F)^{-1}$ ; thus $\iota(x)$ is independent of the representative.

step 1.1step 1.2L2L3

2.2

Multiplicativity: for $x = p/q$ , $y = r/s$ one has $xy = (pr)/(qs)$ , and $\iota(xy) = \iota(pr)((qs) \cdot 1_F)^{-1} = \iota(p)\iota(r)(q \cdot 1_F)^{-1}(s \cdot 1_F)^{-1} = \iota(x)\iota(y)$ , using $(mn) \cdot 1_F = (m \cdot 1_F)(n \cdot 1_F)$ and $(uv)^{-1} = u^{-1} v^{-1}$ .

step 1.2L2

2.3

Additivity: with $x + y = (ps + rq)/(qs)$ , $\iota(x+y) = (\iota(p)(s \cdot 1_F) + \iota(r)(q \cdot 1_F))(q \cdot 1_F)^{-1}(s \cdot 1_F)^{-1} = \iota(p)(q \cdot 1_F)^{-1} + \iota(r)(s \cdot 1_F)^{-1} = \iota(x) + \iota(y)$ , using the additive and multiplicative identities of [L2].

step 1.2L2

2.4

Positivity: if $x = p/q > 0$ in $\mathbb{Q}$ with $q \ge 1$ , then $p \ge 1$ by [L1], so $\iota(p) = p \cdot 1_F > 0$ and $q \cdot 1_F > 0$ by [L2], whence $(q \cdot 1_F)^{-1} > 0$ by [L3] and $\iota(x) = \iota(p)(q \cdot 1_F)^{-1} > 0$ by [L4].

step 1.2L1L2L3L4

2.5

Uniqueness on $\mathbb{Z}$ : let $\psi : \mathbb{Q} \to F$ be any field homomorphism; then $\psi(1) = 1_F$ , additivity forces $\psi(n) = n \cdot 1_F = \iota(n)$ for $n \ge 1$ , and $\psi(0) = 0$ , $\psi(-n) = -(n \cdot 1_F)$ , so $\psi = \iota$ on $\mathbb{Z}$ .

step 1.1L5

3.1

Unit: $\iota(1) = \iota(1/1) = \iota(1)(1 \cdot 1_F)^{-1} = 1_F$ ; hence $\iota$ is a field homomorphism $\mathbb{Q} \to F$ .

step 2.2step 2.3L2L5

3.2

Order: for $x < y$ in $\mathbb{Q}$ we have $y - x > 0$ , so $\iota(y) - \iota(x) = \iota(y - x) > 0$ by 2.3 and 2.4, that is $\iota(x) < \iota(y)$ ; thus $\iota$ is order-preserving.

step 2.3step 2.4

4.1

Injectivity: if $x \ne y$ then $x < y$ or $y < x$ , and 3.2 forces $\iota(x) \ne \iota(y)$ ; so $\iota$ is injective, an embedding of ordered fields.

step 3.2

5.1

Uniqueness on $\mathbb{Q}$ : for $p/q \in \mathbb{Q}$ , $\psi(p/q) = \psi(p)\psi(q)^{-1} = \iota(p)(q \cdot 1_F)^{-1} = \iota(p/q)$ since $\psi$ preserves products and inverses; hence $\psi = \iota$ , so $\iota$ is the unique field homomorphism $\mathbb{Q} \to F$ .

step 2.5step 1.2L5∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-07-25Open item page →

ℚ is dense in every Archimedean ordered field

Statement

Let $F$ be an Archimedean ordered field (Archimedean ordered field) and let $\iota : \mathbb{Q} \to F$ be the canonical embedding (The unique embedding of ℚ into an ordered field). Then $\iota(\mathbb{Q})$ is dense in $F$ : for any $x < y$ in $F$ there is a rational $q$ with $x < \iota(q) < y$ .

Facts & Assumptions

Given: An Archimedean ordered field $F$ with canonical embedding $\iota : \mathbb{Q} \to F$ , and elements $x < y$ of $F$ .

[L1]

Archimedean property: for every $w \in F$ there is $n \ge 1$ with $w < n \cdot 1_F$ (Archimedean ordered field).

[L2]

$\iota$ is an order-preserving field homomorphism with $\iota(m/n) = \iota(m)\,(n \cdot 1_F)^{-1}$ for $n \ge 1$ (The unique embedding of ℚ into an ordered field).

[L3]

Canonical naturals: $n \cdot 1_F > 0$ for $n \ge 1$ , and $(m+n) \cdot 1_F = m \cdot 1_F + n \cdot 1_F$ (Canonical naturals are positive and strictly increasing).

[L4]

If $a > 0$ then $a^{-1} > 0$ (Inverses of positives are positive, and reciprocation reverses order).

[L5]

Sign rules: for $c > 0$ one has $a < b$ iff $ac < bc$ , and products of positives are positive (Sign rules for products and monotonicity of multiplication).

[L6]

Every nonempty $T \subseteq \mathbb{Z}$ that is bounded below has a least element: if $k > -M$ for every $k \in T$ then $\{k + M : k \in T\}$ is a nonempty set of naturals, which has a least element, and subtracting $M$ returns the least element of $T$ (The well-ordering principle, The naturals embed in the integers, Order on the integers).

Proof

technique · direct

1.1

Since $x < y$ , the element $y - x > 0$ , so it is nonzero and its inverse $(y - x)^{-1}$ exists in the field $F$ ; by the Archimedean property applied to $(y - x)^{-1}$ , choose $n \ge 1$ with $(y - x)^{-1} < n \cdot 1_F$ .

L1L4choose

1.2

By [L1] applied to $(n \cdot 1_F)\,x$ there is a natural $N$ with $(n \cdot 1_F)\,x < N \cdot 1_F$ , so the set $T = \{\, k \in \mathbb{Z} : k \cdot 1_F > (n \cdot 1_F)\,x \,\}$ is nonempty ( $N \in T$ ); by [L1] applied to $-(n \cdot 1_F)\,x$ there is a natural $M$ with $-(n \cdot 1_F)\,x < M \cdot 1_F$ , so every $k \in T$ satisfies $k \cdot 1_F > (n \cdot 1_F)\,x > -M \cdot 1_F$ , hence $k > -M$ (were $k \le -M$ , monotonicity of $k \mapsto k \cdot 1_F = \iota(k)$ on $\mathbb{Z}$ , which is [L2], would force $k \cdot 1_F \le -M \cdot 1_F$ , against $k \cdot 1_F > -M \cdot 1_F$ ), so $T$ is bounded below by $-M$ , and therefore has a least element $m$ .

L1L2L3L6choose

2.1

Multiplying $(y - x)^{-1} < n \cdot 1_F$ by the positive $(n \cdot 1_F)^{-1}(y - x)$ gives $(n \cdot 1_F)^{-1} < y - x$ .

step 1.1L4L5

2.2

By minimality of $m$ , $(m-1) \cdot 1_F \le (n \cdot 1_F)\,x < m \cdot 1_F$ .

step 1.2

3.1

Set $q = m/n \in \mathbb{Q}$ , so $\iota(q) = \iota(m)(n \cdot 1_F)^{-1}$ ; dividing $(n \cdot 1_F)\,x < m \cdot 1_F$ by the positive $n \cdot 1_F$ gives $x < \iota(m)(n \cdot 1_F)^{-1} = \iota(q)$ .

step 2.2L2L4L5

3.2

From $(m-1) \cdot 1_F = m \cdot 1_F - 1_F \le (n \cdot 1_F)\,x$ , dividing by the positive $n \cdot 1_F$ gives $\iota(q) - (n \cdot 1_F)^{-1} \le x$ , that is $\iota(q) \le x + (n \cdot 1_F)^{-1}$ .

step 2.2L3L4L5

4.1

Combining with 2.1, $\iota(q) \le x + (n \cdot 1_F)^{-1} < x + (y - x) = y$ .

step 3.2step 2.1

5.1

Therefore $x < \iota(q) < y$ with $q = m/n \in \mathbb{Q}$ , so $\iota(\mathbb{Q})$ is dense in $F$ .

step 3.1step 4.1∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$

Statement

Let $F$ be a complete ordered field (Complete ordered field (least-upper-bound property)). Then every $a \in F$ with $a \ge 0$ has a unique $s \in F$ with $s \ge 0$ and $s^2 = a$ ; we write $s = \sqrt{a}$ . Consequently the positive elements of $F$ are exactly the nonzero squares: $x > 0$ if and only if $x = y^2$ for some $y \neq 0$ .

Facts & Assumptions

Given: A complete ordered field $F$ (Complete ordered field (least-upper-bound property)), that is, an ordered field (Ordered field) with the least-upper-bound property, and an element $a \in F$ with $a \ge 0$ .

[L1]

Every nonempty subset of $F$ that is bounded above has a least upper bound in $F$ (Complete ordered field (least-upper-bound property)).

[L2]

Sign and scaling rules: a product of positives is positive, and for $c > 0$ one has $x < y \iff cx < cy$ (Sign rules for products and monotonicity of multiplication).

[L3]

Squaring is strictly monotone on the nonnegatives: if $0 \le x < y$ then $x^2 < y^2$ ; in particular squaring is injective on $\{x : x \ge 0\}$ (Squaring is monotone on the nonnegatives).

[L4]

A nonzero square is positive: if $y \neq 0$ then $y^2 > 0$ (Squares of nonzero elements are positive).

[L5]

Multiplying inequalities of positives: if $0 < x < y$ and $0 < u < v$ then $xu < yv$ (Multiplying inequalities of positives).

Proof

technique · contradiction

1.1

If $a = 0$ , then $s = 0$ satisfies $s \ge 0$ and $s^2 = 0 = a$ , so existence holds; assume henceforth $a > 0$ .

givenalgebra

1.2

Uniqueness holds once a root exists: if $u, v \ge 0$ satisfy $u^2 = v^2$ , then strict monotonicity of squaring on nonnegatives [L3] rules out both $u < v$ and $u > v$ , forcing $u = v$ ; so at most one $s \ge 0$ has $s^2 = a$ .

L3given

1.3

Define $S = \{ t \in F : t \ge 0 \text{ and } t^2 \le a \}$ ; then $0 \in S$ because $0 \ge 0$ and $0^2 = 0 \le a$ , so $S \neq \emptyset$ .

givenalgebra

1.4

The element $1 + a$ is an upper bound of $S$ : since $a > 0$ we have $1 + a > 1$ , so any $t > 1 + a$ has $t > 1$ and $t > 0$ , whence $t^2 = t \cdot t > 1 \cdot t = t > 1 + a > a$ , giving $t \notin S$ .

givenL2

2.1

By completeness [L1], $s := \sup S$ exists in $F$ ; and since $0 \in S$ we have $s \ge 0$ .

L1step 1.3step 1.4

3.1

Assume, for contradiction, that $s^2 \neq a$ ; by trichotomy either $s^2 < a$ or $s^2 > a$ .

assume-contrastep 2.1

4.1

(Case $s^2 < a$ .) Choose $h$ with $0 < h < 1$ and $h < \dfrac{a - s^2}{2s + 1}$ , possible since $a - s^2 > 0$ and $2s + 1 \ge 1 > 0$ ; then $h^2 = h \cdot h < h \cdot 1 = h$ and $h(2s+1) < a - s^2$ , so $(s+h)^2 = s^2 + 2sh + h^2 < s^2 + 2sh + h = s^2 + h(2s+1) < a$ , whence $s + h \in S$ with $s + h > s$ , contradicting that $s$ is an upper bound of $S$ .

assume-case lowstep 3.1step 2.1L2L5choose

4.2

(Case $s^2 > a$ .) Here $s > 0$ since $s^2 > a \ge 0$ ; choose $h$ with $0 < h < s$ and $h < \dfrac{s^2 - a}{2s}$ , so $2sh < s^2 - a$ and $(s-h)^2 = s^2 - 2sh + h^2 \ge s^2 - 2sh > a$ , hence every $t \in S$ has $t^2 \le a < (s-h)^2$ with $t \ge 0$ and $s - h > 0$ , so $t < s - h$ by [L3]; thus $s - h$ is an upper bound of $S$ with $s - h < s$ , contradicting that $s$ is the least upper bound.

assume-case highstep 3.1step 2.1L3choose

5.1

Both cases of the disjunction in step 3.1 give a contradiction, so the assumption fails and $s^2 = a$ : a unique (by step 1.2) $s = \sqrt{a} \ge 0$ with $s^2 = a$ exists, and applying this to any $x > 0$ writes $x = (\sqrt{x})^2$ with $\sqrt{x} \neq 0$ while conversely any nonzero square is positive by [L4], so the positive elements of $F$ are exactly the nonzero squares.

step 4.1step 4.2step 3.1step 1.2L4casesdischarge-contradiction∎

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Field homomorphisms between ordered fields fix $\mathbb{Q}$

Statement

Let $F$ and $G$ be ordered fields with canonical rational embeddings $\iota_F : \mathbb{Q} \to F$ and $\iota_G : \mathbb{Q} \to G$ (The unique embedding of ℚ into an ordered field). Then every field homomorphism $\varphi : F \to G$ (Field homomorphism and embedding) fixes $\mathbb{Q}$ , meaning $\varphi \circ \iota_F = \iota_G, \qquad \text{i.e. } \varphi(\iota_F(q)) = \iota_G(q) \text{ for all } q \in \mathbb{Q}.$

Facts & Assumptions

Given: Ordered fields $F, G$ , a field homomorphism $\varphi : F \to G$ , and the canonical embeddings $\iota_F, \iota_G$ .

[L1]

The canonical embedding $\iota : \mathbb{Q} \to F$ acts on $\mathbb{Z}$ by $n \mapsto n \cdot 1_F$ and on $\mathbb{Q}$ by $p/q \mapsto (p \cdot 1_F)(q \cdot 1_F)^{-1}$ (likewise for $\iota_G$ ) (The unique embedding of ℚ into an ordered field).

[L2]

The canonical natural $n \cdot 1$ is the $n$ -fold sum $1 + \dots + 1$ ; the integers embed with $q \cdot 1 \ne 0$ for $q \ne 0$ (Canonical naturals are positive and strictly increasing).

[L3]

$\varphi$ is a field homomorphism: $\varphi(1_F) = 1_G$ , $\varphi(x + y) = \varphi(x) + \varphi(y)$ , $\varphi(xy) = \varphi(x)\varphi(y)$ , $\varphi(0_F) = 0_G$ , $\varphi(-x) = -\varphi(x)$ , and $\varphi(x^{-1}) = \varphi(x)^{-1}$ for $x \ne 0$ (Field homomorphism and embedding).

Proof

technique · direct

1.1

By [L3], $\varphi(1_F) = 1_G$ and $\varphi$ preserves sums, products, negation, and inversion of nonzero elements.

1.2

By [L1], $\iota_F$ and $\iota_G$ send each $n \in \mathbb{Z}$ to $n \cdot 1_F$ and $n \cdot 1_G$ , and each $p/q \in \mathbb{Q}$ to $(p \cdot 1)(q \cdot 1)^{-1}$ in the respective field.

1.3

Because $n \cdot 1_F$ is the $n$ -fold sum of $1_F$ ([L2]) and $\varphi$ is additive with $\varphi(1_F) = 1_G$ , we get $\varphi(n \cdot 1_F) = n \cdot 1_G$ for every canonical natural $n$ .

L2L3

2.1

For each integer $n$ this extends by sign: $\varphi(\iota_F(0)) = \varphi(0_F) = 0_G = \iota_G(0)$ and $\varphi(\iota_F(-n)) = \varphi(-(n \cdot 1_F)) = -(n \cdot 1_G) = \iota_G(-n)$ , so $\varphi(\iota_F(m)) = \iota_G(m)$ for all $m \in \mathbb{Z}$ .

step 1.2step 1.3L3

3.1

For a rational $p/q$ with integers $p, q \ne 0$ , $\iota_F(p/q) = (p \cdot 1_F)(q \cdot 1_F)^{-1}$ , so $\varphi(\iota_F(p/q)) = \varphi(p \cdot 1_F)\,\varphi(q \cdot 1_F)^{-1} = (p \cdot 1_G)(q \cdot 1_G)^{-1} = \iota_G(p/q)$ .

step 1.2step 2.1L3

4.1

Since $\varphi \circ \iota_F$ and $\iota_G$ agree on every rational, $\varphi \circ \iota_F = \iota_G$ : the homomorphism $\varphi$ fixes $\mathbb{Q}$ .

step 3.1∎

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Homomorphisms out of a complete ordered field are order-preserving

Statement

Let $F$ be a complete ordered field and $G$ an ordered field, and let $\varphi : F \to G$ be a field homomorphism (Field homomorphism and embedding). Then $\varphi$ is injective and order-preserving: $x > 0$ in $F$ implies $\varphi(x) > 0$ in $G$ , and consequently $a < b$ implies $\varphi(a) < \varphi(b)$ .

Facts & Assumptions

Given: A complete ordered field $F$ , an ordered field $G$ , and a field homomorphism $\varphi : F \to G$ .

[L1]

$\varphi(1_F) = 1_G$ , $\varphi(x + y) = \varphi(x) + \varphi(y)$ , $\varphi(xy) = \varphi(x)\varphi(y)$ , $\varphi(-x) = -\varphi(x)$ ; and every field homomorphism is injective, its kernel being an ideal of the field $F$ with $\varphi(1_F) = 1_G \ne 0_G$ (Field homomorphism and embedding).

[L2]

In a complete ordered field every $a \ge 0$ is a square $a = y^2$ ; the positive elements are exactly the nonzero squares (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ ).

[L3]

In any ordered field a nonzero square is positive: $y \ne 0 \Rightarrow y^2 > 0$ (Squares of nonzero elements are positive).

[L4]

Order via the positive cone: $x > 0$ means $x \in P$ , $a < b$ means $b - a \in P$ ; trichotomy holds (Ordered field).

Proof

technique · direct

1.1

$\varphi$ is injective: by [L1] its kernel is an ideal of the field $F$ , and since $\varphi(1_F) = 1_G \ne 0_G$ the kernel is $\{0_F\}$ .

1.2

Fix $x \in F$ with $x > 0$ ; then $x \ge 0$ , so by [L2] there is $y \in F$ with $x = y^2$ , and $y \ne 0$ since $y = 0$ would give $x = 0$ , against $x > 0$ by [L4].

L2L4

2.1

Applying $\varphi$ , $\varphi(x) = \varphi(y^2) = \varphi(y)^2$ , and $\varphi(y) \ne 0_G$ because $y \ne 0$ and $\varphi$ is injective.

step 1.1step 1.2L1

3.1

By [L3] in $G$ , the nonzero square $\varphi(y)^2$ is positive, so $\varphi(x) = \varphi(y)^2 > 0$ ; as $x > 0$ was arbitrary, $x > 0 \Rightarrow \varphi(x) > 0$ for all $x \in F$ .

step 2.1L3

4.1

If $a < b$ then $b - a > 0$ , so $\varphi(b - a) > 0$ ; since $\varphi(b - a) = \varphi(b) - \varphi(a)$ by [L1], we get $\varphi(b) - \varphi(a) > 0$ , i.e. $\varphi(a) < \varphi(b)$ .

step 3.1L1L4

5.1

Hence $\varphi$ is an injective, order-preserving field homomorphism.

step 1.1step 4.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-25Open item page →

Uniqueness of the complete ordered field: $\mathbb{R}$ up to a unique isomorphism

Statement

Any two complete ordered fields $F$ and $G$ (Complete ordered field (least-upper-bound property)) are isomorphic via a unique ordered-field isomorphism (Ordered-field isomorphism) $\varphi : F \to G$ , and this $\varphi$ fixes $\mathbb{Q}$ ( $\varphi \circ \iota_F = \iota_G$ ). Consequently $\mathbb{R}$ is the unique complete ordered field up to a unique isomorphism, and it admits $\mathbb{Q}$ as an ordered subfield via $\iota_F$ .

Facts & Assumptions

Given: Complete ordered fields $F, G$ with canonical embeddings $\iota_F : \mathbb{Q} \to F$ , $\iota_G : \mathbb{Q} \to G$ ; for $x \in F$ set $L_x := \{\iota_G(q) : q \in \mathbb{Q},\ \iota_F(q) < x\} \subseteq G$ and define $\varphi : F \to G$ by $\varphi(x) := \sup L_x$ , and symmetrically $\psi : G \to F$ by $\psi(y) := \sup\{\iota_F(q) : q \in \mathbb{Q},\ \iota_G(q) < y\}$ .

[L1]

Every complete ordered field is Archimedean (Every complete ordered field is Archimedean).

[L2]

The canonical embedding $\iota : \mathbb{Q} \to F$ is a field homomorphism that is injective and order-preserving in both directions ( $q < r \iff \iota(q) < \iota(r)$ ); likewise $\iota_G$ (The unique embedding of ℚ into an ordered field).

[L3]

Density: in an Archimedean ordered field, for $u < v$ there is $q \in \mathbb{Q}$ with $u < \iota(q) < v$ (ℚ is dense in every Archimedean ordered field).

[L4]

Any field homomorphism between ordered fields fixes $\mathbb{Q}$ (Field homomorphisms between ordered fields fix $\mathbb{Q}$ ).

[L5]

A field homomorphism from a complete ordered field into an ordered field is injective and order-preserving, hence (the domain being totally ordered) order-preserving in both directions (Homomorphisms out of a complete ordered field are order-preserving).

[L6]

Completeness: every nonempty subset of $F$ (resp. $G$ ) bounded above has a least upper bound (Complete ordered field (least-upper-bound property)).

[L7]

An ordered-field isomorphism is a bijective field homomorphism order-preserving in both directions; a field homomorphism preserves $+$ , $\cdot$ , and $1$ (Ordered-field isomorphism, Field homomorphism and embedding).

[L8]

Least-upper-bound calculus in $G$ : for nonempty $T \subseteq G$ bounded above with $u = \sup T$ , any upper bound $w$ of $T$ satisfies $w \ge u$ ; and translation $z \mapsto z + c$ and, for $c > 0$ , scaling $z \mapsto cz$ preserve $\le$ as well as $<$ . Order is preserved by adding a constant and by adding inequalities (claim 1) and Sign rules for products and monotonicity of multiplication (claim 4) state the STRICT forms and only those, $z < z' \Rightarrow z + c < z' + c$ and, for $c > 0$ , $z < z' \iff cz < cz'$ ; the nonstrict forms used here are those together with the equality cases, in which $z + c = z' + c$ and $cz = cz'$ , the order being total by trichotomy (Ordered field). Hence from $\,\alpha \ge \iota_G(q) + c$ for all $q$ with $\iota_F(q) < x$ one gets $\alpha \ge \varphi(x) + c$ , and from $\,\alpha \ge \iota_G(q)\,c$ (with $c > 0$ ) for all such $q$ with $q > 0$ one gets $\alpha \ge \varphi(x)\,c$ (using that the positive rationals below $x$ are cofinal when $x > 0$ ).

Proof

technique · direct

1.1

For each $x \in F$ , applying [L3] (with $F$ Archimedean by [L1]) to $x - 1 < x$ and to $x < x + 1$ gives rationals $a, b$ with $\iota_F(a) < x < \iota_F(b)$ ; then $\iota_G(a) \in L_x$ , and every $\iota_G(q) \in L_x$ has $\iota_F(q) < \iota_F(b)$ so $q < b$ hence $\iota_G(q) < \iota_G(b)$ , so $L_x$ is nonempty and bounded above and $\varphi(x) = \sup L_x$ exists in $G$ by [L6].

L1L2L3L6

1.2

If $x > 0$ , then applying [L3] to $0 < x$ gives a rational $q$ with $0 < \iota_F(q) < x$ , whence $q > 0$ , $\iota_G(q) > 0$ , and $\iota_G(q) \in L_x$ , so $\varphi(x) = \sup L_x \ge \iota_G(q) > 0$ .

L2L3

1.3

For $r \in \mathbb{Q}$ , $L_{\iota_F(r)} = \{\iota_G(q) : q < r\}$ by [L2]; $\iota_G(r)$ is an upper bound, and any $w < \iota_G(r)$ is exceeded by some $\iota_G(q') \in L_{\iota_F(r)}$ via density [L3] in $G$ , so $\sup = \iota_G(r)$ , i.e. $\varphi(\iota_F(r)) = \iota_G(r)$ .

L2L3

2.1

For rationals $q, q'$ with $\iota_F(q) < x$ and $\iota_F(q') < x'$ , additivity of $\iota_F$ gives $\iota_F(q + q') < x + x'$ , so $\iota_G(q) + \iota_G(q') = \iota_G(q + q') \in L_{x + x'}$ and $\varphi(x + x') \ge \iota_G(q) + \iota_G(q')$ ; fixing $q'$ and taking the sup over $q$ , then over $q'$ , yields $\varphi(x + x') \ge \varphi(x) + \varphi(x')$ by the least-upper-bound calculus [L8].

step 1.1L2L3L8

2.2

For any rational $s$ with $\iota_F(s) < x + x'$ we have $\iota_F(s) - x' < x$ ; density [L3] gives a rational $q$ with $\iota_F(s) - x' < \iota_F(q) < x$ , so $\iota_F(q) < x$ , and the left inequality gives $\iota_F(s) - \iota_F(q) < x'$ , i.e. $\iota_F(s - q) = \iota_F(s) - \iota_F(q) < x'$ by additivity of $\iota_F$ ; whence $\iota_G(s) = \iota_G(q) + \iota_G(s - q) \le \varphi(x) + \varphi(x')$ ; as $s$ was arbitrary and $\varphi(x + x') = \sup L_{x + x'}$ , the least upper bound is $\le \varphi(x) + \varphi(x')$ [L8], i.e. $\varphi(x + x') \le \varphi(x) + \varphi(x')$ .

step 1.1L2L3L8

2.3

For $x, x' > 0$ and positive rationals $q, q'$ with $\iota_F(q) < x$ , $\iota_F(q') < x'$ , multiplying positives gives $\iota_F(qq') < xx'$ , so $\iota_G(q)\iota_G(q') = \iota_G(qq') \in L_{xx'}$ and $\varphi(xx') \ge \iota_G(q)\iota_G(q')$ ; since positive rationals below $x$ are cofinal (as $x > 0$ ) their images have supremum $\varphi(x) > 0$ , so scaling by $\iota_G(q') > 0$ and taking sups over $q$ then $q'$ gives $\varphi(xx') \ge \varphi(x)\varphi(x')$ by the least-upper-bound calculus [L8].

step 1.1step 1.2L2L3L8algebra

2.4

For $x, x' > 0$ and any positive rational $s$ with $\iota_F(s) < xx'$ we have $\iota_F(s)(x')^{-1} < x$ ; density [L3] gives a rational $q$ with $\iota_F(s)(x')^{-1} < \iota_F(q) < x$ , where $\iota_F(s)(x')^{-1} > 0$ (as $s > 0$ , $x' > 0$ ), so $\iota_F(q) > 0$ and $q > 0$ ; the left inequality gives $\iota_F(s) < \iota_F(q)\,x'$ , hence $\iota_F(s/q) = \iota_F(s)\iota_F(q)^{-1} < x'$ (dividing by $\iota_F(q) > 0$ ), while $\iota_F(q) < x$ ; therefore $\iota_G(s) = \iota_G(q)\iota_G(s/q) \le \varphi(x)\varphi(x')$ , and as the positive rationals $s$ with $\iota_F(s) < xx'$ are cofinal, $\varphi(xx') = \sup L_{xx'} \le \varphi(x)\varphi(x')$ by [L8].

step 1.1step 1.2L2L3L8algebra

3.1

Combining the two inequalities, $\varphi(x + x') = \varphi(x) + \varphi(x')$ for all $x, x' \in F$ ; in particular $\varphi(0_F) = 0_G$ and $\varphi(-x) = -\varphi(x)$ .

step 2.1step 2.2

3.2

Combining the two inequalities, $\varphi(xx') = \varphi(x)\varphi(x')$ whenever $x, x' > 0$ .

step 2.3step 2.4

4.1

For arbitrary signs, $\varphi(0_F \cdot x') = 0_G = 0_G \cdot \varphi(x')$ , and for $x < 0 < x'$ we get $\varphi(xx') = \varphi(-((-x)x')) = -\varphi((-x)x') = -\varphi(-x)\varphi(x') = \varphi(x)\varphi(x')$ using step 3.1 and step 3.2; the remaining sign cases are identical, so $\varphi(xx') = \varphi(x)\varphi(x')$ for all $x, x' \in F$ .

step 3.1step 3.2

5.1

By step 3.1, step 4.1, and $\varphi(1_F) = \iota_G(1) = 1_G$ from step 1.3, $\varphi$ preserves $+$ , $\cdot$ , and $1$ , so $\varphi$ is a field homomorphism $F \to G$ .

step 1.3step 3.1step 4.1

6.1

Hence by [L5] (as $F$ is complete) $\varphi$ is injective and order-preserving in both directions, and by [L4] it fixes $\mathbb{Q}$ : $\varphi \circ \iota_F = \iota_G$ .

step 5.1L4L5

7.1

The construction and steps 1.1-6.1 used only that $F$ and $G$ are complete ordered fields with canonical embeddings $\iota_F, \iota_G$ ; applying that entire argument verbatim with the roles of $F$ and $G$ interchanged shows the symmetric map $\psi : G \to F$ is likewise an injective, order-preserving field homomorphism that fixes $\mathbb{Q}$ .

step 6.1

8.1

For $x \in F$ , since $\varphi$ fixes $\mathbb{Q}$ and is order-preserving in both directions, $\iota_G(q) < \varphi(x) \iff \iota_F(q) < x$ , so $\psi(\varphi(x)) = \sup\{\iota_F(q) : \iota_F(q) < x\} = x$ by density [L3]; symmetrically $\varphi(\psi(y)) = y$ , so $\varphi$ is a bijection with inverse $\psi$ .

step 6.1step 7.1L3

9.1

Thus $\varphi$ is a bijective field homomorphism order-preserving in both directions, i.e. an ordered-field isomorphism $F \cong G$ fixing $\mathbb{Q}$ .

step 6.1step 8.1L7

10.1

For uniqueness let $\chi : F \to G$ be any ordered-field isomorphism; being such it is in particular a field homomorphism ([L7]), so by [L4] it fixes $\mathbb{Q}$ , and it is order-preserving, so for each $x$ every $\iota_G(q) \in L_x$ equals $\chi(\iota_F(q)) < \chi(x)$ , making $\chi(x)$ an upper bound of $L_x$ , hence $\chi(x) \ge \varphi(x)$ .

step 9.1L4L7

11.1

Conversely, were $\chi(x) > \varphi(x)$ , density [L3] would give a rational $q$ with $\varphi(x) < \iota_G(q) < \chi(x)$ ; then $\iota_G(q) > \sup L_x$ forces $\iota_F(q) \ge x$ , since $\iota_F(q) < x$ would put $\iota_G(q)$ into $L_x$ and hence below $\sup L_x$ ; so $\chi(x) \le \chi(\iota_F(q)) = \iota_G(q) < \chi(x)$ , which is impossible, hence $\chi(x) \le \varphi(x)$ .

step 10.1L3L4

12.1

Therefore $\chi(x) = \varphi(x)$ for every $x$ , so $\chi = \varphi$ : the ordered-field isomorphism is unique.

step 10.1step 11.1

13.1

Applying this to any two constructions of $\mathbb{R}$ , which are complete ordered fields, $\mathbb{R}$ is the unique complete ordered field up to a unique ordered-field isomorphism, and $\iota_F : \mathbb{Q} \to \mathbb{R}$ exhibits $\mathbb{Q}$ as an ordered subfield.

step 9.1step 12.1L2∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

The Cauchy-sequence reals are Archimedean

Statement

The Cauchy-sequence reals $\mathbb{R}_C$ (The reals form a totally ordered field) are Archimedean (Archimedean ordered field): for every $x \in \mathbb{R}_C$ there is a natural number $n$ with $x < n \cdot 1$ , where the canonical natural $n \cdot 1$ is the class $\hat n$ of the constant rational sequence $n$ . Equivalently, the canonical naturals $(\hat n)_{n \ge 1}$ are cofinal.

Facts & Assumptions

Given: A real $x \in \mathbb{R}_C$ .

[L1]

Rational approximation: for any real $z$ and rational $\varepsilon > 0$ there is $q \in \mathbb{Q}$ with $|z - \hat q| < \hat\varepsilon$ , and the embedding $q \mapsto \hat q$ preserves and reflects order and arithmetic (The rationals embed densely in the reals).

[L2]

The rationals are Archimedean: for every rational $y$ there is a natural $n$ with $y < n$ (The rationals are Archimedean).

[L3]

$\mathbb{R}_C$ is a totally ordered field, and $\hat q + \hat r = \widehat{q + r}$ , $\hat 1 = 1$ (The reals form a totally ordered field, Order on the reals).

[L4]

$\mathbb{R}_C$ is Archimedean iff for every real there is a natural $n$ with the real below the canonical natural $n \cdot 1 = \hat n$ (Archimedean ordered field).

Proof

technique · direct

1.1

By [L1] with $\varepsilon = 1$ choose a rational $q$ with $|x - \hat q| < \hat 1$ .

L1choose

1.2

By [L2] applied to the rational $q + 1$ choose a natural $n$ with $q + 1 < n$ .

L2choose

2.1

From step 1.1, $x - \hat q < \hat 1$ , so $x < \hat q + \hat 1 = \widehat{q + 1}$ .

step 1.1L3

2.2

From step 1.2, since the embedding preserves order, $\widehat{q + 1} < \hat n = n \cdot 1$ .

step 1.2L1L3L4

3.1

Combining, $x < \widehat{q + 1} < n \cdot 1$ , so $x < n \cdot 1$ for this canonical natural.

step 2.1step 2.2L3

4.1

As $x \in \mathbb{R}_C$ was arbitrary, every real lies below some canonical natural: $\mathbb{R}_C$ is Archimedean.

step 3.1L4∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The Cauchy-sequence reals have the least-upper-bound property

Statement

The Cauchy-sequence reals $\mathbb{R}_C$ have the least-upper-bound property: every nonempty $S \subseteq \mathbb{R}_C$ that is bounded above has a least upper bound $\sup S \in \mathbb{R}_C$ . Hence, together with The reals form a totally ordered field, $\mathbb{R}_C$ is a complete ordered field (Complete ordered field (least-upper-bound property)).

Facts & Assumptions

Given: A nonempty set $S \subseteq \mathbb{R}_C$ bounded above by $U \in \mathbb{R}_C$ .

[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 $\varepsilon$ (Limits and Cauchy sequences of reals).

[L4]

$\mathbb{R}_C$ is Archimedean, so the reals $2^k$ are cofinal and $(b_0 - a_0)/2^k \to 0$ (The Cauchy-sequence reals are Archimedean).

[L5]

$\mathbb{R}_C$ 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 $s_0 \in S$ (possible as $S \ne \emptyset$ ); by [L6] choose a real $a_0 < s_0$ , so $a_0$ is not an upper bound of $S$ , and put $b_0 = U$ , an upper bound of $S$ .

givenL6L5L1

2.1

Define $(a_k), (b_k)$ by bisection: given $a_k$ (not an upper bound) and $b_k$ (an upper bound), let $m = (a_k + b_k)/2$ ; if $m$ is an upper bound set $a_{k+1} = a_k, b_{k+1} = m$ , otherwise set $a_{k+1} = m, b_{k+1} = b_k$ .

step 1.1L5

3.1

An induction on $k$ shows each $b_k$ is an upper bound of $S$ , each $a_k$ is not, $a_k \le a_{k+1} \le b_{k+1} \le b_k$ , and $b_k - a_k = (b_0 - a_0)/2^k$ .

step 2.1L5L1

4.1

Given rational $\varepsilon > 0$ , by [L4] choose $k$ with $(b_0 - a_0) < 2^k \hat\varepsilon$ ; then for all $j \ge k$ , $b_j - a_j = (b_0 - a_0)/2^j \le (b_0 - a_0)/2^k < \hat\varepsilon$ .

step 3.1L4L5

5.1

For $j, l \ge k$ both $a_j, a_l, b_j, b_l$ lie in the nested interval $[a_k, b_k]$ , so $|a_j - a_l| \le b_k - a_k < \hat\varepsilon$ and likewise $|b_j - b_l| < \hat\varepsilon$ ; hence $(a_k)$ and $(b_k)$ are Cauchy sequences of reals.

step 3.1step 4.1L3L5

6.1

By [L2], $(a_k)$ converges to a real $s$ and $(b_k)$ to a real $s'$ . If $s < s'$ , choose by [L6] a positive rational $\varepsilon$ with $3\hat\varepsilon < s'-s$ . For all large $k$ , convergence and step 4.1 give $|a_k-s| < \hat\varepsilon$ , $|b_k-s'| < \hat\varepsilon$ and $b_k-a_k < \hat\varepsilon$ , whence $s'-s \le |s'-b_k|+(b_k-a_k)+|a_k-s| < 3\hat\varepsilon$ , a contradiction. If $s' < s$ , choose $2\hat\varepsilon < s-s'$ ; for all large $k$ , $a_k \le b_k$ and the two convergence bounds give $s-s' \le |s-a_k|+(a_k-b_k)+|b_k-s'| < 2\hat\varepsilon$ , again a contradiction. Thus $s=s'$ . For fixed $k$ and every $j \ge k$ , step 3.1 gives $a_k \le a_j \le b_j \le b_k$ . If $s<a_k$ , choose $0<\hat\varepsilon<a_k-s$ and use $a_j\to s$ ; if $b_k<s$ , choose $0<\hat\varepsilon<s-b_k$ and use $b_j\to s$ . Each choice contradicts the displayed inequalities for all large $j$ , so $a_k \le s \le b_k$ .

step 3.1step 4.1step 5.1L2L3L5L6algebra

7.1

Every $t \in S$ satisfies $t \le b_k$ for all $k$ , since each $b_k$ is an upper bound. If $s<t$ , choose by [L6] a positive rational $\varepsilon$ with $\hat\varepsilon<t-s$ . Since $b_k\to s$ , eventually $|b_k-s|<\hat\varepsilon$ , hence $b_k<s+\hat\varepsilon<t$ , contradicting $t\le b_k$ . Therefore $t\le 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 $a_k$ , because $a_k$ is not an upper bound; hence $a_k<v$ . If $v<s$ , choose by [L6] a positive rational $\varepsilon$ with $\hat\varepsilon<s-v$ . Since $a_k\to s$ , eventually $|a_k-s|<\hat\varepsilon$ , so $a_k>s-\hat\varepsilon>v$ , a contradiction. Thus $s\le v$ , and $s$ is the least upper bound.

step 3.1step 6.1L1L3L5L6

8.1

Hence $s = \sup S$ exists in $\mathbb{R}_C$ ; as $S$ was an arbitrary nonempty bounded-above set, $\mathbb{R}_C$ has the least-upper-bound property and is a complete ordered field.

step 7.1step 7.2L1∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Equivalence of the Cauchy and Dedekind constructions of $\mathbb{R}$

Statement

The Cauchy-sequence reals $\mathbb{R}_C$ and the Dedekind-cut reals $\mathbb{R}_D$ are isomorphic as ordered fields via a unique isomorphism $\varphi : \mathbb{R}_C \to \mathbb{R}_D$ that preserves all arithmetic ( $+$ , $\cdot$ , $0$ , $1$ , inverses) and the order ( $<$ , hence $\le$ , $|\cdot|$ , and suprema), and restricts to the identity on the common rationals $\mathbb{Q}$ . This is the precise sense in which the two constructions build the same $\mathbb{R}$ .

Facts & Assumptions

Given: The Cauchy-sequence reals $\mathbb{R}_C$ and the Dedekind-cut reals $\mathbb{R}_D$ .

[L1]

$\mathbb{R}_C$ is a totally ordered field (The reals form a totally ordered field).

[L2]

$\mathbb{R}_C$ has the least-upper-bound property, hence is complete (The Cauchy-sequence reals have the least-upper-bound property, Complete ordered field (least-upper-bound property)).

[L3]

$\mathbb{R}_D$ is a totally ordered field (The Dedekind reals form a totally ordered field).

[L4]

$\mathbb{R}_D$ has the least-upper-bound property, hence is complete (Dedekind completeness: the least-upper-bound property, Complete ordered field (least-upper-bound property)).

[L5]

Any two complete ordered fields are isomorphic via a unique ordered-field isomorphism, which fixes $\mathbb{Q}$ (Uniqueness of the complete ordered field: $\mathbb{R}$ up to a unique isomorphism).

Proof

technique · direct

1.1

$\mathbb{R}_C$ is a complete ordered field: a totally ordered field ([L1]) with the least-upper-bound property ([L2]).

L1L2

1.2

$\mathbb{R}_D$ is a complete ordered field: a totally ordered field ([L3]) with the least-upper-bound property ([L4]).

L3L4

2.1

By [L5] applied to $F = \mathbb{R}_C$ and $G = \mathbb{R}_D$ there is a unique ordered-field isomorphism $\varphi : \mathbb{R}_C \to \mathbb{R}_D$ , and it fixes the common rationals $\mathbb{Q}$ .

step 1.1step 1.2L5

3.1

As a field isomorphism $\varphi$ preserves $+$ , $\cdot$ , $0$ , $1$ and inverses; as an ordered-field isomorphism it satisfies $x < y \iff \varphi x < \varphi y$ , hence preserves $\le$ and $|\cdot|$ ; and it preserves suprema, in the sense that for any nonempty $S \subseteq \mathbb{R}_C$ bounded above with $s = \sup S$ , its image $\varphi[S] = \{\varphi(t) : t \in S\}$ has $\varphi(s) = \sup \varphi[S]$ , since $\varphi(s)$ is an upper bound of $\varphi[S]$ and, $\varphi^{-1}$ being order-preserving, every upper bound of $\varphi[S]$ is $\ge \varphi(s)$ .

step 2.1L5

4.1

Therefore $\mathbb{R}_C$ and $\mathbb{R}_D$ are the same complete ordered field presented two ways, joined by the unique isomorphism $\varphi$ that restricts to the identity on $\mathbb{Q}$ and preserves all arithmetic and order: the Cauchy and Dedekind constructions give the same $\mathbb{R}$ .

step 2.1step 3.1L5∎

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

$\sqrt{2}$ exists in every complete ordered field, and is irrational

Example

In any complete ordered field $F$ , the element $2 = 1 + 1$ is positive, so by Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ applied to $a = 2$ it has a unique $s > 0$ with $s^2 = 2$ : this is $\sqrt{2}$ . Moreover $s$ is not the image of any rational under the embedding $\iota : \mathbb{Q} \to F$ , because no rational squares to $2$ . Thus every complete ordered field contains $\sqrt{2}$ , the canonical gap that $\mathbb{Q}$ lacks, now filled by completeness.

Facts & Assumptions

Given: A complete ordered field $F$ (Complete ordered field (least-upper-bound property)) with unit $1$ ; write $2 := 1 + 1$ . In any ordered field $1 > 0$ , hence $2 = 1 + 1 > 0$ .

[L1]

Every $a \ge 0$ in $F$ has a unique $s \ge 0$ with $s^2 = a$ (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ ).

[L2]

There is a unique field homomorphism $\iota : \mathbb{Q} \to F$ ; it is injective and order-preserving, and satisfies $\iota(1) = 1$ (The unique embedding of ℚ into an ordered field).

[L3]

No rational number squares to $2$ (FALSE: some rational number squares to 2).

Verification

technique · direct

1.1

In $F$ we have $2 = 1 + 1 > 0$ , so in particular $2 \ge 0$ .

given

2.1

Apply Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ [L1] with $a = 2$ : there is a unique $s \ge 0$ with $s^2 = 2$ , and $s \neq 0$ since $s^2 = 2 > 0$ , so $s > 0$ ; write $\sqrt{2} := s$ .

L1step 1.1

3.1

The element $s$ is not rational: if $s = \iota(q)$ for some $q \in \mathbb{Q}$ , then $\iota(q^2) = \iota(q)^2 = s^2 = 2 = \iota(1) + \iota(1) = \iota(2)$ , so injectivity of $\iota$ [L2] forces $q^2 = 2$ , which is impossible by [L3]; hence $s$ lies outside $\iota(\mathbb{Q})$ .

L2L3step 2.1

4.1

Therefore every complete ordered field contains a unique positive $s = \sqrt{2}$ with $s^2 = 2$ , and this $s$ is irrational: it is exactly the gap in $\mathbb{Q}$ that completeness fills.

step 2.1step 3.1∎

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

A field homomorphism of ordered fields need not preserve order

Statement refuted

Refuted claim: every field homomorphism $\varphi : F \to G$ between ordered fields is order-preserving, that is, $a < b$ in $F$ implies $\varphi(a) < \varphi(b)$ in $G$ .

The witness is the conjugation map on $\mathbb{Q}(\sqrt{2}) = \{a + b\sqrt{2} : a, b \in \mathbb{Q}\} \subseteq \mathbb{R}$ , which is a field homomorphism from an ordered field to itself yet sends the positive element $\sqrt{2}$ to the negative element $-\sqrt{2}$ .

Facts & Assumptions

Given: The reals $\mathbb{R}$ , a complete ordered field, with the positive square root $\sqrt{2}$ of $2$ .

[L1]

In $\mathbb{R}$ the element $2 = 1 + 1$ has a positive square root $\sqrt{2}$ with $(\sqrt{2})^2 = 2$ and $\sqrt{2} > 0$ (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ ).

[L2]

No rational number squares to $2$ , so $\sqrt{2}$ is irrational (FALSE: some rational number squares to 2).

[L3]

A field homomorphism $\varphi$ satisfies $\varphi(x + y) = \varphi(x) + \varphi(y)$ , $\varphi(xy) = \varphi(x)\varphi(y)$ , and $\varphi(1) = 1$ (Field homomorphism and embedding).

[L4]

In an ordered field, $x > 0$ means $x$ lies in the positive cone, and $a < b$ means $b - a > 0$ ; exactly one of $x > 0$ , $x = 0$ , $x < 0$ holds (Ordered field).

[L5]

A field homomorphism from a complete ordered field into an ordered field is order-preserving (Homomorphisms out of a complete ordered field are order-preserving).

Counterexample

technique · direct

1.1

Working inside $\mathbb{R}$ , let $K = \{a + b\sqrt{2} : a, b \in \mathbb{Q}\}$ ; then $(a + b\sqrt{2}) + (c + d\sqrt{2}) = (a + c) + (b + d)\sqrt{2}$ and $(a + b\sqrt{2})(c + d\sqrt{2}) = (ac + 2bd) + (ad + bc)\sqrt{2}$ both lie in $K$ , so $K$ is closed under addition and multiplication.

L1algebra

1.2

Each nonzero $a + b\sqrt{2} \in K$ is invertible in $K$ , with $(a + b\sqrt{2})^{-1} = \frac{a - b\sqrt{2}}{a^2 - 2b^2}$ , where $a^2 - 2b^2 \ne 0$ since otherwise $(a, b) \ne (0, 0)$ forces $b \ne 0$ and the rational $(a/b)^2 = 2$ , contradicting [L2].

L2algebra

1.3

The representation of an element of $K$ as $a + b\sqrt{2}$ with $a, b \in \mathbb{Q}$ is unique, for $a + b\sqrt{2} = a' + b'\sqrt{2}$ with $b \ne b'$ would give $\sqrt{2} = (a' - a)/(b - b') \in \mathbb{Q}$ .

L2algebra

1.4

In $K$ the element $\sqrt{2} = 0 + 1 \cdot \sqrt{2}$ satisfies $\sqrt{2} > 0$ .

L1L4

2.1

By steps 1.1 and 1.2, $K$ is a subfield of $\mathbb{R}$ , hence an ordered field under the positive cone inherited from $\mathbb{R}$ .

step 1.1step 1.2L4

2.2

By the uniqueness in step 1.3, the map $\sigma : K \to K$ given by $\sigma(a + b\sqrt{2}) = a - b\sqrt{2}$ is well defined.

step 1.3

2.3

The real number $2^{1/4} = \sqrt{\sqrt{2}}$ is not in $K$ , for $2^{1/4} = a + b\sqrt{2}$ would square to $\sqrt{2} = (a^2 + 2b^2) + 2ab\sqrt{2}$ , whence step 1.3 forces $a^2 + 2b^2 = 0$ and $2ab = 1$ , impossible for real $a, b$ .

step 1.3algebra

3.1

$\sigma$ is additive: $\sigma((a + b\sqrt{2}) + (c + d\sqrt{2})) = (a + c) - (b + d)\sqrt{2} = (a - b\sqrt{2}) + (c - d\sqrt{2}) = \sigma(a + b\sqrt{2}) + \sigma(c + d\sqrt{2})$ .

step 2.2algebra

3.2

$\sigma$ is multiplicative: $\sigma((a + b\sqrt{2})(c + d\sqrt{2})) = (ac + 2bd) - (ad + bc)\sqrt{2} = (a - b\sqrt{2})(c - d\sqrt{2}) = \sigma(a + b\sqrt{2})\,\sigma(c + d\sqrt{2})$ .

step 2.2algebra

3.3

$\sigma$ fixes the identity: $\sigma(1) = \sigma(1 + 0 \cdot \sqrt{2}) = 1$ .

step 2.2

3.4

$\sigma(\sqrt{2}) = \sigma(0 + 1 \cdot \sqrt{2}) = -\sqrt{2}$ , and $-\sqrt{2} < 0$ in $K$ by step 1.4.

step 2.2step 1.4L4

4.1

By steps 3.1, 3.2, and 3.3, $\sigma$ satisfies the three homomorphism identities, so $\sigma : K \to K$ is a field homomorphism between ordered fields.

step 3.1step 3.2step 3.3L3

5.1

Steps 2.1 and 4.1 exhibit a field homomorphism $\sigma$ between ordered fields with $\sqrt{2} > 0$ in the domain yet $\sigma(\sqrt{2}) = -\sqrt{2} < 0$ by step 3.4, so $\sigma$ is not order-preserving, refuting the claim that every field homomorphism between ordered fields is order-preserving.

step 2.1step 4.1step 3.4L4

6.1

There is no conflict with [L5]: if $K$ were complete, [L5] would make $\sigma$ order-preserving, contrary to step 5.1. Hence $K$ is not complete.

step 5.1L5∎

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

Not every ordered field is Archimedean

Statement refuted

Refuted claim: every ordered field is Archimedean, that is, in every ordered field $F$ each $x \in F$ satisfies $x < n \cdot 1_F$ for some natural number $n$ .

The witness is $\mathbb{R}(t)$ , the field of rational functions over $\mathbb{R}$ , ordered so that $f > 0$ exactly when $f(x) > 0$ for all sufficiently large real $x$ . In this ordered field the element $t$ exceeds every canonical natural number, so the naturals are not cofinal.

Facts & Assumptions

Given: $\mathbb{R}(t)$ , the field of fractions of the polynomial ring $\mathbb{R}[t]$ , and the set $P = \{f \in \mathbb{R}(t) : f \ne 0 \text{ and } f(x) > 0 \text{ for all sufficiently large real } x\}$ .

[L1]

An ordered field is a field with a positive cone $P$ satisfying trichotomy (for each nonzero $x$ , exactly one of $x \in P$ , $-x \in P$ ) and closure of $P$ under addition and multiplication; then $a < b$ means $b - a \in P$ (Ordered field).

[L2]

An ordered field $F$ is Archimedean when for every $x \in F$ there is a natural number $n$ with $x < n \cdot 1_F$ , equivalently the canonical naturals $n \cdot 1_F$ are cofinal (Archimedean ordered field).

[L3]

Every complete ordered field is Archimedean (Every complete ordered field is Archimedean).

[L4]

$\mathbb{R}$ is a totally ordered field (The reals form a totally ordered field).

Counterexample

technique · direct

1.1

Let $f=p/q\ne0$ , where $p(x)=a_mx^m+\cdots+a_0$ and $q(x)=b_nx^n+\cdots+b_0$ have nonzero leading coefficients. For $x>1$ , dividing by the leading terms gives $p(x)=a_mx^m(1+\sum_{i<m}(a_i/a_m)x^{i-m})$ and the analogous formula for $q$ . If $x$ is larger than $1$ plus the sums of the absolute values of the lower coefficient ratios, then both lower-term sums have absolute value less than $1$ . Thus $p(x)$ and $q(x)$ eventually have the signs of $a_m$ and $b_n$ , respectively, and $f(x)$ has the constant nonzero eventual sign of $a_m/b_n$ . Hence exactly one of $f\in P$ and $-f\in P$ holds.

givenL4algebra

1.2

If $f, g \in P$ then $f(x) > 0$ and $g(x) > 0$ for all large $x$ , so $(f + g)(x) > 0$ and $(fg)(x) > 0$ for all large $x$ , giving $f + g \in P$ and $fg \in P$ .

givenalgebra

1.3

For each natural number $n$ the rational function $t - n \cdot 1 = t - n$ satisfies $(t - n)(x) = x - n > 0$ for all $x > n$ , so $t - n \in P$ .

givenalgebra

2.1

By the trichotomy of step 1.1 and the closure of step 1.2, $P$ is a positive cone, so $\mathbb{R}(t)$ is an ordered field.

step 1.1step 1.2L1

2.2

By step 1.3, $t - n \cdot 1 \in P$ for every natural $n$ , which by [L1] means $n \cdot 1 < t$ for every natural $n$ .

step 1.3L1

3.1

In the ordered field $\mathbb{R}(t)$ the element $t$ satisfies $n \cdot 1 < t$ for every natural $n$ (step 2.2), so no natural $n$ has $t < n \cdot 1$ ; the canonical naturals are not cofinal and $\mathbb{R}(t)$ is not Archimedean, refuting the claim that every ordered field is Archimedean.

step 2.1step 2.2L2

4.1

This is consistent with [L3], whose contrapositive states that a non-Archimedean ordered field cannot be complete: $\mathbb{R}(t)$ is an ordered field that is not complete.

step 3.1L3∎

False statementConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

FALSE: there exist two non-isomorphic complete ordered fields

Statement

False statement. There exist two complete ordered fields (Complete ordered field (least-upper-bound property)) that are not isomorphic; that is, completeness together with the ordered-field axioms fails to determine the real numbers up to isomorphism.

Facts & Assumptions

Given: The claim that there are complete ordered fields $F$ and $G$ admitting no ordered-field isomorphism between them.

[L1]

Any two complete ordered fields are isomorphic via a unique ordered-field isomorphism (Uniqueness of the complete ordered field: $\mathbb{R}$ up to a unique isomorphism).

[L2]

A complete ordered field is one with the least-upper-bound property (Complete ordered field (least-upper-bound property)).

[L3]

An ordered-field isomorphism is a bijective, order-preserving field homomorphism (Ordered-field isomorphism).

Refutation

technique · direct

1.1

Let $F$ and $G$ be any complete ordered fields, as the claim posits, each with the least-upper-bound property.

givenL2

1.2

By [L1] there exists an ordered-field isomorphism $\varphi : F \to G$ (indeed a unique one).

2.1

Hence $F$ and $G$ are isomorphic, contradicting the asserted non-isomorphism; since $F, G$ were arbitrary complete ordered fields, no non-isomorphic pair can exist and the statement is false.

step 1.1step 1.2L3∎

Sources

Standard references

Recommended treatments; not extraction sources.

Foundations of the Real Numbers for Analysis

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Field

Definition

Remarks

Ordered field

Definition

Remarks

Absolute value in an ordered field

Definition

Remarks

Archimedean ordered field

Definition

Remarks

Complete ordered field (least-upper-bound property)

Definition

Remarks

Field homomorphism and embedding

Definition

Remarks

Ordered-field isomorphism

Definition

Remarks

Identities and inverses in a field are unique

Statement

Facts & Assumptions

Proof

Multiplication by zero: 0⋅a=00 \cdot a = 00⋅a=0

Statement

Facts & Assumptions

Proof

Sign rules for products: (−a)b=−(ab)(-a)b = -(ab)(−a)b=−(ab) and (−a)(−b)=ab(-a)(-b) = ab(−a)(−b)=ab

Statement

Facts & Assumptions

Proof

(−1)(−1)=1(-1)(-1) = 1(−1)(−1)=1

Statement

Facts & Assumptions

Proof

A field has no zero divisors: ab=0⇒a=0ab = 0 \Rightarrow a = 0ab=0⇒a=0 or b=0b = 0b=0

Statement

Facts & Assumptions

Proof

Multiplicative cancellation: c≠0c \ne 0c=0 and ac=bc⇒a=bac = bc \Rightarrow a = bac=bc⇒a=b

Statement

Facts & Assumptions

Proof

Order is preserved by adding a constant and by adding inequalities

Statement

Facts & Assumptions

Proof

Sign rules for products and monotonicity of multiplication

Statement

Facts & Assumptions

Proof

Squares of nonzero elements are positive

Statement

Facts & Assumptions

Proof

The multiplicative identity is positive

Statement

Facts & Assumptions

Proof

Inverses of positives are positive, and reciprocation reverses order

Statement

Facts & Assumptions

Proof

Basic properties of the absolute value

Statement

Facts & Assumptions

Proof

The triangle inequality

Statement

Facts & Assumptions

Proof

The reverse triangle inequality

Statement

Multiplication by zero: $0 \cdot a = 0$

Sign rules for products: $(-a)b = -(ab)$ and $(-a)(-b) = ab$

$(-1)(-1) = 1$

A field has no zero divisors: $ab = 0 \Rightarrow a = 0$ or $b = 0$

Multiplicative cancellation: $c \ne 0$ and $ac = bc \Rightarrow a = b$

Reciprocals and order: $1/r$ against $1$

When $ab < b$ for positive $a, b$

The canonical natural $\iota(n) = n \cdot 1_F$ of a field

For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$

Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$

Field homomorphisms between ordered fields fix $\mathbb{Q}$

Uniqueness of the complete ordered field: $\mathbb{R}$ up to a unique isomorphism