Sturm's theorem

sturm

Submitter: Kim Morrison.

Notes: §97 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The number of distinct real roots of a squarefree real polynomial in an open interval equals the drop in the number of sign variations of its Sturm chain across the interval. The Sturm chain, the sign-variation counter, and the variation function σ are defined in the problem; mathlib has none of them. The chain uses the negated-remainder convention p_{k+1} = -(p_{k-1} mod p_k), for which the count is σ(a) - σ(b). Sturm's theorem is formalized in Isabelle/HOL (Manuel Eberl, AFP entry Sturm_Sequences) in the same distinct-root form.

Source: J. C. F. Sturm (1829). Listed as §97 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Formalized in Isabelle/HOL by Manuel Eberl (AFP entry Sturm_Sequences).

Informal solution: As x increases across a simple root of p exactly one sign variation of the Sturm chain is lost and none is gained — the standard sign analysis of consecutive chain entries at a root, using squarefreeness so that p and p' have no common root — while across a root of an interior chain entry the variation count is unchanged. Between roots σ is locally constant. Hence the number of distinct roots of p in (a, b) equals σ(a) - σ(b).

theorem declaration uses `sorry`sturm (p : ℝ[X]) (hp : Squarefree p) {a b : ℝ} (hab : a < b)
    (ha : p.eval a ≠ 0) (hb : p.eval b ≠ 0) :
    ((p.roots.toFinset).filter (fun x => a < x ∧ x < b)).card =
      sigma p a - sigma p b := byp:ℝ[X]hp:Squarefree pa:ℝb:ℝhab:a < bha:eval a p ≠ 0hb:eval b p ≠ 0⊢ {x ∈ p.roots.toFinset | a < x ∧ x < b}.card = sigma p a - sigma p b
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on May 26, 2026

• @adrianmartir with Aristotle (Harmonic) on May 28, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 28, 2026