Gröbner bases¶
Fix a field \(K\) (\(\mathbb Q\), \(\mathbb Q(i)\) or \(\mathbb F_p\)), variables \(x_1 > \cdots > x_n\), and a monomial order \(\prec\) (Definition R-2).
Definition B-1. For an ideal \(I \subseteq K[x_1, \dots, x_n]\), a finite \(G = \{g_1, \dots, g_t\} \subseteq I\) is a Gröbner basis of \(I\) when the leading monomials of \(G\) generate the ideal of leading monomials of \(I\): \(\langle \operatorname{LM}(G) \rangle = \langle \operatorname{LM}(I) \rangle\). The S-polynomial of \(f\) and \(g\) is \(S(f, g) = \frac{L}{\operatorname{LT}(f)} f - \frac{L}{\operatorname{LT}(g)} g\) with \(L = \operatorname{lcm}(\operatorname{LM} f, \operatorname{LM} g)\).
Theorem B-2 (Buchberger's criterion, cited). \(G\) is a Gröbner basis of \(\langle G \rangle\) if and only if every S-polynomial \(S(g_i, g_j)\) has remainder \(0\) on division by \(G\) (Theorem V-4) [Buchberger 1965; Cox, Little and O'Shea 2015, ch. 2, §6, Theorem 6].
Theorem B-3 (Buchberger's algorithm, cited). Starting from the input generators, repeatedly adding nonzero remainders of S-polynomials terminates (by the ascending chain condition on monomial ideals, Dickson's lemma) with a Gröbner basis of the ideal generated by the inputs. The product and chain criteria of Gebauer and Möller skip S-pairs whose remainders are known to be \(0\), without affecting the result [Gebauer and Möller 1988; Cox, Little and O'Shea 2015, ch. 2, §§7–10].
Scheduling and reduction. Pair selection uses a binary heap ordered by LCM under the chosen monomial order, then by the two stable basis indices. This is exactly the earlier linear selector's total order. Installation applies the same pair criteria before rebuilding the heap, so its representation does not alter which S-polynomial is selected next. Basis polynomials are immutable after insertion; their leading monomials and leading-coefficient inverses can therefore be retained by index. The active reducer order is sorted after an insertion and reused until the next insertion. Initial generator reductions and cofactor propagation retain their established schedules.
F4. Over a prime field below \(2^{31}\), under GRLEX and GREVLEX and without cofactor tracking, the library runs F4 [Faugère 1999] instead of reducing one S-polynomial at a time. Each round takes every pending pair whose LCM has the least degree, writes both halves of each S-polynomial as rows of a sparse matrix, adds a row \(m \cdot g\) for every monomial of the matrix that a leading monomial divides (symbolic preprocessing), and row-reduces the matrix. A reduced row whose leading monomial no other row has is a polynomial of the ideal whose leading monomial no basis element divides, so it joins the basis. Pairs are pruned by the same Gebauer–Möller criteria, and when no pairs remain every S-polynomial has a standard representation in terms of the basis, which is Buchberger's criterion. The final interreduction is one more matrix. The reduced basis is unique (Theorem B-4), so F4 returns exactly the basis Buchberger's algorithm returns.
Rational bases under GREVLEX. Without cofactor tracking, a basis over \(\mathbb Q\) under GREVLEX is computed through the homogenized inputs. The generators become primitive integer polynomials \(F\) and, unless already homogeneous, are homogenized with a new variable \(h\), least in GREVLEX. Let \(J\) be the ideal of the homogenized generators \(F^h\) and \(I\) that of \(F\).
Dehomogenization. Let \(H\) be the reduced GREVLEX basis of \(J\). For \(f \in I\), some \(h^k f^h\) lies in \(J\); its leading monomial is that of \(f^h\) times \(h^k\), and under GREVLEX the leading monomial of \(f^h\) carries no \(h\). A leading monomial in \(H\) divides it, and setting \(h = 1\) in a homogeneous polynomial maps its leading monomial to the leading monomial of the image. So \(H|_{h=1}\) is a Gröbner basis of \(I\); dropping elements whose leading monomial another's divides and reducing the tails gives the reduced basis.
The library reconstructs \(H\) from the reduced bases \(H_p\) of the images \(J_p\) modulo primes below \(2^{31}\), computed by F4, by Chinese remaindering and rational reconstruction, and accepts a candidate \(G\) only with a certificate:
Theorem B-4a (certified reconstruction). Let \(G\) be a set of homogeneous monic polynomials with rational coefficients such that (a) every element of \(F^h\) reduces to zero modulo \(G\); (b) every S-pair of \(G\) kept by the Gebauer–Möller criteria reduces to zero modulo \(G\); (c) the leading monomials of \(G\) are those of some set \(H_p \subseteq J_p\) for a prime \(p\); and (d) no tail monomial of an element of \(G\) is divisible by a leading monomial of \(G\). Then \(G\) is the reduced basis of \(J\).
Proof. By (b), \(G\) is a Gröbner basis of \(\langle G\rangle\), so \(\dim \langle G \rangle_d = c_d\), the number of degree-\(d\) monomials in the ideal of its leading monomials. By (a), \(J \subseteq \langle G \rangle\). By (c), \(c_d\) monomials of degree \(d\) are leading monomials of elements of \(J_p\), so \(\dim (J_p)_d \ge c_d\). And \((J_p)_d\) is spanned by the rows of the Macaulay matrix of \(J_d\) reduced modulo \(p\), and reducing an integer matrix modulo \(p\) cannot raise its rank, so \(\dim (J_p)_d \le \dim J_d\). Hence \(c_d \le \dim J_d \le \dim \langle G\rangle_d = c_d\) in every degree, so \(J = \langle G \rangle\), and with (d) and monicity \(G\) is its reduced basis (Theorem B-4). \(\square\)
The checks (a), (b), and (d) are exact computations over the integers; (c) holds by construction. After the first prime, an image replays the matrices of the first F4 run, reducing only the rows that gave new elements; its elements are still combinations of multiples of the generators modulo \(p\), so they lie in \(J_p\) whether or not the replay found its reduced basis. For (b) the S-polynomials of each degree are reduced in one F4 matrix over the integers, fraction-free: reducing an S-polynomial to zero by any choice of reducers gives it a standard representation. The theorem does not require \(p\) to be a lucky prime [Arnold 2003]: an unlucky image can only delay certification. If reconstruction or certification gives up, \(J\) is computed exactly instead, by fraction-free Buchberger, which proceeds degree by degree on homogeneous input and so avoids most intermediate coefficient growth.
Theorem B-4 (reduced bases, cited). Every ideal has exactly one reduced Gröbner basis for a given order: monic, and with no monomial of any element divisible by the leading monomial of another [Cox, Little and O'Shea 2015, ch. 2, §7, Proposition 6].
Theorem B-5 (membership). If \(G\) is a Gröbner basis of \(I\), then \(f \in I\) if and only if the remainder of \(f\) on division by \(G\) is \(0\) [Cox, Little and O'Shea 2015, ch. 2, §6, Corollary 2].
Cofactors¶
Proposition B-6 (cofactor tracking). Let the inputs be \(f_1, \dots, f_s\). If Buchberger's algorithm records, for every basis element \(g\), polynomials \(c_{g,1}, \dots, c_{g,s}\) with \(g = \sum_k c_{g,k} f_k\), updating them at each S-polynomial and each reduction step by the same linear combinations it applies to \(g\), the invariant holds throughout; then a division of \(f\) by \(G\) with remainder \(0\), \(f = \sum_g a_g g\), yields \(f = \sum_k \big(\sum_g a_g c_{g,k}\big) f_k\).
Proof. The inputs satisfy the invariant with unit vectors. An S-polynomial and a reduction step form \(K[x]\)-linear combinations of elements that satisfy it, and applying the same combinations to their cofactor vectors preserves it. Substituting the cofactor expressions into the division identity gives the last equation. \(\square\)
Cofactors can grow much larger than the basis; tracking is optional, and is switched on only when a membership certificate is wanted.
Certificate B-C1 (ideal membership). Data: \(h_1, \dots, h_s\). Check: \(f = \sum_k h_k f_k\). Claim: \(f \in \langle f_1, \dots, f_s \rangle\).
Theorem B-7 (what membership certificates prove). Let
\(f = \sum_k h_k f_k\) hold as polynomials with rational coefficients. Then,
in the scalar carrier, for every assignment of finite values to the
variables at which \(f_1, \dots, f_s\) all vanish, \(f\) vanishes. In
particular, if \(f = 1\), the polynomials \(f_k\) have no common zero among
finite values (a Nullstellensatz certificate of infeasibility).
Proof. Evaluation at finite values is a ring homomorphism into \(\mathbb C\) (Theorem P-2 of the kernel's theory). \(\square\)
This is how Gröbner bases serve proofs: the algorithm finds the cofactors, and the kernel checks one polynomial identity.
For QQi, B-2 through B-6 apply unchanged because \(\mathbb Q(i)\) is a field (Definition R-1a). Evaluating a B-C1 identity under its embedding in \(\mathbb C\) proves the same vanishing implication for complex assignments; in particular, a witness for \(1\) proves the absence of a common complex zero. The library checks this identity exactly. The current kernel polynomial encoding remains rational-only, so this extension does not supply a kernel rule or encoding for complex coefficient certificates.