Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 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.

Reducing f modulo gi(xi)=∏s∈Si(xi−s) lowers each deg⁡xi below ∣Si∣, preserves the values on the grid, and preserves any top-degree coefficient whose exponents stay below the grid sizes

Statement

Let F be a field, let f∈F[x1,…,xn], and let finite nonempty sets S1,…,Sn⊆F. Put

gi(xi):=∏s∈Si(xi−s).

Then there is a polynomial f~∈F[x1,…,xn] such that:

  1. either f~=0, or deg⁡xif~<∣Si∣ for every i and deg⁡f~≤deg⁡f;
  2. f~(a)=f(a) for every a∈S1×⋯×Sn;
  3. if deg⁡f=∑iti and the monomial x1t1⋯xntn has top total degree with each ti<∣Si∣, then [x1t1⋯xntn]f~=[x1t1⋯xntn]f.

Facts & Assumptions

Given: a field F, finite nonempty subsets S1,…,Sn⊆F, and a polynomial f∈F[x1,…,xn].

[F1]

The total degree and the separate degrees are taken from the monomial expansion (Monomials, coefficients, degree in each variable and total degree in F[x1,…,xn]).

[F2]

Division by a monic polynomial in one variable over a commutative ring gives a quotient and remainder with smaller degree in that variable (Division by a monic polynomial over a commutative ring).

[F3]

For every s∈Si, the factor s−s appears in ∏t∈Si(s−t), so gi(s)=0.

Proof

technique · direct
1.1F1F2construct

Set r(0):=f. For each i=1,…,n, view r(i−1) as a polynomial in xi with coefficients in F[x1,…,xi−1,xi+1,…,xn]. Since gi is monic of degree ∣Si∣, [F2] gives r(i−1)=qigi+r(i) with r(i)=0 or deg⁡xir(i)<∣Si∣. Because gi involves only xi, this subtraction leaves all previously obtained bounds deg⁡xj<∣Sj∣ for j<i unchanged; and every nonleading term of gi has smaller xi-degree than its leading term, so the division step introduces no monomial of larger total degree. Therefore f~:=r(n) satisfies part 1.

2.1F3step 1.1

Let a=(a1,…,an)∈S1×⋯×Sn. For each i, step 1.1 gives r(i−1)−r(i)=qigi, and [F3] gives gi(ai)=0 because ai∈Si. Hence r(i−1)(a)=r(i)(a) for every i, so chaining these equalities yields f~(a)=f(a).

3.1step 1.1∎

In the situation of part 3, fix a stage i. Any monomial of total degree deg⁡f in qigi must use the leading term xi∣Si∣ of gi, because every other term of gi has smaller total degree. So every top-degree monomial of qigi has xi-exponent at least ∣Si∣. Since the target monomial has exponent ti<∣Si∣ for every i, no stage changes its coefficient. Therefore [x1t1⋯xntn]f~=[x1t1⋯xntn]f.

Remarks

  • Part 3 is the clause that the Nullstellensatz actually uses. The degree reduction and grid agreement alone do not see the top coefficient.

Depends on

Used by

Dependency tree · two levels

13 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