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

A non-null Cauchy sequence is eventually bounded away from zero, with constant sign

Statement

If $(a_n)$ is Cauchy but not null, there are a rational $\delta > 0$ and an index $N_0$ such that $|a_n| > \delta$ for all $n \ge N_0$ ; moreover either $a_n > \delta$ for all $n \ge N_0$ , or $a_n < -\delta$ for all $n \ge N_0$ .

Facts & Assumptions

Given: A Cauchy sequence $(a_n)$ that is not null.

[A1]

Negation of null (Null sequence): there is a rational $\varepsilon_0 > 0$ such that for every $N$ some $n \ge N$ has $|a_n| \ge \varepsilon_0$ .

[A2]

Cauchy (Cauchy sequence of rationals).

[L1]

Ordered-field arithmetic: $\varepsilon_0/3 > 0$ , $\varepsilon_0 - \varepsilon_0/3 > \varepsilon_0/3$ (The rationals form a totally ordered field).

[L2]

Triangle inequality, in the form $|u| \ge |v| - |v - u|$ (Absolute value and the triangle inequality).

Proof

technique · direct

1.1

Fix $\varepsilon_0 > 0$ witnessing that $(a_n)$ is not null.

1.2

Fix $N_0$ with $|a_m - a_n| < \varepsilon_0/3$ for all $m, n \ge N_0$ .

A2L1

2.1

Pick $n_0 \ge N_0$ with $|a_{n_0}| \ge \varepsilon_0$ .

step 1.1step 1.2

3.1

For every $n \ge N_0$ : $|a_n| \ge |a_{n_0}| - |a_{n_0} - a_n| > \varepsilon_0 - \varepsilon_0/3 > \varepsilon_0/3 =: \delta$ ; so $|a_n| > \delta$ for all $n \ge N_0$ .

step 2.1step 1.2L2L1

4.1

Sign stability: if some $a_m > \delta$ and some $a_n < -\delta$ with $m, n \ge N_0$ , then $|a_m - a_n| > 2\delta = 2\varepsilon_0/3 > \varepsilon_0/3$ , impossible by step 1.2; so beyond $N_0$ all terms have one sign, and by step 3.1 either $a_n > \delta$ for all $n \ge N_0$ or $a_n < -\delta$ for all $n \ge N_0$ .

step 3.1step 1.2L1∎

Depends on

Used by

The null ideal is maximal Lemma
The reals form a totally ordered field Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 25 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

T. Tao, Analysis I, 3rd ed., §5.4 (standard reference, not scraped)
L. S. Krapp, Constructions of the real numbers: a set theoretical approach (Oxford, 2014) (standard reference, not scraped)