LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 $\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∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 46 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed. (standard reference, not scraped)
University of Pennsylvania Math 360 notes: Ordered fields (standard reference, not scraped)