Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27
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-Noetherian nilradical need not be nilpotent

Example

Let

A=k[x1,x2,]/(x1,x22,x33,).

Then the nilradical of A is the ideal generated by the residue classes of the variables xi, but that ideal is not nilpotent.

Facts & Assumptions

Given: A field k and the quotient ring A=k[x1,x2,]/(x1,x22,x33,).

[L1]

The nilradical is the ideal of all nilpotent elements (The nilradical and reduced rings).

Verification

technique · direct
1.1

Let n=(x1,x2,). Each generator xi is nilpotent, and every element of n involves only finitely many generators, so in this commutative ring it is a finite sum of commuting nilpotents and hence nilpotent. Therefore nNil(A). Conversely, the quotient A/nk is reduced, so every nilpotent element of A lies in n. Thus Nil(A)=n.

L1givenalgebra
1.2

For every integer N1, the element xN+1N lies in nN. It is nonzero in A because only the (N+1)-st power of xN+1 is killed by the defining relations. Hence nN0 for every N, so n is not nilpotent.

givenalgebra
2.1

This shows that the Noetherian hypothesis in the nilradical-nilpotence theorem is essential.

step 1.1step 1.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

2 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