Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck 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.1L1givenalgebra

Let n=(x‾1,x‾2,… ). Each generator x‾i 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 n⊆Nil⁡(A). Conversely, the quotient A/n≅k is reduced, so every nilpotent element of A lies in n. Thus Nil⁡(A)=n.

1.2givenalgebra

For every integer N≥1, the element x‾N+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 nN≠0 for every N, so n is not nilpotent.

2.1step 1.1step 1.2∎

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

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