The subresultant gcd criterion

Over a field, the principal subresultant coefficients of two polynomials locate the degree of their greatest common divisor: taken at the actual degree of the nonzero left polynomial and at any bound dominating the degree of the right one, they vanish at every index below the degree of the gcd and are nonzero at that degree. Hence, at the actual degrees of any two polynomials, the degree of the gcd is the least index with a nonzero principal subresultant coefficient.

Both halves read the principal subresultant matrix as the linear map (A, B) ↦ A * q + B * p on polynomials of bounded degree, through Polynomial.subresultantMatrix_mulVec. A common factor of degree d > j supplies the kernel vector (p / g, -(q / g)) at index j; at index d, a kernel vector is a relation A * q + B * p = 0 whose degrees are too small for a nonzero solution, by the Bézout identity for the gcd.

Main results

• Polynomial.psc_eq_zero_of_mul_add_mul_eq_zero: a nontrivial relation A * q + B * p = 0 with A and B of degrees below m - j and n - j forces the principal coefficient at j to vanish.
• Polynomial.psc_eq_zero_of_lt_natDegree_gcd: the principal coefficients vanish below the degree of the gcd.
• Polynomial.psc_natDegree_gcd_ne_zero: the principal coefficient at the degree of the gcd is nonzero.
• Polynomial.natDegree_gcd_eq_iff_psc: the degree of the gcd is the least index with a nonzero principal subresultant coefficient.
• Polynomial.natDegree_gcd_eq_of_psc_eq_zero_iff: two pairs of polynomials whose principal subresultant coefficients vanish at the same indices have gcds of the same degree.

References

• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 4, Proposition 4.25 and Corollary 4.26.
• Q. Vermande, Cylindrical Algebraic Decomposition in Coq/Rocq, §3.

theorem Polynomial.psc_eq_zero_of_mul_add_mul_eq_zero {R : Type u_1} [CommRing R] [IsDomain R] {p q A B : Polynomial R} {m n j : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hA : A.degree < ↑(m - j)) (hB : B.degree < ↑(n - j)) (hAB : A * q + B * p = 0) (hne : A ≠ 0 ∨ B ≠ 0) : p.psc q m n j = 0

A nontrivial relation A * q + B * p = 0, with A and B of degrees below m - j and n - j, is a kernel vector of the principal subresultant matrix at index j, so the principal subresultant coefficient vanishes there.

theorem Polynomial.psc_eq_zero_of_lt_natDegree_gcd {K : Type u_1} [Field K] [DecidableEq K] {p q : Polynomial K} {m n j : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hj : j < (EuclideanDomain.gcd p q).natDegree) : p.psc q m n j = 0

Below the degree of the gcd, the principal subresultant coefficients vanish, at any formal degree bounds dominating the actual degrees.

theorem Polynomial.psc_natDegree_gcd_ne_zero {K : Type u_1} [Field K] [DecidableEq K] {p q : Polynomial K} {m n : ℕ} (hp : p ≠ 0) (hm : p.natDegree = m) (hn : q.natDegree ≤ n) : p.psc q m n (EuclideanDomain.gcd p q).natDegree ≠ 0

At the degree of the gcd, the principal subresultant coefficient is nonzero, provided the left bound is the actual degree of the nonzero left polynomial and the right bound dominates the degree of the right polynomial.

theorem Polynomial.natDegree_gcd_eq_iff_psc {K : Type u_1} [Field K] [DecidableEq K] (p q : Polynomial K) (j : ℕ) : (EuclideanDomain.gcd p q).natDegree = j ↔ p.psc q p.natDegree q.natDegree j ≠ 0 ∧ ∀ i < j, p.psc q p.natDegree q.natDegree i = 0

The subresultant gcd criterion: at the actual degrees, the degree of the gcd of p and q is the least index with nonzero principal subresultant coefficient. When p = 0, the gcd is q and the criterion reads off the empty terminal determinant at q.natDegree.

theorem Polynomial.natDegree_gcd_eq_of_psc_eq_zero_iff {K : Type u_1} [Field K] [DecidableEq K] {L : Type u_2} [Field L] [DecidableEq L] {p q : Polynomial K} {p' q' : Polynomial L} (hp' : p' ≠ 0) (hq' : q' ≠ 0) (h : ∀ j ≤ min p'.natDegree q'.natDegree, p.psc q p.natDegree q.natDegree j = 0 ↔ p'.psc q' p'.natDegree q'.natDegree j = 0) : (EuclideanDomain.gcd p q).natDegree = (EuclideanDomain.gcd p' q').natDegree

The degree of the gcd is determined by which principal subresultant coefficients vanish, at the actual degrees and at indices up to the smaller degree. If the coefficients of a pair p', q' of nonzero polynomials vanish exactly where those of p, q do, the two gcds have the same degree; the two pairs may live over different fields.