LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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 $N$ of null sequences is an ideal of the ring $C$ of Cauchy sequences (Cauchy sequences form a commutative ring): it is a subgroup under addition, and $c \cdot z \in N$ whenever $c \in C$ and $z \in N$ .

Facts & Assumptions

Given: Null sequences $(z_{n}), (w_{n})$ , a Cauchy sequence $(c_{n})$ , and a rational $ε > 0$ .

[A1]

Null: beyond some index, $∣ z_{n} ∣$ is smaller than any prescribed positive rational.

[L1]

Ordered-field arithmetic in $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 $N \subseteq C$ (Null sequences are Cauchy).

Proof

technique · direct

1.1A1L1

Fix $N_{z}, N_{w}$ with $∣ z_{n} ∣ < ε / 2$ for $n \geq N_{z}$ and $∣ w_{n} ∣ < ε / 2$ for $n \geq N_{w}$ .

1.2L3

Fix $M \geq 0$ with $∣ c_{n} ∣ \leq M$ ([L3]) and set $B = \max (M, 1) \geq 1$ , so $∣ c_{n} ∣ \leq B$ for all $n$ .

2.1step 1.1L2

Sum: for $n \geq \max (N_{z}, N_{w})$ , $∣ z_{n} + w_{n} ∣ \leq ∣ z_{n} ∣ + ∣ w_{n} ∣ < ε$ ; negation: $∣ - z_{n} ∣ = ∣ z_{n} ∣$ . So $N$ is a subgroup under addition.

2.2step 1.2A1L1

Fix $N$ with $∣ z_{n} ∣ < ε / B$ for $n \geq N$ .

3.1step 1.2step 2.2L2

Product: for $n \geq N$ , $∣ c_{n} z_{n} ∣ = ∣ c_{n} ∣ ∣ z_{n} ∣ \leq B ∣ z_{n} ∣ < ε$ ; so $(c_{n} z_{n})$ is null.

4.1step 2.1step 3.1L4∎

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

Null sequences form an ideal

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources