The structure theorem for subresultants

Let p and q be polynomials over a field, with q of degree n, and let p, q, -(p % q), … be their signed remainder sequence Polynomial.sturmSeq p q. The subresultant polynomials of p and q are determined, up to nonzero scalars, by this sequence. For consecutive entries s and t after the first:

• the subresultant at index deg s - 1 is a nonzero multiple of t;
• the subresultant at index deg t is a nonzero multiple of t;
• the subresultants at the indices strictly between deg t and deg s - 1 vanish.

The two indices coincide unless the degree drops by more than one from s to t; in that case the indices between them form a degree gap. Together with the vanishing of all subresultants below the degree of the last entry, which divides p and q (TauCeti.getLast?_sturmSeq_dvd and Polynomial.subresultant_eq_zero_of_lt_natDegree_commonDivisor), this determines every subresultant polynomial of p and q at an index below n, up to nonzero scalars. The left input is taken at a formal bound m dominating its degree, as in the rest of the subresultant API, and the first two statements need n ≤ m only for the initial pair; the right input is taken at its actual degree.

The one-step Euclidean recurrence and degree-gap identities are in TauCeti.RingTheory.Polynomial.Subresultant.Euclidean. The exact transport factors and endpoint scalars are in TauCeti.RingTheory.Polynomial.Subresultant.Scaling; the existential statements here follow from those formulas and factor nonvanishing. Degree-gap vanishing also follows from exact transport and the one-step vanishing identity.

Main results

• Polynomial.exists_subresultant_eq_C_mul_subresultant_of_getElem?_sturmSeq: the subresultants of p and q are nonzero multiples of those of any two consecutive later entries of the signed remainder sequence.
• Polynomial.exists_subresultant_natDegree_sub_one_eq_C_mul_of_getElem?_sturmSeq, Polynomial.exists_subresultant_natDegree_eq_C_mul_of_getElem?_sturmSeq, Polynomial.subresultant_eq_zero_of_getElem?_sturmSeq: the structure theorem.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 8 (the structure theorem for subresultants and signed remainder sequences).

Along the signed remainder sequence

theorem Polynomial.exists_subresultant_eq_C_mul_subresultant_of_getElem?_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {p q a b : Polynomial K} {m i j : ℕ} (hp : p.natDegree ≤ m) (ha : (p.sturmSeq q)[i + 1]? = some a) (hb : (p.sturmSeq q)[i + 2]? = some b) (hj : j < b.natDegree) : ∃ (c : K), c ≠ 0 ∧ p.subresultant q m q.natDegree j = C c * a.subresultant b a.natDegree b.natDegree j

The subresultants of p and q are nonzero multiples of those of any two consecutive entries a, b of the signed remainder sequence after the first, each taken at its actual degree, at every index below the degree of b.

theorem Polynomial.exists_subresultant_natDegree_sub_one_eq_C_mul_of_getElem?_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {p q s t : Polynomial K} {m i : ℕ} (hp : p.natDegree ≤ m) (hq : i = 0 → q.natDegree ≤ m) (hs : (p.sturmSeq q)[i + 1]? = some s) (ht : (p.sturmSeq q)[i + 2]? = some t) : ∃ (c : K), c ≠ 0 ∧ p.subresultant q m q.natDegree (s.natDegree - 1) = C c * t

Structure theorem for subresultants, upper index. For consecutive entries s, t of the signed remainder sequence of p and q after the first, the subresultant of p and q at index deg s - 1 is a nonzero multiple of t. Only the initial pair additionally requires q.natDegree ≤ m.

theorem Polynomial.exists_subresultant_natDegree_eq_C_mul_of_getElem?_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {p q s t : Polynomial K} {m i : ℕ} (hp : p.natDegree ≤ m) (hq : i = 0 → q.natDegree ≤ m) (hs : (p.sturmSeq q)[i + 1]? = some s) (ht : (p.sturmSeq q)[i + 2]? = some t) : ∃ (c : K), c ≠ 0 ∧ p.subresultant q m q.natDegree t.natDegree = C c * t

Structure theorem for subresultants, lower index. For consecutive entries s, t of the signed remainder sequence of p and q after the first, the subresultant of p and q at index deg t is a nonzero multiple of t. Only the initial pair additionally requires q.natDegree ≤ m.

theorem Polynomial.subresultant_eq_zero_of_getElem?_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {p q s t : Polynomial K} {m i j : ℕ} (hp : p.natDegree ≤ m) (hs : (p.sturmSeq q)[i + 1]? = some s) (ht : (p.sturmSeq q)[i + 2]? = some t) (htj : t.natDegree < j) (hjs : j + 1 < s.natDegree) : p.subresultant q m q.natDegree j = 0

Structure theorem for subresultants, degree gap. For consecutive entries s, t of the signed remainder sequence of p and q after the first, the subresultants of p and q at the indices strictly between deg t and deg s - 1 vanish.