Signed root sums for alternating Sturm chains

The local jumps of a alternating chain telescope to a signed sum over the roots of its first polynomial in an open interval. Only those roots must be simple; the endpoints may be roots of interior entries, but not of the first entry.

theorem TauCeti.Sturm.IsAlternating.sum_sign {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p q : Polynomial R} {cs : List (Polynomial R)} (h : IsAlternating (p :: q :: cs)) {a b : R} (hsimple : ∀ (r : R), a < r → r < b → Polynomial.eval r p = 0 → Polynomial.eval r (Polynomial.derivative p) ≠ 0) (hab : a < b) (ha : Polynomial.eval a p ≠ 0) (hb : Polynomial.eval b p ≠ 0) : ↑(signVariationsAt (p :: q :: cs) a) - ↑(signVariationsAt (p :: q :: cs) b) = ∑ r ∈ p.roots.toFinset with a < r ∧ r < b, ↑(SignType.sign (Polynomial.eval r (Polynomial.derivative p) * Polynomial.eval r q))

The signed Sturm formula on an interval whose endpoints are not roots of the head polynomial. Interior entries may vanish at either endpoint.