Euclidean reduction of subresultants

Adding a polynomial multiple of the right input to the left input preserves all fixed-bound subresultant minors, provided the multiplier fits the difference of the bounds. In particular, division with remainder preserves the minors before the bounds are lowered. The principal-coefficient recurrence then records the power of the leading coefficient and the sign introduced by lowering bounds and swapping inputs.

Reduction invariance holds over any commutative ring and at every index, including the terminal principal index. Division with remainder requires a field; the divisor and remainder may be zero. The principal-coefficient recurrences require the index to lie at or below both the remainder bound and the divisor degree. Strictly between the degree of the remainder and the degree of the divisor, the principal coefficients vanish. The polynomial subresultants also satisfy an exact Euclidean recurrence, with explicit endpoint multiples and vanishing inside degree gaps. For the signed principal coefficients, one step of the signed remainder sequence p, q, -(p % q) multiplies the coefficients at or below the remainder bound by a common factor independent of the index.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapters 4 and 8 (subresultants and polynomial remainder sequences).

theorem Polynomial.subresultantCoeff_add_mul_left {R : Type u_1} [CommRing R] {p q a : Polynomial R} {m n j : ℕ} (hp : p.natDegree ≤ m) (hq : q.natDegree ≤ n) (ha : a.natDegree + n ≤ m) (k : ℕ) : (p + a * q).subresultantCoeff q m n j k = p.subresultantCoeff q m n j k

Adding a multiple of the right input preserves every fixed-bound coefficient minor. The multiplier's degree plus the right bound must not exceed the left bound.

theorem Polynomial.psc_add_mul_left {R : Type u_1} [CommRing R] {p q a : Polynomial R} {m n j : ℕ} (hp : p.natDegree ≤ m) (hq : q.natDegree ≤ n) (ha : a.natDegree + n ≤ m) : (p + a * q).psc q m n j = p.psc q m n j

Polynomial reduction preserves principal coefficients, including the terminal index.

theorem Polynomial.subresultant_add_mul_left {R : Type u_1} [CommRing R] {p q a : Polynomial R} {m n j : ℕ} (hp : p.natDegree ≤ m) (hq : q.natDegree ≤ n) (ha : a.natDegree + n ≤ m) : (p + a * q).subresultant q m n j = p.subresultant q m n j

Polynomial reduction preserves the fixed-bound subresultant polynomial.

theorem Polynomial.subresultantCoeff_mod_left {K : Type u_2} [Field K] {p q : Polynomial K} {m j : ℕ} (hp : p.natDegree ≤ m) (k : ℕ) : (p % q).subresultantCoeff q m q.natDegree j k = p.subresultantCoeff q m q.natDegree j k

Division with remainder preserves coefficient minors at the original left bound and actual right degree. The left bound may be oversized, and the divisor and remainder may be zero.

theorem Polynomial.psc_mod_left {K : Type u_2} [Field K] {p q : Polynomial K} {m j : ℕ} (hp : p.natDegree ≤ m) : (p % q).psc q m q.natDegree j = p.psc q m q.natDegree j

Division with remainder preserves principal coefficients before the left bound drops.

theorem Polynomial.subresultant_mod_left {K : Type u_2} [Field K] {p q : Polynomial K} {m j : ℕ} (hp : p.natDegree ≤ m) : (p % q).subresultant q m q.natDegree j = p.subresultant q m q.natDegree j

Division with remainder preserves the subresultant polynomial at fixed bounds.

theorem Polynomial.psc_eq_sign_mul_leadingCoeff_pow_mul_psc_mod {K : Type u_2} [Field K] {p q : Polynomial K} {m r j : ℕ} (hp : p.natDegree ≤ m) (hr : (p % q).natDegree ≤ r) (hrm : r ≤ m) (hjr : j ≤ r) (hjq : j ≤ q.natDegree) : p.psc q m q.natDegree j = (-1) ^ ((m - j) * (q.natDegree - j)) * q.leadingCoeff ^ (m - r) * q.psc (p % q) q.natDegree r j

A Euclidean step for principal subresultant coefficients. Lowering the remainder's bound from m to r contributes q.leadingCoeff ^ (m - r); the displayed sign comes from both the bound drop and the input swap. The smaller terminal index, zero divisors, and zero remainders are included.

theorem Polynomial.psc_eq_sign_mul_leadingCoeff_pow_mul_psc_neg_mod {K : Type u_2} [Field K] {p q : Polynomial K} {m r j : ℕ} (hp : p.natDegree ≤ m) (hr : (p % q).natDegree ≤ r) (hrm : r ≤ m) (hjr : j ≤ r) (hjq : j ≤ q.natDegree) : p.psc q m q.natDegree j = (-1) ^ ((m - j + 1) * (q.natDegree - j)) * q.leadingCoeff ^ (m - r) * q.psc (-(p % q)) q.natDegree r j

The principal-coefficient recurrence for the signed remainder -(p % q). Negating the remainder adds the sign of its q.natDegree - j columns.

