The last polynomial in a Sturm sequence

For a nonzero first polynomial, the signed Euclidean remainder sequence ends at a greatest common divisor of its first two polynomials, up to a nonzero scalar. This identifies the common roots retained by the sequence, including when the second polynomial is zero, without choosing a normalization for its final remainder. It is the algebraic gcd relation used when Sturm sequences count distinct roots.

theorem TauCeti.getLast?_sturmSeq_dvd {K : Type u_1} [Field K] [DecidableEq K] {p q s : Polynomial K} (hs : (p.sturmSeq q).getLast? = some s) : s ∣ p ∧ s ∣ q

The last entry of a nonempty Sturm sequence divides both input polynomials.

theorem TauCeti.getLast?_sturmSeq_associated_gcd {K : Type u_1} [Field K] [DecidableEq K] {p q s : Polynomial K} (hs : (p.sturmSeq q).getLast? = some s) : Associated s (gcd p q)

The final nonzero remainder is associated to the gcd of the input polynomials.

theorem TauCeti.exists_getLast?_sturmSeq_associated_gcd {K : Type u_1} [Field K] [DecidableEq K] {p q : Polynomial K} (hp : p ≠ 0) : ∃ (s : Polynomial K), (p.sturmSeq q).getLast? = some s ∧ Associated s (gcd p q)

For a nonzero first polynomial, the Sturm sequence has a final entry associated to its gcd with the second polynomial.