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.

The null ideal is maximal

Statement

If $(a_n) \in \mathcal{C} \setminus \mathcal{N}$ , then the ideal of $\mathcal{C}$ generated by $\mathcal{N}$ and $(a_n)$ is all of $\mathcal{C}$ . Hence $\mathcal{N}$ is a maximal ideal.

Facts & Assumptions

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

[L1]

Away-from-zero: there are $\delta > 0$ and $N_0$ with $|a_n| > \delta$ for all $n \ge N_0$ (A non-null Cauchy sequence is eventually bounded away from zero, with constant sign).

[L2]

Triangle inequality and $|uv| = |u||v|$ (Absolute value and the triangle inequality).

[L3]

Cauchy definition and field arithmetic in $\mathbb{Q}$ : $\varepsilon\delta^2 > 0$ for $\varepsilon > 0$ (The rationals form a totally ordered field).

[L4]

Null definition; a sequence that is $0$ from some index on is null (Null sequence).

[L5]

Ideal arithmetic in $\mathcal{C}$ : an ideal containing $1$ is the whole ring (Cauchy sequences form a commutative ring, Null sequences form an ideal).

Proof

technique · direct

1.1

Fix $\delta > 0$ and $N_0$ with $|a_n| > \delta$ for all $n \ge N_0$ ; in particular $a_n \ne 0$ there.

2.1

Define $b_n = 1$ for $n < N_0$ and $b_n = 1/a_n$ for $n \ge N_0$ .

step 1.1choose

3.1

$(b_n)$ is Cauchy: for $m, n \ge N_0$ , $|b_m - b_n| = \dfrac{|a_n - a_m|}{|a_m|\,|a_n|} < \dfrac{|a_m - a_n|}{\delta^2}$ ; given $\varepsilon > 0$ , choosing the Cauchy index of $(a_n)$ at $\varepsilon\delta^2$ makes this $< \varepsilon$ .

step 2.1step 1.1L2L3

3.2

For $n \ge N_0$ , $a_n b_n = 1$ , so the sequence $(a_n b_n - 1)$ is $0$ from $N_0$ on, hence null.

step 2.1L4

4.1

Therefore $1_{\mathcal{C}} = (a_n)(b_n) - \bigl((a_n b_n) - 1\bigr)$ lies in the ideal generated by $(a_n)$ and $\mathcal{N}$ , so that ideal is all of $\mathcal{C}$ ; any ideal strictly containing $\mathcal{N}$ contains a non-null element and thus equals $\mathcal{C}$ : $\mathcal{N}$ is maximal.

step 3.1step 3.2L5∎

Depends on

Used by

Dependency tree · next 3 levels

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