theorem Polynomial.psc_eq_zero_of_natDegree_mod_lt {K : Type u_2} [Field K] {p q : Polynomial K} {m j : ℕ} (hp : p.natDegree ≤ m) (hrj : (p % q).natDegree < j) (hjq : j < q.natDegree) (hjm : j ≤ m) : p.psc q m q.natDegree j = 0

Principal coefficients vanish at the indices strictly between the degree of the remainder p % q and the degree of q. The remainder may be zero.

theorem Polynomial.signedPsc_eq_mul_signedPsc_neg_mod {K : Type u_2} [Field K] {p q : Polynomial K} {m r j : ℕ} (hp : p.natDegree ≤ m) (hqm : q.natDegree ≤ m) (hr : (p % q).natDegree ≤ r) (hrm : r ≤ m) (hjr : j ≤ r) (hjq : j ≤ q.natDegree) : p.signedPsc q m q.natDegree j = (-1) ^ (m - q.natDegree).choose 2 * q.leadingCoeff ^ (m - r) * q.signedPsc (-(p % q)) q.natDegree r j

One step of the signed remainder sequence multiplies the signed principal coefficients by a common factor. For indices at most a bound r for the remainder, the signed coefficients of (p, q) are those of (q, -(p % q)) times (-1) ^ (m - q.natDegree).choose 2 * q.leadingCoeff ^ (m - r), which does not depend on the index.

theorem Polynomial.signedPsc_eq_zero_of_natDegree_mod_lt {K : Type u_2} [Field K] {p q : Polynomial K} {m j : ℕ} (hp : p.natDegree ≤ m) (hrj : (p % q).natDegree < j) (hjq : j < q.natDegree) (hjm : j ≤ m) : p.signedPsc q m q.natDegree j = 0

The signed principal coefficients vanish at the indices strictly between the degree of the remainder p % q and the degree of q.

One Euclidean step

theorem Polynomial.subresultant_eq_C_mul_subresultant_mod {K : Type u_2} [Field K] {p q : Polynomial K} {m r j : ℕ} (hp : p.natDegree ≤ m) (hr : (p % q).natDegree ≤ r) (hrm : r ≤ m) (hj : j < min r q.natDegree) : p.subresultant q m q.natDegree j = C ((-1) ^ ((m - j) * (q.natDegree - j)) * q.leadingCoeff ^ (m - r)) * q.subresultant (p % q) q.natDegree r j

A Euclidean step for subresultant polynomials. Below the remainder bound r, the subresultant of (p, q) is that of (q, p % q) times ± q.leadingCoeff ^ (m - r).

theorem Polynomial.subresultant_eq_C_mul_subresultant_neg_mod {K : Type u_2} [Field K] {p q : Polynomial K} {m r j : ℕ} (hp : p.natDegree ≤ m) (hr : (p % q).natDegree ≤ r) (hrm : r ≤ m) (hj : j < min r q.natDegree) : p.subresultant q m q.natDegree j = C ((-1) ^ ((m - j + 1) * (q.natDegree - j)) * q.leadingCoeff ^ (m - r)) * q.subresultant (-(p % q)) q.natDegree r j

The Euclidean step for the signed remainder -(p % q), the next entry of the signed remainder sequence. Negating the remainder adds the sign of its q.natDegree - j columns.

The degree gap

theorem Polynomial.subresultant_eq_C_mul_mod {K : Type u_2} [Field K] {p q : Polynomial K} {m j : ℕ} (hp : p.natDegree ≤ m) (hr : (p % q).natDegree ≤ j) (hjq : j < q.natDegree) (hjm : j < m) : p.subresultant q m q.natDegree j = C ((-1) ^ ((m - j) * (q.natDegree - j)) * q.leadingCoeff ^ (m - j) * (p % q).coeff j ^ (q.natDegree - j - 1)) * (p % q)

From the degree of the remainder up to q.natDegree - 1, the subresultant of (p, q) is an explicit multiple of the remainder p % q.

theorem Polynomial.subresultant_natDegree_sub_one {K : Type u_2} [Field K] {p q : Polynomial K} {m : ℕ} (hp : p.natDegree ≤ m) (hq : 0 < q.natDegree) (hqm : q.natDegree ≤ m) : p.subresultant q m q.natDegree (q.natDegree - 1) = C ((-q.leadingCoeff) ^ (m + 1 - q.natDegree)) * (p % q)

The subresultant at index q.natDegree - 1 is (-q.leadingCoeff) ^ (m + 1 - q.natDegree) times the remainder p % q.

theorem Polynomial.subresultant_eq_zero_of_degree_mod_lt {K : Type u_2} [Field K] {p q : Polynomial K} {m j : ℕ} (hp : p.natDegree ≤ m) (hr : (p % q).degree < ↑j) (hjq : j + 1 < q.natDegree) : p.subresultant q m q.natDegree j = 0

Strictly inside the degree gap, between the degree of the remainder and q.natDegree - 1, the subresultants of (p, q) vanish. This includes every index below q.natDegree - 1 when q divides p.