Alphabeta Math
CorollaryStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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.

If R is Noetherian then R[x1,…,xn] is Noetherian for every n∈N

Statement

Let R be a Noetherian commutative ring. Then the iterated polynomial ring R[x1,…,xn] of Polynomial rings in finitely many commuting indeterminates by iteration is Noetherian for every n∈N.

The index starts at 0, where the published definition sets R[x1,…,x0]=R and the assertion is the hypothesis itself.

Facts & Assumptions

Given: A Noetherian commutative ring R.

[L1]

Polynomial rings in finitely many commuting indeterminates are defined recursively by R[x1,…,x0]:=R and R[x1,…,xn+1]:=R[x1,…,xn][xn+1] (Polynomial rings in finitely many commuting indeterminates by iteration).

[L2]

If R is a Noetherian commutative ring then R[x] is a Noetherian commutative ring (Hilbert basis theorem: if R is Noetherian then R[x] is Noetherian).

Proof

technique · induction
1.1baseL1given

At n=0 the recursive definition gives R[x1,…,x0]=R, which is Noetherian by hypothesis; this is the base of the induction and is not skipped.

1.2ih

Let n∈N and assume R[x1,…,xn] is Noetherian.

2.1L1L2step 1.2

The recursive definition gives R[x1,…,xn+1]=R[x1,…,xn][xn+1], a polynomial ring in one indeterminate over the ring assumed Noetherian in step 1.2; the Hilbert basis theorem applied to that ring makes R[x1,…,xn+1] Noetherian.

3.1step 1.1step 2.1discharge-induction∎

The base case of step 1.1 and the passage of step 2.1 give, by induction on n, that R[x1,…,xn] is Noetherian for every n∈N.

Remarks

  • Finitely many indeterminates is essential. The induction produces a proof for each n∈N separately and says nothing about a ring of polynomials in infinitely many indeterminates; the companion examples page carries a witness that the conclusion fails there.

  • The converse holds too, by iterating R[x] is Noetherian if and only if R is Noetherian down the tower of coefficient rings.

Depends on

Dependency tree · 2 levels

Sources