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.

Depends on

Used by

Brownian paths are locally Holder below one half Corollary
Brownian paths have infinite total variation Corollary
Conditional cauchy schwarz inequality Corollary
No function ℝ → ℝ is continuous at every rational and discontinuous at every irrational, because ℚ is not G_δ Corollary
One-dimensional Brownian motion is recurrent Corollary
ℚ is F_σ, meager and not G_δ, while the irrationals are G_δ, residual and not F_σ Corollary
Standard borel spaces have countable generating and measure determining algebras Corollary
Stolz-Cesaro, 0/0 form: if bₖ is strictly decreasing to 0, aₖ → 0, and the difference quotient converges, then aₖ/bₖ converges to the same value Corollary
The Brownian zero set is uncountable Corollary
The Cauchy-sequence reals have the least-upper-bound property Corollary
The critical Hölder boundary at zero Corollary
A nonconstant summary can lose an identifiable parameter Counterexample
A null sequence times an unbounded sequence need not be null: (k+1)⁻¹·(k+1) = 1 Counterexample
An identifiable model can have persistent ABC summary distortion Counterexample
An infinite-dimensional Gaussian has no locally finite translation-invariant density reference Counterexample
An unbounded stopped exponential martingale needs uniform integrability Counterexample
In ℝ the interiors of ℚ and of its complement are both empty while the interior of their union is everything Counterexample
Infinite-dimensional Gaussian random-walk reverse flow is singular Counterexample
On (0,∞) the metrics |x-y| and |1/x - 1/y| share their topology and not their Cauchy sequences Counterexample
On ℕ with d(m,n) = 1 + 1/(m+n) for m ≠ n the sets {n, n+1, …} are nested, closed, bounded and complete with empty intersection Counterexample
On the positive integers the metrics |m-n| and |1/m - 1/n| both induce the discrete topology, and only the first is complete Counterexample
ℚ ∩ [0,1] has measure zero and not content zero, although it is bounded Counterexample
ℚ ∩ [0,2] is bounded and disconnected, so being an interval of ℚ is not enough Counterexample
ℚ is dense in ℝ and has measure zero Counterexample
ℝ is the union of a meager set and a set of measure zero, so smallness of category and smallness of measure are independent notions Counterexample
ℝ/ℚ carries the indiscrete topology, although ℝ is metrizable and the quotient has more than one point Counterexample
Refuted: the agreement set of two continuous maps is closed, with no hypothesis on the codomain. Two continuous maps ℝ → {a,b} into the indiscrete two-point space have agreement set ℚ Counterexample
The indicator of ℚ has a limit at no point of ℝ Counterexample
The indicator of ℚ is continuous at no point of ℝ Counterexample
The irrationals form a residual G_δ set that is not F_σ Counterexample
The truncated decimal approximations of √2 form a Cauchy sequence of rationals with no rational limit Counterexample
x ↦ 1/x is continuous on (0,1) and sends the Cauchy sequence (1/(k+2))_k ≥ 0 to an unbounded one Counterexample
x ↦ x/2 maps (0,1] into itself, is a 1/2-contraction, and has no fixed point Counterexample
ψ(1/x) has no limit at 0: two sequences tending to 0 give values constantly 0 and constantly 1/2 Counterexample
Cauchy sequence in a metric space Definition
Convergence of a sequence in a metric space: xₖ → x iff d(xₖ, x) → 0 in ℝ Definition
Countably Infinite-Mode CAR C*-Algebra Definition
Measurable and decomposable operator fields Definition
Real powers from suprema of rational powers, with the reciprocal convention below base one Definition
Sequences of reals: bounded, eventually, frequently, tails, subsequences Definition

…and 209 more results.

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

T. Tao, Analysis I, 3rd ed., §5.4 (standard reference, not scraped)
Dense set (Wikipedia) (standard reference, not scraped)