Signed principal subresultant coefficients

The signed principal coefficients used in real-root counting differ from the Sylvester principal minors by a degree-dependent sign. Polynomial.signedPsc records this normalization, including the leading coefficients above the smaller formal bound. Polynomial.signedPsc_def gives the full Sylvester–Habicht sign conversion; its two binomial terms and column-block sign simplify to (-1) ^ (m - j).choose 2.

The degree-drop identities retain the formal bounds and include the smaller terminal index. Mapping coefficients commutes with the signed coefficients without a degree-preservation assumption at fixed bounds, and at the actual degrees when the map preserves both degrees. The specialization formulas use reducta taken before mapping, so they can be used with nullified leading terms. These are the scalar coefficients for permanences-minus-variations formulas.

References

• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 4 (Sylvester–Habicht normalization).
• Q. Vermande, Cylindrical Algebraic Decomposition in Coq/Rocq, §3 (subresultantE uses the signed normalization).

noncomputable def Polynomial.signedPsc {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j : ℕ) : R

Signed principal subresultant coefficients at fixed bounds. Inside the subresultant range they are signed Sylvester minors. Above that range the coefficients at the two input bounds are retained, and all other entries vanish. The equal-bound terminal entry is 1, including for zero inputs.

theorem Polynomial.signedPsc_def {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j : ℕ) : p.signedPsc q m n j = if j ≤ min m n then (-1) ^ ((m + n - 2 * j).choose 2 + (n - j).choose 2 + (m - j) * (n - j)) * p.psc q m n j else if j = m then p.coeff m else if j = n then q.coeff n else 0

Conversion from the Sylvester convention to the signed Sylvester–Habicht normalization. The last exponent accounts for swapping the column blocks.

@[simp]

theorem Polynomial.signedPsc_of_le {R : Type u_1} [CommRing R] (p q : Polynomial R) {m n j : ℕ} (hj : j ≤ min m n) : p.signedPsc q m n j = (-1) ^ (m - j).choose 2 * p.psc q m n j

Within the subresultant range only the left-bound gap determines the sign.

@[simp]

theorem Polynomial.signedPsc_of_lt {R : Type u_1} [CommRing R] (p q : Polynomial R) {m n j : ℕ} (hj : min m n < j) : p.signedPsc q m n j = if j = m then p.coeff m else if j = n then q.coeff n else 0

Above the smaller bound only the two input-bound coefficients are retained.

@[simp]

theorem Polynomial.signedPsc_eq_zero_of_max_lt {R : Type u_1} [CommRing R] (p q : Polynomial R) {m n j : ℕ} (hj : max m n < j) : p.signedPsc q m n j = 0

Coefficients beyond both formal bounds vanish.

@[simp]

theorem Polynomial.signedPsc_map_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (p q : Polynomial R) (m n j : ℕ) : (map f p).signedPsc (map f q) m n j = f (p.signedPsc q m n j)

Signed coefficients specialize at fixed bounds, even when degrees drop.

theorem Polynomial.signedPsc_map_of_natDegree_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {p q : Polynomial R} (hp : (map f p).natDegree = p.natDegree) (hq : (map f q).natDegree = q.natDegree) (j : ℕ) : (map f p).signedPsc (map f q) (map f p).natDegree (map f q).natDegree j = f (p.signedPsc q p.natDegree q.natDegree j)

At the actual degrees, signed coefficients commute with a coefficient map that preserves both degrees, for instance one that does not kill the leading coefficients (Polynomial.natDegree_map_of_leadingCoeff_ne_zero). When a degree drops, Polynomial.map_signedPsc_of_right_degree_drop and Polynomial.map_signedPsc_of_left_degree_drop apply instead.

@[simp]

theorem Polynomial.signedPsc_left_bound {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n : ℕ) : p.signedPsc q m n m = if m ≤ n then p.coeff m ^ (n - m) else p.coeff m

The smaller left bound has no sign correction; a larger left bound retains the left input coefficient itself.

@[simp]

theorem Polynomial.signedPsc_right_bound {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n : ℕ) : p.signedPsc q m n n = if n ≤ m then (-1) ^ (m - n).choose 2 * q.coeff n ^ (m - n) else q.coeff n

The smaller right bound retains the gap sign and the terminal power; a larger right bound retains the right input coefficient itself.

theorem Polynomial.signedPsc_comm {R : Type u_1} [CommRing R] (p q : Polynomial R) {m n j : ℕ} : p.signedPsc q m n j = (-1) ^ ((m - j).choose 2 + (n - j).choose 2 + (m - j) * (n - j)) * q.signedPsc p n m j

Swapping inputs changes both the normalization and the column-block order.

theorem Polynomial.signedPsc_C_mul_left {R : Type u_1} [CommRing R] (p q : Polynomial R) (r : R) {m n j : ℕ} (hj : j ≤ min m n) : (C r * p).signedPsc q m n j = r ^ (n - j) * p.signedPsc q m n j

Scaling the left input scales its signed minor by the number of its columns.

theorem Polynomial.signedPsc_C_mul_right {R : Type u_1} [CommRing R] (p q : Polynomial R) (r : R) {m n j : ℕ} (hj : j ≤ min m n) : p.signedPsc (C r * q) m n j = r ^ (m - j) * p.signedPsc q m n j

Scaling the right input scales its signed minor by the number of its columns.

@[simp]

theorem Polynomial.signedPsc_zero_left {R : Type u_1} [CommRing R] (q : Polynomial R) {m n j : ℕ} (hjn : j < n) : signedPsc 0 q m n j = 0

A zero left input makes a signed minor vanish when its column block is nonempty (j < n). This excludes the empty-determinant terminal case.

@[simp]

theorem Polynomial.signedPsc_zero_right {R : Type u_1} [CommRing R] (p : Polynomial R) {m n j : ℕ} (hjm : j < m) : p.signedPsc 0 m n j = 0

A zero right input makes a signed minor vanish when its column block is nonempty (j < m). This excludes the empty-determinant terminal case.

theorem Polynomial.signedPsc_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.signedPsc q m N j = p.coeff m ^ (N - n) * p.signedPsc q m n j

Lowering the right bound contributes a power of the coefficient at the left formal bound, with no additional sign. The smaller terminal index is included.

theorem Polynomial.signedPsc_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.signedPsc q M n j = (-1) ^ ((M - m).choose 2 + (M - m) * (m + n - 2 * j)) * q.coeff n ^ (M - m) * p.signedPsc q m n j

Lowering the left bound contributes the normalization-gap sign as well as the power of the coefficient at the right bound. Terminal indices are included.

theorem Polynomial.signedPsc_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.signedPsc q m n j = 0

Simultaneous strict degree drops make every strict-index signed minor zero. The equal-bound terminal determinant is deliberately excluded.

theorem Polynomial.map_signedPsc_of_right_degree_drop {R : Type u_1} {S : Type u_2} [CommRing R] [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.signedPsc q m N j) = f (p.coeff m) ^ (N - n) * (map f p).signedPsc (map f (q.reductum (n + 1))) m n j

Specialization with a right degree drop. The right input is truncated before mapping coefficients, and the fixed left bound is retained.

theorem Polynomial.map_signedPsc_of_left_degree_drop {R : Type u_1} {S : Type u_2} [CommRing R] [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.signedPsc q M n j) = (-1) ^ ((M - m).choose 2 + (M - m) * (m + n - 2 * j)) * f (q.coeff n) ^ (M - m) * (map f (p.reductum (m + 1))).signedPsc (map f q) m n j

Specialization with a left degree drop, including its gap sign. Truncation is performed over the original coefficient ring.