LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)

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.

The rationals embed densely in the reals

Statement

The map $q \mapsto \hat{q}$ (The real numbers) is an embedding of ordered fields. Every real is approximated by rationals: for $x \in R$ and rational $ε > 0$ there is $q \in Q$ with $∣ x - \hat{q} ∣ < \hat{ε}$ . Consequently, strictly between any two reals lies a rational.

Statement references

The real numbers

Facts & Assumptions

Given: A real $x = [(a_{n})]$ and a rational $ε > 0$ .

[L1]

The orders of $Q$ and $R$ ; ordered-field arithmetic (The rationals form a totally ordered field, The reals form a totally ordered field).

[L2]

Field arithmetic in $Q$ : $ε / 2, δ / 4$ are positive rationals, and every nonzero rational $q$ has a reciprocal $1 / q$ with $q \cdot (1 / q) = 1$ (The rationals form a field).

[L3]

Cauchy definition (Cauchy sequence of rationals).

[L4]

Real positivity via eventual rational lower bounds (Order on the reals).

[L5]

$R = C / N$ is a field (The reals form a field), and $0_{R} = \hat{0}$ , $1_{R} = \hat{1}$ are the classes of the constant sequences (The real numbers). A multiplicative inverse there is unique: if $a b = 1_{R} = a c$ then $b = b (a c) = (b a) c = c$ .

Proof

technique · direct

1.1L1L4

Embedding: constant sequences are Cauchy; $\hat{q} = \hat{r}$ iff the constant $q - r$ is null iff $q = r$ ; operations match termwise; and $q < r$ gives the constant lower bound $r - q > 0$ , so $\hat{q} < \hat{r}$ and order is preserved and reflected.

1.2L3L2

Fix $N$ with $∣ a_{m} - a_{n} ∣ < ε / 2$ for all $m, n \geq N$ , and set $q = a_{N}$ .

2.1step 1.2L4L1

The difference $\hat{q} - x$ has representative $(a_{N} - a_{n})$ with $∣ a_{N} - a_{n} ∣ < ε / 2$ for $n \geq N$ ; hence both $\hat{ε} - (x - \hat{q})$ and $\hat{ε} - (\hat{q} - x)$ have representatives eventually $> ε / 2$ , so both are positive: $∣ x - \hat{q} ∣ < \hat{ε}$ .

2.2step 1.1L2L5

Inverses: let $q$ be a nonzero rational. Then $\hat{q} \neq \hat{0} = 0_{R}$ by the injectivity of step 1.1, and $1 / q$ exists in $Q$ by [L2]; since the operations match termwise (step 1.1), $\hat{q} \cdot \hat{1 / q} = \hat{q \cdot (1 / q)} = \hat{1} = 1_{R}$ . Inverses in $R$ are unique by [L5], so $(\hat{q})^{- 1} = \hat{1 / q}$ : the embedding preserves reciprocals.

3.1step 2.1L4L1L2

Density: let $x < y$ ; pick $δ > 0$ rational and $N$ with the representative of $y - x$ eventually $> δ$ ; set $ε = δ / 4$ and pick $q$ with $∣ x - \hat{q} ∣ < \hat{ε}$ ; then $q^{'} = q + 2 ε$ satisfies ${\hat{q}}^{'} - x \geq - \hat{ε} + 2 \hat{ε} = \hat{ε} > 0$ and $y - {\hat{q}}^{'} \geq \hat{δ} - \hat{ε} - 2 \hat{ε} = \hat{δ} / 4 > 0$ , so $x < {\hat{q}}^{'} < y$ .

4.1step 1.1step 2.2step 3.1∎

The rationals embed as an ordered subfield — injectively, preserving the order in both directions, the ring operations, and reciprocals — and they approximate every real arbitrarily well and separate any two reals.

The rationals embed densely in the reals

Statement

Statement references

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources