LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-07-25

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

ℚ is dense in every Archimedean ordered field

Statement

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

Facts & Assumptions

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

[L1]

Archimedean property: for every $w \in F$ there is $n \geq 1$ with $w < n \cdot 1_{F}$ (Archimedean ordered field).

[L2]

$ι$ is an order-preserving field homomorphism with $ι (m / n) = ι (m) (n \cdot 1_{F})^{- 1}$ for $n \geq 1$ (The unique embedding of ℚ into an ordered field).

[L3]

Canonical naturals: $n \cdot 1_{F} > 0$ for $n \geq 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 $a c < b c$ , and products of positives are positive (Sign rules for products and monotonicity of multiplication).

[L6]

Every nonempty $T \subseteq 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.1L1L4choose

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 \geq 1$ with $(y - x)^{- 1} < n \cdot 1_{F}$ .

1.2L1L2L3L6choose

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 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 \leq - M$ , monotonicity of $k \mapsto k \cdot 1_{F} = ι (k)$ on $Z$ , which is [L2], would force $k \cdot 1_{F} \leq - 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$ .

2.1step 1.1L4L5

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

2.2step 1.2

By minimality of $m$ , $(m - 1) \cdot 1_{F} \leq (n \cdot 1_{F}) x < m \cdot 1_{F}$ .

3.1step 2.2L2L4L5

Set $q = m / n \in Q$ , so $ι (q) = ι (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 < ι (m) (n \cdot 1_{F})^{- 1} = ι (q)$ .

3.2step 2.2L3L4L5

From $(m - 1) \cdot 1_{F} = m \cdot 1_{F} - 1_{F} \leq (n \cdot 1_{F}) x$ , dividing by the positive $n \cdot 1_{F}$ gives $ι (q) - (n \cdot 1_{F})^{- 1} \leq x$ , that is $ι (q) \leq x + (n \cdot 1_{F})^{- 1}$ .

4.1step 3.2step 2.1

Combining with 2.1, $ι (q) \leq x + (n \cdot 1_{F})^{- 1} < x + (y - x) = y$ .

5.1step 3.1step 4.1∎

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

ℚ is dense in every Archimedean ordered field

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources