ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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.

Working the Hilbert basis construction on an ideal of $Z [x]$ with non-monic stages

Example

Take $a = (2 x, 3 x^{2}, x^{3})$ in $Z [x]$ . Its stage ideals (The leading coefficients of the degree- $n$ elements of an ideal of $R [x]$ , together with $0$ , form an ideal of $R$ , and these ideals ascend with $n$ ) are

$a_{0} = 0, a_{1} = (2), a_{n} = Z for n \geq 2,$

so the chain stabilises at $N = 2$ . Choosing the realisers $2 x$ at stage $1$ and $x^{2}$ at stage $2$ , the generating list produced by Over a Noetherian ring, an ideal of $R [x]$ is generated by finitely many polynomials realising generators of its stages up to the stabilisation degree is $2 x, x^{2}$ , and indeed $a = (2 x, x^{2})$ .

The reduction of A single cancellation step lowers the degree of a polynomial in an ideal once its leading coefficient lies in a realised stage applied to $f = 5 x^{4} + 2 x \in a$ at stage $n = 2$ subtracts $h = 5 x^{4}$ and leaves $2 x$ , of degree $1$ ; applied again at stage $n = 1$ it subtracts $2 x$ and leaves $0$ .

The stage $a_{1} = (2)$ is generated by a non-unit, so no division by a leading coefficient is available at that stage; the reduction uses the stage ideal instead.

Facts & Assumptions

Given: The ring $Z [x]$ and the ideal $a = (2 x, 3 x^{2}, x^{3})$ .

[L1]

