Degree drops in subresultant coefficient minors

Fixed-bound principal subresultants need not equal the principal subresultants computed at smaller actual degrees. Lowering the right bound contributes a power of the coefficient at the left bound; lowering the left bound also contributes a block-order sign. The coefficient-minor identities specialize to principal coefficients, including their terminal cases. These identities explain how specialization interacts with degree drops, without assuming nonvanishing of specialized leading coefficients.

References

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

theorem Polynomial.subresultantCoeff_succ_right {R : Type u_1} [CommRing R] {p q : Polynomial R} {m n j : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hjm : j < m) (hjn : j ≤ n) (k : ℕ) : p.subresultantCoeff q m (n + 1) j k = p.coeff m * p.subresultantCoeff q m n j k

Lowering an oversized right bound by one scales every coefficient minor by the coefficient at the left bound. The smaller right terminal index is included, but j < m is essential.

theorem Polynomial.subresultantCoeff_eq_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) (hjm : j < m) (hjn : j ≤ n) (k : ℕ) : p.subresultantCoeff q m N j k = p.coeff m ^ (N - n) * p.subresultantCoeff q m n j k

Lowering an oversized right bound scales every coefficient minor by the corresponding power of the coefficient at the left bound, including the smaller right terminal index.

theorem Polynomial.subresultantCoeff_eq_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) (hjm : j ≤ m) (hjn : j < n) (k : ℕ) : p.subresultantCoeff q M n j k = (-1) ^ ((M - m) * (n - j)) * q.coeff n ^ (M - m) * p.subresultantCoeff q m n j k

Lowering an oversized left bound scales coefficient minors by the right coefficient power and the column-block sign. The smaller left terminal index is included.

theorem Polynomial.psc_eq_coeff_pow_mul_of_right_degree_drop {R : Type u_1} [CommRing R] {p q : Polynomial R} {m n N j : ℕ} (hn : q.natDegree ≤ n) (hN : n ≤ N) (hjm : j ≤ m) (hjn : j ≤ n) : p.psc q m N j = p.coeff m ^ (N - n) * p.psc q m n j

An arbitrary drop in the right bound contributes the corresponding power of the coefficient at the left bound. The lower right bound need only dominate the degree; the left input is truncated to its formal bound, so no degree bound on it is needed.

theorem Polynomial.psc_succ_right {R : Type u_1} [CommRing R] {p q : Polynomial R} {m n j : ℕ} (hn : q.natDegree ≤ n) (hjm : j ≤ m) (hjn : j ≤ n) : p.psc q m (n + 1) j = p.coeff m * p.psc q m n j

Lowering an oversized right degree bound by one multiplies the principal subresultant by the coefficient at the left bound. The terminal smaller index is included.

theorem Polynomial.psc_eq_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) (hjm : j ≤ m) (hjn : j ≤ n) : p.psc q M n j = (-1) ^ ((M - m) * (n - j)) * q.coeff n ^ (M - m) * p.psc q m n j

Dropping the left bound also contributes the sign of moving its removed columns past the right block. The lower left bound need only dominate the degree.

theorem Polynomial.psc_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) (hj : j < min m n) : p.psc q m n j = 0

At strict subresultant indices, simultaneous drops in both degree bounds force vanishing. Terminal indices are excluded: their empty determinant can still be 1.

theorem Polynomial.map_psc_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 : ℕ} (hn : (map f q).natDegree ≤ n) (hN : n ≤ N) (hjm : j ≤ m) (hjn : j ≤ n) : f (p.psc q m N j) = f (p.coeff m) ^ (N - n) * (map f p).psc (map f (q.reductum (n + 1))) m n j

After coefficient specialization, lowering the right bound amounts to truncating that input and multiplying by a power of the specialized coefficient at the left bound. In particular, the lower bound can be the actual degree of the specialized right input.

theorem Polynomial.map_psc_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) (hjm : j ≤ m) (hjn : j ≤ n) : f (p.psc q M n j) = (-1) ^ ((M - m) * (n - j)) * f (q.coeff n) ^ (M - m) * (map f (p.reductum (m + 1))).psc (map f q) m n j

The left-bound specialization formula retains the column-block sign as well as the power of the specialized coefficient at the right bound. Truncation occurs before mapping.