Computing Cauchy indices by Sturm sequences

The Cauchy index of an arbitrary quotient q / p is the difference of the sign variations of Polynomial.sturmSeq p q at the two endpoints. On the whole line these variations depend only on leading coefficients and degree parities. The numerator need not be a multiple of the derivative of the denominator, and common factors and multiple roots are allowed.

This connects signed Euclidean remainder sequences to Cauchy indices, so coefficient formulas for the sequences can compute indices and Tarski queries. In particular, one Euclidean step changes the whole-line index of q / p only by the contribution of the leading coefficients of p and q (Polynomial.cauchyIndex_univ_eq_add_cauchyIndex_neg_mod).

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, §2.2.2 (the Cauchy index and signed remainder sequences). The sequence used here is Mathlib's Polynomial.sturmSeq, by Tomaz Mascarenhas, Pedro Saccomani, and Sarah Pereira.

theorem Polynomial.cauchyIndex_eq_sub_signVariations_Ioo {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p q : Polynomial R) {a b : R} (hab : a < b) : p.cauchyIndex q (Set.Ioo a b) = ↑(TauCeti.Sturm.signVariationsRight (p.sturmSeq q) a) - ↑(TauCeti.Sturm.signVariationsLeft (p.sturmSeq q) b)

On an arbitrary open interval, the Cauchy index is the right-hand variation at the left endpoint minus the left-hand variation at the right endpoint. Either endpoint may be a pole or a common root.

theorem Polynomial.cauchyIndex_eq_sub_signVariations_univ {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p q : Polynomial R) : p.cauchyIndex q Set.univ = ↑(TauCeti.Sturm.signVariationsAtBot (p.sturmSeq q)) - ↑(TauCeti.Sturm.signVariationsAtTop (p.sturmSeq q))

The Cauchy index of q / p on the whole ordered real closed field is computed by the degree-parity and leading-coefficient variations of its Sturm sequence. No squarefreeness or coprimality assumption is needed. For a zero denominator both sides are zero by convention.

theorem Polynomial.cauchyIndex_univ_eq_add_cauchyIndex_neg_mod {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p q : Polynomial R} (hp : p ≠ 0) (hq : q ≠ 0) : p.cauchyIndex q Set.univ = (if Odd (p.natDegree + q.natDegree) then ↑(SignType.sign p.leadingCoeff) * ↑(SignType.sign q.leadingCoeff) else 0) + q.cauchyIndex (-(p % q)) Set.univ

The Euclidean recurrence for the whole-line Cauchy index. Passing from q / p to -(p % q) / q changes the index by sign p.leadingCoeff * sign q.leadingCoeff when the degrees of p and q have opposite parities, and leaves it unchanged otherwise.