LemmaStatement: AI-adaptedProof: AI-generatedprecheck 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.

Null sequences are Cauchy

Statement

Every null sequence (Null sequence) is a Cauchy sequence (Cauchy sequence of rationals).

Facts & Assumptions

Given: A null sequence $(a_{n})$ and a rational $ε > 0$ .

[A1]

Null: for every rational $δ > 0$ there is $N$ with $∣ a_{n} ∣ < δ$ for all $n \geq N$ .

[A2]

Cauchy: for every rational $δ > 0$ there is $N$ with $∣ a_{m} - a_{n} ∣ < δ$ for all $m, n \geq N$ .

[L1]

Field arithmetic in $Q$ : $ε / 2 > 0$ and $ε / 2 + ε / 2 = ε$ (The rationals form a field, The rationals form a totally ordered field).

[L2]

Triangle inequality (Absolute value and the triangle inequality).

Proof

technique · direct

1.1

$ε / 2$ is a positive rational.

2.1

Fix $N$ with $∣ a_{n} ∣ < ε / 2$ for all $n \geq N$ .

step 1.1A1

3.1

For $m, n \geq N$ : $∣ a_{m} - a_{n} ∣ \leq ∣ a_{m} ∣ + ∣ a_{n} ∣ < ε / 2 + ε / 2 = ε$ .

step 2.1L1L2

4.1

$(a_{n})$ is Cauchy.

step 3.1A2∎

Depends on

Used by

Null sequences form an ideal Lemma

Dependency tree · two levels

12 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.2 (standard reference, not scraped)