The first nonzero subresultant polynomial

Subresultant polynomials vanish below the degree of any common divisor. At the degree of a monic common divisor, the subresultant is that divisor multiplied by its principal coefficient. Over a field, the first nonzero subresultant polynomial therefore recovers the monic gcd, with its scalar fixed by the determinant convention. This identifies the terminal polynomial in comparisons of subresultants with Euclidean remainder sequences.

The polynomial identification requires a strict index: when the gcd degree equals the smaller input degree, the terminal principal coefficient is scalar data, not a subresultant polynomial. Formal degree bounds are retained throughout; the nonvanishing assertion uses an actual left degree and a right degree bound, as in the principal-coefficient gcd criterion.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 4, Proposition 4.25 and Corollary 4.26 (subresultants and the gcd).

theorem Polynomial.subresultant_eq_zero_of_lt_natDegree_commonDivisor {R : Type u_1} [CommRing R] [IsDomain R] {p q g : Polynomial R} {m n j : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hgp : g ∣ p) (hgq : g ∣ q) (hj : j < g.natDegree) : p.subresultant q m n j = 0

Subresultant polynomials vanish below the degree of any common divisor, even when their formal degree bounds exceed the input degrees.

theorem Polynomial.subresultant_eq_C_mul_of_monic_commonDivisor {R : Type u_1} [CommRing R] {p q g : Polynomial R} {m n : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hg : g.Monic) (hgp : g ∣ p) (hgq : g ∣ q) (hj : g.natDegree < min m n) : p.subresultant q m n g.natDegree = C (p.psc q m n g.natDegree) * g

At the degree of a monic common divisor, a strict-index subresultant polynomial is exactly that divisor scaled by the principal subresultant coefficient. The scalar is allowed to vanish. No field hypothesis or actual-degree equality is required.

theorem Polynomial.subresultant_natDegree_gcd {K : Type u_1} [Field K] [DecidableEq K] {p q : Polynomial K} {m n : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hj : (EuclideanDomain.gcd p q).natDegree < min m n) : p.subresultant q m n (EuclideanDomain.gcd p q).natDegree = C (p.psc q m n (EuclideanDomain.gcd p q).natDegree) * normalize (EuclideanDomain.gcd p q)

At the gcd degree, a strict-index subresultant is the monic normalization of the Euclidean gcd scaled by its principal coefficient. This formula also permits oversized formal bounds, where that coefficient can vanish.

theorem Polynomial.subresultant_natDegree_gcd_associated {K : Type u_1} [Field K] [DecidableEq K] {p q : Polynomial K} {m n : ℕ} (hm : p.natDegree = m) (hn : q.natDegree ≤ n) (hj : (EuclideanDomain.gcd p q).natDegree < min m n) : Associated (p.subresultant q m n (EuclideanDomain.gcd p q).natDegree) (EuclideanDomain.gcd p q)

With an actual left degree, the subresultant at a strict gcd index is associated to the gcd. Together with vanishing below that index, this identifies the first nonzero subresultant polynomial. A right degree bound suffices; neither squarefreeness nor monicity is assumed.