Sturm's theorem in Lean 4/Mathlib without real analysis beyond IVT: one-sided signs + Cauchy index

Mathlib (late 2026) has Polynomial.sturmSeq and List.signVariations but not Sturm's theorem. A layout that went through in ~600 lines with no sorry:

1. One-sided signs, defined algebraically: rest p x := p /ₘ (X - C x) ^ rootMultiplicity x p (Mathlib: pow_mul_divByMonic_rootMultiplicity_eq, eval_divByMonic_pow_rootMultiplicity_ne_zero). sgnR p x := sign (eval x (rest p x)), sgnL p x := (-1)^m * sgnR p x. A local_form lemma (p = (X - C x)^n * g, g x ≠ 0 ⇒ multiplicity n and rest = g, via rootMultiplicity_mul_X_sub_C_pow + mul_divByMonic_cancel_left) gives multiplicativity and 'adding a higher-order term changes nothing'. 2. IVT used exactly once: on (x, y] without roots, sign p(y) = sgnR p x. Telescoping by strong induction on the number of roots in (a,b), peeling off Finset.max': sgnL p b - sgnR p a = Σ_{roots in (a,b)} (sgnR - sgnL). 3. Jump of q/p at x: if ord q < ord p ∧ Odd (ord p + ord q) then sgnR p * sgnR q else 0. Then jump p q + jump q p = halfJump (p*q) is a 3-way case split, and jump p (q + s*p) = jump p q is the only real lemma. With p' : jump p p' x = 1 at each root (Mathlib derivative_X_sub_C_pow). 4. Generalized chains C c * p = s * q - C d * r (c, d > 0) need no degree condition at all; induction on the chain + List.signVariations_cons_cons_of_ne_zero + omega closes Sturm. Mathlib's sturmSeq p q is such a chain (c = d = 1, s = -((-p)/q), from EuclideanDomain.div_add_mod). 5. ±∞: div_tendsto_atTop_leadingCoeff_div_of_degree_eq with Q = X^natDegree gives the eventual sign; pick a, b from (eventually ...).exists.

Bonus: since step 4 needs no division, a certificate checker over List ℤ (only + and *) runs fine under decide +kernel; a degree-20 positivity goal checks in well under a second.