Degree drops in subresultant polynomials

Below the smaller degree bounds, lowering a bound scales the entire subresultant polynomial, not just its principal coefficient. At a smaller terminal bound, the surviving polynomial is instead a scalar multiple of the corresponding input. Thus terminal scalar data must not be replaced by the zero polynomial used outside the strict subresultant range.

The coefficient-minor formulas retain formal bounds and hold over arbitrary commutative rings. The specialization formulas use reducta taken before mapping coefficients, allowing degree drops and zero fibers. These identities supply the specialization laws for comparisons with polynomial remainder sequences.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 4 (specialization of subresultants).

theorem Polynomial.subresultant_eq_C_coeff_pow_mul_of_right_degree_drop {R : Type u_1} [CommRing R] {p q : Polynomial R} {m n N j : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hN : n ≤ N) (hj : j < min m n) : p.subresultant q m N j = C (p.coeff m ^ (N - n)) * p.subresultant q m n j

Below both smaller bounds, an arbitrary right-bound drop scales the whole subresultant polynomial. The formula does not replace a terminal scalar minor by a polynomial.

theorem Polynomial.subresultant_eq_C_sign_mul_coeff_pow_mul_of_left_degree_drop {R : Type u_1} [CommRing R] {p q : Polynomial R} {m M n j : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hM : m ≤ M) (hj : j < min m n) : p.subresultant q M n j = C ((-1) ^ ((M - m) * (n - j)) * q.coeff n ^ (M - m)) * p.subresultant q m n j

Below both smaller bounds, a left-bound drop scales the whole subresultant polynomial, including the column-block sign.

@[simp]

theorem Polynomial.subresultant_right_bound_of_degree_drop {R : Type u_1} [CommRing R] {p q : Polynomial R} {m n N : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hnm : n < m) (hnN : n < N) : p.subresultant q m N n = C (p.coeff m ^ (N - n) * q.coeff n ^ (m - n - 1)) * q

When only the right bound drops, the subresultant at its smaller terminal index survives as a scalar multiple of the right polynomial, rather than a terminal subresultant polynomial.

@[simp]

theorem Polynomial.subresultant_left_bound_of_degree_drop {R : Type u_1} [CommRing R] {p q : Polynomial R} {m M n : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hmn : m < n) (hmM : m < M) : p.subresultant q M n m = C ((-1) ^ ((M - m) * (n - m)) * q.coeff n ^ (M - m) * p.coeff m ^ (n - m - 1)) * p

The smaller left terminal index likewise survives as a scalar multiple of the left input, with the sign from swapping the formal column blocks.

@[simp]

theorem Polynomial.subresultant_eq_zero_of_natDegree_lt_bounds {R : Type u_1} [CommRing R] {p q : Polynomial R} {m n j : ℕ} (hm : p.natDegree < m) (hn : q.natDegree < n) : p.subresultant q m n j = 0

Dropping both formal bounds forces every subresultant polynomial to vanish, not merely its principal coefficient. Outside the strict range the polynomial is zero by convention.

theorem Polynomial.map_subresultant_of_right_degree_drop {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) {p q : Polynomial R} {m n N j : ℕ} (hm : (map f p).natDegree ≤ m) (hn : (map f q).natDegree ≤ n) (hN : n ≤ N) (hj : j < min m n) : map f (p.subresultant q m N j) = C (f (p.coeff m) ^ (N - n)) * (map f p).subresultant (map f (q.reductum (n + 1))) m n j

After specialization, a right-bound drop below the smaller bounds scales the mapped subresultant. The reduced input is obtained by truncating before mapping.

theorem Polynomial.map_subresultant_of_left_degree_drop {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) {p q : Polynomial R} {m M n j : ℕ} (hm : (map f p).natDegree ≤ m) (hn : (map f q).natDegree ≤ n) (hM : m ≤ M) (hj : j < min m n) : map f (p.subresultant q M n j) = C ((-1) ^ ((M - m) * (n - j)) * f (q.coeff n) ^ (M - m)) * (map f (p.reductum (m + 1))).subresultant (map f q) m n j

The left-bound specialization formula retains the column-block sign and the right coefficient power, with truncation before mapping.