LemmaStatement: Literature-sourcedProof: 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.

Null sequences form an ideal

Statement

The set $\mathcal{N}$ of null sequences is an ideal of the ring $\mathcal{C}$ of Cauchy sequences (Cauchy sequences form a commutative ring): it is a subgroup under addition, and $c \cdot z \in \mathcal{N}$ whenever $c \in \mathcal{C}$ and $z \in \mathcal{N}$ .

Facts & Assumptions

Given: Null sequences $(z_n), (w_n)$ , a Cauchy sequence $(c_n)$ , and a rational $\varepsilon > 0$ .

[A1]

Null: beyond some index, $|z_n|$ is smaller than any prescribed positive rational.

[L1]

Ordered-field arithmetic in $\mathbb{Q}$ (The rationals form a totally ordered field).

[L2]

Triangle inequality and multiplicativity of $|\cdot|$ (Absolute value and the triangle inequality).

[L3]

Cauchy sequences are bounded (Every Cauchy sequence of rationals is bounded).

[L4]

Null sequences are Cauchy, so $\mathcal{N} \subseteq \mathcal{C}$ (Null sequences are Cauchy).

Proof

technique · direct

1.1

Fix $N_z, N_w$ with $|z_n| < \varepsilon/2$ for $n \ge N_z$ and $|w_n| < \varepsilon/2$ for $n \ge N_w$ .

A1L1

1.2

Fix $M \ge 0$ with $|c_n| \le M$ ([L3]) and set $B = \max(M, 1) \ge 1$ , so $|c_n| \le B$ for all $n$ .

2.1

Sum: for $n \ge \max(N_z, N_w)$ , $|z_n + w_n| \le |z_n| + |w_n| < \varepsilon$ ; negation: $|-z_n| = |z_n|$ . So $\mathcal{N}$ is a subgroup under addition.

step 1.1L2

2.2

Fix $N$ with $|z_n| < \varepsilon/B$ for $n \ge N$ .

step 1.2A1L1

3.1

Product: for $n \ge N$ , $|c_n z_n| = |c_n|\,|z_n| \le B\,|z_n| < \varepsilon$ ; so $(c_n z_n)$ is null.

step 1.2step 2.2L2

4.1

$\mathcal{N}$ is a nonempty additive subgroup of $\mathcal{C}$ absorbing multiplication by $\mathcal{C}$ : an ideal.

step 2.1step 3.1L4∎

Depends on

Used by

The real numbers Definition
Null rational sequences form a maximal ideal in the ring of rational Cauchy sequences Example
The reals are the quotient of rational Cauchy sequences by the maximal ideal of null sequences Example
FALSE: the rationals are complete False statement
The null ideal is maximal Lemma
The reals form a field Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 28 results over 14 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.3 (standard reference, not scraped)
L. S. Krapp, Constructions of the real numbers: a set theoretical approach (Oxford, 2014) (standard reference, not scraped)