$R [x]$ is the set of finitely supported functions $N \to R$ , with coefficientwise addition and the convolution product $(a b)_{i} = \sum_{j + k = i} a_{j} b_{k}$ (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[L2]

For $0 \neq f \in R [x]$ the degree is the largest index carrying a nonzero coefficient and the leading coefficient is the coefficient there; the zero polynomial has no degree and no leading coefficient (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L3]

For $S \subseteq R$ , $(S)$ is the intersection of all two-sided ideals containing $S$ , so $S \subseteq (S)$ (The ideal generated by a subset and principal ideals).

[L4]

In a commutative ring, $(S)$ consists of finite sums $\sum r_{i} s_{i}$ , and $(a) = R a$ (In a commutative ring, $(S)$ consists of finite sums $\sum r_{i} s_{i}$ , and $(a) = R a$ ).

[L5]

For an ideal $a$ of $R [x]$ and $n \in N$ , the set $a_{n}$ of leading coefficients of the nonzero degree- $n$ elements of $a$ , together with $0$ , is an ideal of $R$ , and $a_{n} \subseteq a_{n + 1}$ (The leading coefficients of the degree- $n$ elements of an ideal of $R [x]$ , together with $0$ , form an ideal of $R$ , and these ideals ascend with $n$ ).

[L6]

Over a Noetherian ring, with $N$ a stabilisation index of the stage chain and with realisers chosen for generators of $a_{n}$ for each $n \leq N$ , those realisers generate $a$ (Over a Noetherian ring, an ideal of $R [x]$ is generated by finitely many polynomials realising generators of its stages up to the stabilisation degree).

[L7]

With $a_{n} = (c_{1}, \dots, c_{m})$ realised at stage $n$ by $g_{1}, \dots, g_{m}$ , a nonzero $f \in a$ of degree $d \geq n$ with $lc (f) = \sum_{j} r_{j} c_{j} \in a_{n}$ admits $h = \sum_{j} r_{j} x^{d - n} g_{j}$ in the ideal generated by the $g_{j}$ with $f - h = 0$ or $\deg (f - h) < d$ (A single cancellation step lowers the degree of a polynomial in an ideal once its leading coefficient lies in a realised stage).

[L8]

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

[L9]

$Z$ is a Noetherian ring (Fields and $Z$ are Noetherian, and so are their polynomial rings in finitely many variables).

Verification

technique · direct

1.1L1L2L3L4given

Every element of $a$ is $a \cdot 2 x + b \cdot 3 x^{2} + c \cdot x^{3}$ with $a, b, c \in Z [x]$ . Its constant coefficient is $0$ , since each of $2 x$ , $3 x^{2}$ , $x^{3}$ has support in the indices $\geq 1$ ; and its coefficient at $x^{1}$ is $2 a_{0}$ , since the second and third products have support in the indices $\geq 2$ . So $a$ contains no nonzero constant, giving $a_{0} = 0$ , and every element of $a_{1}$ lies in $(2)$ .

2.1L1L2L4L5step 1.1

The element $2 x$ lies in $a$ , is nonzero of degree $1$ and has leading coefficient $2$ , so $2 \in a_{1}$ ; with step 1.1 this gives $a_{1} = (2)$ . The element $x^{2} = 3 x^{2} - x \cdot (2 x)$ lies in $a$ , is nonzero of degree $2$ and has leading coefficient $1$ , so $1 \in a_{2}$ and $a_{2} = Z$ .

3.1L5step 2.1

The stages ascend, so $Z = a_{2} \subseteq a_{n} \subseteq Z$ and $a_{n} = Z$ for every $n \geq 2$ . The chain reads $0 ⊊ (2) ⊊ Z = Z = \dots$ and stabilises at $N = 2$ ; it does not stabilise at $N = 1$ , since $a_{1} = (2) \neq Z = a_{2}$ .

4.1L4L6L8L9step 3.1

Run the finite-generation lemma with $N = 2$ . Stage $0$ has $a_{0} = 0$ and contributes no realiser; stage $1$ has the single generator $2$ of $(2)$ , realised by $2 x$ ; stage $2$ has the single generator $1$ of $Z$ , realised by $x^{2}$ . So the lemma returns $a = (2 x, x^{2})$ . This is checkable by hand: $2 x$ and $x^{2}$ lie in $a$ by steps 1.1 and 2.1, while $3 x^{2} = 3 \cdot x^{2}$ and $x^{3} = x \cdot x^{2}$ lie in $(2 x, x^{2})$ .

5.1L2L7step 4.1

Take $f = 5 x^{4} + 2 x$ , which lies in $a$ because $5 x^{4} = 5 x^{2} \cdot x^{2}$ and $2 x$ do. It is nonzero of degree $d = 4$ with $lc (f) = 5 \in Z = a_{2}$ , so the cancellation lemma applies at $n = \min (4, 2) = 2$ with the single realiser $x^{2}$ and coefficient $r_{1} = 5$ : it forms $h = 5 x^{4 - 2} \cdot x^{2} = 5 x^{4}$ and leaves $f - h = 2 x$ , nonzero of degree $1 < 4$ . Applying it again to $2 x$ at $n = 1$ , with realiser $2 x$ and coefficient $r_{1} = 1$ , forms $h = 1 \cdot x^{0} \cdot 2 x = 2 x$ and leaves $0$ . Adding the two corrections back recovers $f = 5 x^{4} + 2 x$ as an element of $(2 x, x^{2})$ .

6.1L5L8L9step 5.1∎

The point of the example is the non-monic stage. At stage $1$ the ideal $a_{1} = (2)$ has no unit generator, so the degree- $1$ part of an element of $a$ cannot be cleared by dividing by a leading coefficient; the reduction has to express $lc (f)$ inside the stage ideal and use a realiser, which is exactly what steps 4.1 and 5.1 do. That $Z [x]$ is Noetherian at all is the Hilbert basis theorem applied to the Noetherian ring $Z$ .

Remarks

The generating list is not minimal by construction, and here it happens to be short. The lemma returns one realiser per generator of each stage up to $N$ ; a larger stabilisation index or a larger generating set of a stage would return a longer list generating the same ideal.
The original list is not the one the construction returns. The ideal was presented as $(2 x, 3 x^{2}, x^{3})$ and the construction returns $(2 x, x^{2})$ ; both generate $a$ , and step 4.1 checks the agreement directly rather than inferring it.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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

M. Hochster, Introduction to Commutative Algebra, Math 614, Theorem 5.6 (standard reference, not scraped)
B. Totaro, Commutative Algebra (Michaelmas 2011), notes by Z. Norwood, §8 Theorem 8.3 (standard reference, not scraped)

Working the Hilbert basis construction on an ideal of Z[x]Z[x] with non-monic stages