LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)audited 2026-07-24

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 are Archimedean

Statement

For every rational $x$ there is a natural number $n$ with $x < n$ . Consequently, for every rational $\varepsilon > 0$ there is a natural $n \ge 1$ with $1/n < \varepsilon$ .

Facts & Assumptions

Given: A rational $x = [(a,b)]$ with $b > 0$ .

[L1]

The order and arithmetic of $\mathbb{Q}$ (The rationals form a totally ordered field).

[L2]

Integer facts: positive integers are exactly $\iota(m)$ with $m \ge 1$ natural; nonnegative integers are the image of $\mathbb{N}$ ; the embeddings preserve arithmetic and order (The naturals embed in the integers, The integers embed in the rationals, The integers form a totally ordered ring).

Proof

technique · direct

1.1

Since $b > 0$ , $b$ lies in the image of $\mathbb{N}$ and $b \ge 1$ .

1.2

If $a \le 0$ set $k = 0$ ; otherwise $a$ is a positive integer, so $a = \iota(k)$ for some natural $k \ge 1$ . In both cases $a \le k$ (as integers).

2.1

Then $a < k + 1$ and, since $b \ge 1$ and $k+1 > 0$ , also $k + 1 \le (k+1)b$ .

step 1.1step 1.2L2

3.1

Hence $a < (k+1)b$ , and dividing by $b > 0$ (order-scaling in the definition of the rational order), $x = [(a,b)] < [( (k+1)b,\, b)] = k+1 =: n$ .

step 2.1L1

4.1

For rational $\varepsilon > 0$ : apply the above to $x = 1/\varepsilon$ to get $n$ with $1/\varepsilon < n$ , hence $1/n < \varepsilon$ .

step 3.1L1∎

Depends on

Used by

On a closed interval of ℚ there is a continuous unbounded function, a bounded one with no maximum, and one without the intermediate value property Counterexample
The sequence 1/n is null Example
FALSE: the rationals are complete False statement
For a cut A, -A is a cut and A + (-A) = 0^* Lemma
For a positive cut A, the reciprocal A⁻¹ satisfies A · A⁻¹ = 1^* Lemma
The Cauchy-sequence reals are Archimedean Lemma
The Dedekind reals are Archimedean Lemma
Conventions for sequences: indexing, eventually, lim, and rational ε Remark
The reals are complete Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 42 results over 16 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

T. Tao, Analysis I, 3rd ed., §4.2 (standard reference, not scraped)
Archimedean property (Wikipedia) (standard reference, not scraped)