Sturm's theorem

sturm — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Sturm's theorem.** For a squarefree real polynomial `p` and an interval
`(a, b)` with `a < b` whose endpoints are not roots of `p`, the number of
distinct roots of `p` in `(a, b)` equals `σ(a) − σ(b)`. -/
theorem 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 := by
  sorry

Informal solution sketch

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).

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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: sturm
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.