Sturm's theorem

For a squarefree real polynomial p and a < b with p a ≠ 0, p b ≠ 0, the number of distinct real roots of p in (a, b] is V(a) - V(b), where V(x) is the number of sign variations of the Sturm sequence p, p', -(p % p'), … evaluated at x.

The local analysis at a root of a member of the chain is organised through the relation Sturm.FlankReduce on sign lists, and the global statement follows by induction on the number of critical points in (a, b]. The file also provides a sign-variation toolkit on lists of signs (Sturm.signChanges, Sturm.wallCount) that BudanFourier reuses.

Main definitions

• Sturm.sturmAux p q: the signed remainder chain p, q, -(p % q), ….
• Sturm.sturmSeq p: sturmAux p (derivative p).
• Sturm.signVarAt L x: the number of sign variations of the values at x of the polynomials in L.
• Sturm.signChanges s: the number of sign variations of a list of signs, zeros ignored.

Main results

• Sturm.sturm: Sturm's theorem.
• Sturm.signVarAt_drop_at_critical_point: the local drop of V at a single critical point.
• Sturm.signChanges_eq_wallCount, Sturm.wallCount_even_iff_endpoints: parity of the number of sign variations from the end signs.
• Sturm.sturmAux_eq_sturmSeq, Sturm.signVarAt_eq_signVariations: the chain is Mathlib's Polynomial.sturmSeq and signVarAt is Mathlib's List.signVariations of the values; Sturm.signVariations_eq_signChanges relates Polynomial.signVariations to signChanges.

Implementation notes

Mathlib has the Sturm sequence (Polynomial.sturmSeq) and sign variations of lists, but not Sturm's theorem. This file keeps its own chain sturmAux, defined by recursion on the degree of the divisor, and proves that it agrees with Polynomial.sturmSeq for p ≠ 0.

References

• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, 2nd ed., Springer, 2006, §2.2.
• W. Li, The Sturm–Tarski Theorem, Archive of Formal Proofs, 2014 (Isabelle/HOL).

@[irreducible]

noncomputable def Sturm.sturmAux (p q : Polynomial ℝ) : List (Polynomial ℝ)

The signed remainder chain starting from (p, q): p :: q :: -(p % q) :: …, stopping when a remainder hits 0. Terminates because (p % q).degree < q.degree.

Equations

• Sturm.sturmAux p q = if _hq : q = 0 then [p] else p :: Sturm.sturmAux q (-(p % q))

noncomputable def Sturm.sturmSeq (p : Polynomial ℝ) : List (Polynomial ℝ)

Sturm sequence of p: the signed remainder sequence of p and its derivative.

Equations

• Sturm.sturmSeq p = Sturm.sturmAux p (Polynomial.derivative p)

noncomputable def Sturm.signVarAt (L : List (Polynomial ℝ)) (x : ℝ) : ℕ

Sign variations of a list of polynomials evaluated at x: count sign changes in L.map (eval x), ignoring zeros. Eval-analogue of Polynomial.signVariations.

Equations

• One or more equations did not get rendered due to their size.

P1 — chain algebra

The signed-remainder step next = -(a % b) obeys a + next = b * (a / b). Evaluated at a root of the middle member b, this forces a(x) = -next(x): the predecessor and successor are antipodal there. With consecutive members coprime (squarefree case), neither vanishes, so they have strictly opposite signs — the engine that makes interior sign-variation changes cancel.

theorem Sturm.add_neg_mod (a b : Polynomial ℝ) : a + -(a % b) = b * (a / b)

Signed-remainder step. With next = -(a % b), we have a + next = b * (a / b).

theorem Sturm.eval_eq_neg_next_of_root {a b : Polynomial ℝ} {x : ℝ} (hx : b.IsRoot x) : Polynomial.eval x a = -Polynomial.eval x (-(a % b))

Antipodal at a root of the middle member. If x is a root of b, the predecessor a and the successor next = -(a % b) take opposite values at x: a(x) = -next(x).

theorem Sturm.isCoprime_step {a b : Polynomial ℝ} (h : IsCoprime a b) : IsCoprime b (-(a % b))

Coprimality is preserved by the signed-remainder step. If a, b are coprime then so are b and the successor next = -(a % b). (Same ideal: (a, b) = (b, a % b).)

theorem Sturm.isCoprime_self_derivative {p : Polynomial ℝ} (hp : Squarefree p) : IsCoprime p (Polynomial.derivative p)

Squarefree ⟹ coprime to its derivative (over ℝ, a perfect field). The whole Sturm chain inherits its gcd from gcd p p', which is a unit precisely when p is squarefree.

theorem Sturm.not_common_root {a b : Polynomial ℝ} (h : IsCoprime a b) {x : ℝ} (ha : a.IsRoot x) (hb : b.IsRoot x) : False

Coprime polynomials share no real root (Bézout: u·a + v·b = 1 evaluated at a common root gives 0 = 1).

P2 — local constancy

On an interval where a polynomial has no root its evaluation keeps a constant sign (IVT: an opposite sign at the endpoints would force a root in between). Hence on an interval free of roots of EVERY chain member, the whole sign pattern — and therefore signVarAt — is constant.

theorem Sturm.sign_eval_eq_of_no_root {q : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) (hne : ∀ x ∈ Set.Icc a b, Polynomial.eval x q ≠ 0) : SignType.sign (Polynomial.eval a q) = SignType.sign (Polynomial.eval b q)

Constant sign on a root-free interval. If q has no root in [a, b], then q takes the same sign at a and b.

theorem Sturm.signVarAt_eq_of_no_root {L : List (Polynomial ℝ)} {a b : ℝ} (hab : a ≤ b) (hne : ∀ q ∈ L, ∀ x ∈ Set.Icc a b, Polynomial.eval x q ≠ 0) : signVarAt L a = signVarAt L b

signVarAt is constant on a root-free interval. If no member of L has a root in [a, b], the sign variations of L agree at a and b.

P3 — behaviour at a root of p (analytic core)

At a simple root α of p (so p'(α) ≠ 0), write p = (X - α)·g; then g(α) = p'(α) ≠ 0, and near α, sign(p(x)) = sign(x - α)·sign(p'(α)): p flips sign, with orientation fixed by p'. This is the analytic engine behind "the leading pair (p, p') loses exactly one sign variation as x crosses α". The remaining combinatorial accounting (full V-drop over the list) is P3'/P5.

theorem Sturm.eval_divByMonic_eq_derivative_at_root {p : Polynomial ℝ} {α : ℝ} (hp0 : Polynomial.eval α p = 0) : Polynomial.eval α (p /ₘ (Polynomial.X - Polynomial.C α)) = Polynomial.eval α (Polynomial.derivative p)

At a root α of p, the cofactor p /ₘ (X - α) evaluates to p'(α).

theorem Sturm.eventually_sign_eval_simple_root {p : Polynomial ℝ} {α : ℝ} (hp0 : Polynomial.eval α p = 0) (hp' : Polynomial.eval α (Polynomial.derivative p) ≠ 0) : ∀ᶠ (x : ℝ) in nhds α, SignType.sign (Polynomial.eval x p) = SignType.sign (x - α) * SignType.sign (Polynomial.eval α (Polynomial.derivative p))

Sign flip at a simple root. Near a simple root α of p, sign(p(x)) = sign(x - α) · sign(p'(α)).

P3' — sign-variation combinatorics (toward the V-drop)

Factor signVarAt through a pure signChanges : List SignType → ℕ and prove the bookkeeping facts the V-drop needs: zeros are invisible, and a three-term window with opposite nonzero ends always shows exactly one variation regardless of its middle (the interior-root cancellation from P1's antipodal property, in combinatorial form).

def Sturm.signChanges (s : List SignType) : ℕ

Sign changes in a raw list of signs: drop the zeros, then count adjacent differences.

Equations

• Sturm.signChanges s = (List.destutter (fun (x1 x2 : SignType) => x1 ≠ x2) (List.filter (fun (x : SignType) => decide (x ≠ 0)) s)).length - 1

theorem Sturm.signVarAt_eq_signChanges (L : List (Polynomial ℝ)) (x : ℝ) : signVarAt L x = signChanges (List.map (fun (p : Polynomial ℝ) => SignType.sign (Polynomial.eval x p)) L)

signVarAt is signChanges of the evaluated sign pattern.

@[simp]

theorem Sturm.signChanges_cons_zero (s : List SignType) : signChanges (0 :: s) = signChanges s

A leading zero is invisible to signChanges.

theorem Sturm.signChanges_triple {a m b : SignType} (ha : a ≠ 0) (hb : b ≠ 0) (hab : a ≠ b) : signChanges [a, m, b] = 1

Interior cancellation, combinatorial form. A three-term window whose ends are nonzero and opposite shows exactly one sign change, whatever its middle term is.

theorem Sturm.signChanges_cons_of_filter_nil {c : SignType} {s : List SignType} (hs : List.filter (fun (x : SignType) => decide (x ≠ 0)) s = []) : signChanges (c :: s) = 0

If every entry of s is a zero, prepending anything gives no variations.

theorem Sturm.signChanges_cons_of_ne_zero {c d : SignType} (hc : c ≠ 0) {s : List SignType} (hd : (List.filter (fun (x : SignType) => decide (x ≠ 0)) s).head? = some d) : signChanges (c :: s) = signChanges s + if c = d then 0 else 1

Head recursion. Prepending a nonzero sign c adds exactly one variation when c differs from the first surviving (nonzero) sign d of s, and none when it agrees. This is the leading-pair flip in combinatorial form.

theorem Sturm.filter_ne_zero_head?_cons {c : SignType} (hc : c ≠ 0) (t : List SignType) : (List.filter (fun (x : SignType) => decide (x ≠ 0)) (c :: t)).head? = some c

The first surviving sign of c :: t is c when c ≠ 0.

theorem Sturm.signChanges_head_drop {c c' : SignType} (hc : c ≠ 0) (hc' : c' ≠ 0) (hne : c ≠ c') {t : List SignType} (hd : (List.filter (fun (x : SignType) => decide (x ≠ 0)) t).head? = some c') : signChanges (c :: t) = signChanges (c' :: t) + 1

Leading-pair drop. If the head c flips relative to the first surviving sign c' of the tail (c ≠ c', both nonzero), the count is one more than with head c'. With c = sign p(α⁻) and c' = sign p'(α) = sign p(α⁺), this is the exact -1 of the (p, p') pair across a root.

theorem Sturm.signChanges_remove_middle {a b m : SignType} (ha : a ≠ 0) (hb : b ≠ 0) (hab : a ≠ b) {rest : List SignType} : signChanges (a :: m :: b :: rest) = signChanges (a :: b :: rest)

Interior cancellation. Deleting a middle entry that sits between two nonzero opposite signs leaves the count unchanged — whatever the deleted sign is. This is why an interior chain member, whose sign may change across α, does not move V (its neighbours are fixed and opposite).

P5 — structural facts about the Sturm sequence (toward assembly)

@[simp]

theorem Sturm.sturmAux_zero (p : Polynomial ℝ) : sturmAux p 0 = [p]

The chain stops at a zero divisor: sturmAux p 0 = [p].

theorem Sturm.sturmAux_cons {p q : Polynomial ℝ} (hq : q ≠ 0) : sturmAux p q = p :: sturmAux q (-(p % q))

One unfolding step of the chain when the divisor is nonzero.

theorem Sturm.sturmAux_head? (p q : Polynomial ℝ) : (sturmAux p q).head? = some p

Every chain sturmAux p q starts with p.

theorem Sturm.sturmSeq_head? (p : Polynomial ℝ) : (sturmSeq p).head? = some p

The Sturm sequence starts with p.

theorem Sturm.sturmAux_mem_ne_zero (p q : Polynomial ℝ) : p ≠ 0 → ∀ r ∈ sturmAux p q, r ≠ 0

Every member of a Sturm chain is nonzero, provided the dividend is.

theorem Sturm.sturmSeq_prod_ne_zero {p : Polynomial ℝ} (hp : p ≠ 0) : (sturmSeq p).prod ≠ 0

The product of all Sturm-sequence members is nonzero (each member is nonzero in the domain ℝ[X]). Its roots are exactly the critical points; this makes the critical set finite.

theorem Sturm.sturmAux_consecutive_coprime (p q : Polynomial ℝ) : IsCoprime p q → ∀ (x m : Polynomial ℝ), [x, m] <:+: sturmAux p q → IsCoprime x m

Consecutive members of a signed-remainder chain are coprime (with a coprime seed). Each step preserves coprimality (isCoprime_step), so every adjacent pair [x, m] appearing in the chain is coprime — the source of hiso (no two adjacent members vanish at a common point).

theorem Sturm.sturmAux_consecutive_succ (p q x m y : Polynomial ℝ) : [x, m, y] <:+: sturmAux p q → y = -(x % m)

The successor of a chain triple is the signed remainder. For any three consecutive members [x, m, y] of a signed-remainder chain, y = -(x % m) — the chain's defining relation, surfaced as a fact about adjacent triples. Together with eval_eq_neg_next_of_root this gives the antipodal flank behaviour at an interior root (the source of hflank).

theorem Sturm.sturmAux_getLast_isUnit (p q : Polynomial ℝ) : IsCoprime p q → ∀ (g : Polynomial ℝ), (sturmAux p q).getLast? = some g → IsUnit g

The last member of a coprime-seeded chain is a unit. The chain ends at the last nonzero remainder — the gcd — which for a coprime seed is a unit (IsCoprime p 0 ↔ IsUnit p at the base). Hence the final Sturm member is a nonzero constant, never vanishing (the source of hlast).

theorem Sturm.signVarAt_cons_head_drop {p : Polynomial ℝ} {tail : List (Polynomial ℝ)} {x y : ℝ} (hpx0 : Polynomial.eval x p ≠ 0) (hpy0 : Polynomial.eval y p ≠ 0) (hne : SignType.sign (Polynomial.eval x p) ≠ SignType.sign (Polynomial.eval y p)) (htail : List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval x q)) tail = List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval y q)) tail) (hfirst : (List.filter (fun (x : SignType) => decide (x ≠ 0)) (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval y q)) tail)).head? = some (SignType.sign (Polynomial.eval y p))) : signVarAt (p :: tail) x = signVarAt (p :: tail) y + 1

Root-crossing bridge. If, between two points x and y, only the head polynomial p changes sign (the rest of the list keeps its signs), p is nonzero at both, and the head sign at y equals the first surviving sign of the tail, then V is exactly one larger at x. This lifts the combinatorial signChanges_head_drop to the evaluated sign lists — the -1 of V across a simple root of p, in generic position.

theorem Sturm.map_sign_eq_of_no_root {L : List (Polynomial ℝ)} {a b : ℝ} (hab : a ≤ b) (hne : ∀ q ∈ L, ∀ z ∈ Set.Icc a b, Polynomial.eval z q ≠ 0) : List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval a q)) L = List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval b q)) L

Tail signs are unchanged on a root-free interval (the htail provider for the keystone).

theorem Sturm.filter_map_sign_head?_cons {q : Polynomial ℝ} {rest : List (Polynomial ℝ)} {y : ℝ} (hq : Polynomial.eval y q ≠ 0) : (List.filter (fun (x : SignType) => decide (x ≠ 0)) (List.map (fun (r : Polynomial ℝ) => SignType.sign (Polynomial.eval y r)) (q :: rest))).head? = some (SignType.sign (Polynomial.eval y q))

The first surviving tail sign is the sign of the first (nonzero-valued) member (the hfirst provider for the keystone).

Interior cancellation at arbitrary position (monolith engine)

theorem Sturm.filter_append_cons_head?_eq {a : SignType} (ha : a ≠ 0) (pre X Y : List SignType) : (List.filter (fun (x : SignType) => decide (x ≠ 0)) (pre ++ a :: X)).head? = (List.filter (fun (x : SignType) => decide (x ≠ 0)) (pre ++ a :: Y)).head?

The first surviving sign of pre ++ a :: X does not depend on X (the inserted/changed entry sits after the nonzero a, never becoming the first nonzero).

theorem Sturm.signChanges_remove_middle_append {a b m : SignType} (ha : a ≠ 0) (hb : b ≠ 0) (hab : a ≠ b) (pre rest : List SignType) : signChanges (pre ++ a :: m :: b :: rest) = signChanges (pre ++ a :: b :: rest)

Interior cancellation, any position. Deleting a middle entry between two nonzero opposite signs leaves the count unchanged, anywhere in the list (induction on the prefix).

Interior-member crossing (piece ii): neighbours are nonzero and opposite

theorem Sturm.sign_neighbours_opposite_at_interior_root {a m : Polynomial ℝ} {c : ℝ} (hco : IsCoprime a m) (hm : Polynomial.eval c m = 0) : SignType.sign (Polynomial.eval c a) ≠ 0 ∧ SignType.sign (Polynomial.eval c a) ≠ SignType.sign (Polynomial.eval c (-(a % m)))

At a root of an interior chain member, its neighbours are nonzero and opposite. If a and m are coprime (consecutive Sturm members) and m(c) = 0, then a(c) and the successor (-(a % m))(c) are both nonzero and carry opposite signs — exactly the configuration that makes signChanges_remove_middle fire, so the interior root contributes 0 to the variation change.

theorem Sturm.signVarAt_remove_middle (pre rest : List (Polynomial ℝ)) (pa pm pb : Polynomial ℝ) {z : ℝ} (ha : SignType.sign (Polynomial.eval z pa) ≠ 0) (hb : SignType.sign (Polynomial.eval z pb) ≠ 0) (hab : SignType.sign (Polynomial.eval z pa) ≠ SignType.sign (Polynomial.eval z pb)) : signVarAt (pre ++ pa :: pm :: pb :: rest) z = signVarAt (pre ++ pa :: pb :: rest) z

Surgery atom. At a point z where the two flanking polynomials pa, pb take nonzero opposite signs, the middle polynomial pm can be deleted from the list without changing signVarAt — anywhere in the list. This is signChanges_remove_middle_append lifted to evaluated polynomial lists; iterating it deletes every interior member that vanishes at a critical point.

theorem Sturm.signChanges_middle_irrelevant {a b m m' : SignType} (ha : a ≠ 0) (hb : b ≠ 0) (hab : a ≠ b) (pre rest : List SignType) : signChanges (pre ++ a :: m :: b :: rest) = signChanges (pre ++ a :: m' :: b :: rest)

Middle irrelevance. Between two nonzero opposite signs, the middle entry's value does not affect the count: changing it from m to m' is invisible (both reduce to the same list with the middle deleted). This is the two-point form of interior cancellation — across a critical point an interior member changes sign, but its fixed opposite neighbours absorb the change.

theorem Sturm.signVarAt_middle_irrelevant (pre rest : List (Polynomial ℝ)) (pa pm pm' pb : Polynomial ℝ) {z : ℝ} (ha : SignType.sign (Polynomial.eval z pa) ≠ 0) (hb : SignType.sign (Polynomial.eval z pb) ≠ 0) (hab : SignType.sign (Polynomial.eval z pa) ≠ SignType.sign (Polynomial.eval z pb)) : signVarAt (pre ++ pa :: pm :: pb :: rest) z = signVarAt (pre ++ pa :: pm' :: pb :: rest) z

Middle irrelevance at the polynomial level (one interior member, at one point).

The key step: flank-reduction (the decoupled two-point comparison engine)

From the Socratic analysis of a critical point: deleting interior chain members that vanish there (each flanked by nonzero opposite neighbours) preserves the sign-variation count. Encode "delete flanked middles" as an inductive relation; it preserves signChanges. The Sturm chain then only has to exhibit the reductions — the combinatorics is decoupled.

inductive Sturm.FlankReduce : List SignType → List SignType → Prop

xs reduces to ys by deleting middle entries flanked by nonzero opposite signs.

• refl (l : List SignType) : FlankReduce l l
• del (pre : List SignType) (a m b : SignType) (rest : List SignType) (ha : a ≠ 0) (hb : b ≠ 0) (hab : a ≠ b) {ys : List SignType} : FlankReduce (pre ++ a :: b :: rest) ys → FlankReduce (pre ++ a :: m :: b :: rest) ys

theorem Sturm.FlankReduce.signChanges_eq {xs ys : List SignType} (h : FlankReduce xs ys) : signChanges xs = signChanges ys

Flank-reduction preserves the count. Each deletion is signChanges_remove_middle_append.

theorem Sturm.signVarAt_eq_of_flankReduce {L₁ L₂ : List (Polynomial ℝ)} {z : ℝ} (h : FlankReduce (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval z q)) L₁) (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval z q)) L₂)) : signVarAt L₁ z = signVarAt L₂ z

Lift to evaluated polynomial lists. If the sign patterns of two polynomial lists at z are flank-related, their sign variations at z agree. This is where the decoupling pays off: the Sturm chain only has to exhibit a FlankReduce between the c⁻ and c⁺ sign patterns.

theorem Sturm.flankReduce_eval_step (pre rest : List (Polynomial ℝ)) (pa pm pb : Polynomial ℝ) {z : ℝ} (ha : SignType.sign (Polynomial.eval z pa) ≠ 0) (hb : SignType.sign (Polynomial.eval z pb) ≠ 0) (hab : SignType.sign (Polynomial.eval z pa) ≠ SignType.sign (Polynomial.eval z pb)) {ys : List SignType} (hrest : FlankReduce (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval z q)) (pre ++ pa :: pb :: rest)) ys) : FlankReduce (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval z q)) (pre ++ pa :: pm :: pb :: rest)) ys

Chain-level reduction step. If at z the flanking polynomials pa, pb carry nonzero opposite signs, a FlankReduce of the list with the middle pm deleted extends to one of the full list. Iterating this (one per interior vanisher) exhibits the reduction of the chain's sign pattern. The flank hypotheses come from sign_neighbours_opposite_at_interior_root (chain structure).

theorem Sturm.FlankReduce.cons (s : SignType) {xs ys : List SignType} (h : FlankReduce xs ys) : FlankReduce (s :: xs) (s :: ys)

FlankReduce is closed under consing. Prepending the same head to both sides preserves the relation (every deletion's prefix just grows by one). Lets the chain-walk keep a fixed head while reducing the tail.

theorem Sturm.flankReduce_chain_walk {c z : ℝ} (a : Polynomial ℝ) (tail : List (Polynomial ℝ)) : (∀ (x m y : Polynomial ℝ), [x, m, y] <:+: a :: tail → Polynomial.eval c m = 0 → SignType.sign (Polynomial.eval z x) ≠ 0 ∧ SignType.sign (Polynomial.eval z y) ≠ 0 ∧ SignType.sign (Polynomial.eval z x) ≠ SignType.sign (Polynomial.eval z y)) → (∀ (x y : Polynomial ℝ), [x, y] <:+: a :: tail → ¬(Polynomial.eval c x = 0 ∧ Polynomial.eval c y = 0)) → (∀ (q : Polynomial ℝ), (a :: tail).getLast? = some q → Polynomial.eval c q ≠ 0) → FlankReduce (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval z q)) (a :: tail)) (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval z q)) (a :: List.filter (fun (q : Polynomial ℝ) => decide (Polynomial.eval c q ≠ 0)) tail))

Chain-walk reduction (the decoupled wall). Walking a polynomial chain a :: tail, every interior member that vanishes at c — flanked (hflank) by neighbours of nonzero opposite sign at the evaluation point z — is deleted: the sign pattern at z FlankReduces to that of the chain with those interior vanishers removed (the head is always kept). hiso records that no two consecutive members both vanish at c (Sturm chains satisfy this by consecutive coprimality); hlast records that the final member does not vanish at c (Sturm's last member is a nonzero constant). With these, the chain's c⁻/c⁺ sign patterns both reduce to the same kept chain.

Domain-wall view: signChanges as a local additive sum (BPR sign-variation theory in Lean)

Following classical real-algebraic-geometry sign-variation theory (Basu–Pollack–Roy). On a zero-free list, signChanges equals the local count of adjacent disagreements (wallCount), an additive sum that makes the two-point comparison decouple.

def Sturm.wallCount : List SignType → ℕ

The local count of adjacent disagreements (±1 domain walls; no zeros dropped).

Equations

• Sturm.wallCount [] = 0
• Sturm.wallCount [head] = 0
• Sturm.wallCount (a :: b :: t) = (if a = b then 0 else 1) + Sturm.wallCount (b :: t)

theorem Sturm.signChanges_eq_wallCount_of_zero_free (f : List SignType) : 0 ∉ f → signChanges f = wallCount f

On a zero-free list, signChanges is the local additive wallCount (head recursion).

theorem Sturm.signChanges_eq_wallCount (s : List SignType) : signChanges s = wallCount (List.filter (fun (x : SignType) => decide (x ≠ 0)) s)

The additive bridge. signChanges s = wallCount (nonzero filtrate of s).

theorem Sturm.wallCount_neg_one_pow (a : SignType) (l : List SignType) : 0 ∉ a :: l → (-1) ^ wallCount (a :: l) = a * (a :: l).getLast ⋯

The ℤ/2 layer of sign variation. For a zero-free list, (-1)^(wallCount) telescopes to the product of the endpoint signs: modulo 2, sign variation forgets everything but whether the ends disagree. This is the engine behind Descartes' even-difference refinement and the transversality (sign p') at a simple root — the single-bit shadow of the count.

theorem Sturm.wallCount_even_iff_endpoints {a : SignType} {l : List SignType} (h : 0 ∉ a :: l) : Even (wallCount (a :: l)) ↔ a = (a :: l).getLast ⋯

Parity, clean form. A zero-free list has an even number of sign changes iff its endpoints agree. The ±1 shadow: parity of sign variation = "do the ends match?".

Continuity sub-thread: signs are locally constant near a nonzero point

theorem Sturm.eventually_sign_eval_eq {q : Polynomial ℝ} {c : ℝ} (hc : Polynomial.eval c q ≠ 0) : ∀ᶠ (z : ℝ) in nhds c, SignType.sign (Polynomial.eval z q) = SignType.sign (Polynomial.eval c q)

Local sign constancy. Near a point where q is nonzero, q keeps its sign (continuity).

theorem Sturm.eventually_flank_opposite_at_interior_root {a m : Polynomial ℝ} {c : ℝ} (hco : IsCoprime a m) (hm : Polynomial.eval c m = 0) : ∀ᶠ (z : ℝ) in nhds c, SignType.sign (Polynomial.eval z a) ≠ 0 ∧ SignType.sign (Polynomial.eval z a) ≠ SignType.sign (Polynomial.eval z (-(a % m)))

Flank-opposite persists near an interior root. At a root c of an interior member m (coprime to its predecessor a), the predecessor and successor -(a % m) keep nonzero opposite signs at every nearby z — exactly the flank hypotheses flankReduce_eval_step needs at c⁻ / c⁺ (not just at c).

Local root-crossing (closing P3 for one simple root, generic position)

theorem Sturm.sign_eval_eq_sign_deriv_right {p : Polynomial ℝ} {α b : ℝ} (hroot : Polynomial.eval α p = 0) (hp'0 : Polynomial.eval α (Polynomial.derivative p) ≠ 0) (hαb : α < b) (hp_only : ∀ z ∈ Set.Icc α b, Polynomial.eval z p = 0 → z = α) : SignType.sign (Polynomial.eval b p) = SignType.sign (Polynomial.eval α (Polynomial.derivative p))

Just to the right of a simple root, p carries the sign of p'(α).

theorem Sturm.sign_eval_eq_neg_sign_deriv_left {p : Polynomial ℝ} {α a : ℝ} (hroot : Polynomial.eval α p = 0) (hp'0 : Polynomial.eval α (Polynomial.derivative p) ≠ 0) (haα : a < α) (hp_only : ∀ z ∈ Set.Icc a α, Polynomial.eval z p = 0 → z = α) : SignType.sign (Polynomial.eval a p) = -SignType.sign (Polynomial.eval α (Polynomial.derivative p))

Just to the left of a simple root, p carries the opposite sign of p'(α).

theorem Sturm.signVarAt_drop_at_simple_root {p : Polynomial ℝ} {α a b : ℝ} (hp'ne : Polynomial.derivative p ≠ 0) (hroot : Polynomial.eval α p = 0) (hp'0 : Polynomial.eval α (Polynomial.derivative p) ≠ 0) (haα : a < α) (hαb : α < b) (hp_left : ∀ z ∈ Set.Icc a α, Polynomial.eval z p = 0 → z = α) (hp_right : ∀ z ∈ Set.Icc α b, Polynomial.eval z p = 0 → z = α) (htail : ∀ q ∈ (sturmSeq p).tail, ∀ z ∈ Set.Icc a b, Polynomial.eval z q ≠ 0) : signVarAt (sturmSeq p) a = signVarAt (sturmSeq p) b + 1

Local root-crossing. Across a simple root α of p (generic position: α the only root of p in [a,α] and [α,b], and no Sturm-tail member vanishes in [a,b]), the sign variations of the Sturm sequence drop by exactly one.

Single critical point: the decoupled crossing (chain-walk + head-drop)

theorem Sturm.signVarAt_drop_at_critical_point {p : Polynomial ℝ} (hp : Squarefree p) {a b c : ℝ} (hab : a ≤ b) (hc : c ∈ Set.Icc a b) (ha : Polynomial.eval a p ≠ 0) (hb : Polynomial.eval b p ≠ 0) (h_only : ∀ q ∈ sturmSeq p, ∀ z ∈ Set.Icc a b, Polynomial.eval z q = 0 → z = c) : signVarAt (sturmSeq p) a = signVarAt (sturmSeq p) b + if Polynomial.eval c p = 0 then 1 else 0

Single-critical-point crossing. If c ∈ [a, b] is the only point of [a, b] where any member of the Sturm sequence of a squarefree p vanishes (with p(a), p(b) ≠ 0), then V drops by 1 if p(c) = 0 and is unchanged otherwise. Both endpoints' sign patterns FlankReduce (via flankReduce_chain_walk) to the same chain with the interior c-vanishers removed; on that reduced chain only the head p can cross, so the change collapses to a single head-drop. This is the per-point quantum of Sturm's theorem — and it also covers the case c = a/c = b (a tail member vanishing at an endpoint, which then necessarily has p(c) ≠ 0) and the degenerate no-critical case.

Playground — what else falls out of the machinery

theorem Sturm.exists_root_of_sign_ne {p : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) (h : SignType.sign (Polynomial.eval a p) ≠ SignType.sign (Polynomial.eval b p)) : ∃ x ∈ Set.Icc a b, Polynomial.eval x p = 0

Bolzano, sign form. A sign change of p between a and b forces a real root in [a,b] (contrapositive of local constancy).

theorem Sturm.signVariations_eq_signChanges (P : Polynomial ℝ) : P.signVariations = signChanges (List.map (⇑SignType.sign) P.coeffList)

Bridge to Descartes' rule of signs. Mathlib's signVariations (sign changes of the coefficient list) is exactly our signChanges of the mapped coefficient signs — so the whole signChanges toolkit (zeros invisible, interior cancellation, head recursion) transfers to it.

theorem Sturm.signChanges_coeff_cons_zero (P : Polynomial ℝ) : signChanges (0 :: List.map (⇑SignType.sign) P.coeffList) = P.signVariations

A simple corollary of the bridge: the sign-variation count of the coefficients is invariant under prepending a zero sign (the signChanges lemma, now visible for Descartes).

theorem Sturm.sturm (p : Polynomial ℝ) (hp : Squarefree p) {a b : ℝ} (hab : a < b) (ha : Polynomial.eval a p ≠ 0) (hb : Polynomial.eval b p ≠ 0) : signVarAt (sturmSeq p) a - signVarAt (sturmSeq p) b = {x ∈ p.roots.toFinset | a < x ∧ x ≤ b}.card

Sturm's theorem. For squarefree p and a < b with neither endpoint a root of p, the drop in sign variations of the Sturm sequence equals the number of distinct real roots in (a, b].

Comparison with Mathlib's Polynomial.sturmSeq and List.signVariations

theorem Sturm.sturmAux_eq_sturmSeq {p q : Polynomial ℝ} (hp : p ≠ 0) : sturmAux p q = p.sturmSeq q

For p ≠ 0, the chain sturmAux p q is Mathlib's Sturm sequence Polynomial.sturmSeq p q.

theorem Sturm.sturmSeq_eq {p : Polynomial ℝ} (hp : p ≠ 0) : sturmSeq p = p.sturmSeq (Polynomial.derivative p)

The Sturm sequence of p ≠ 0 is Mathlib's Polynomial.sturmSeq p (derivative p).

theorem Sturm.signVarAt_eq_signVariations (L : List (Polynomial ℝ)) (x : ℝ) : signVarAt L x = (List.map (fun (p : Polynomial ℝ) => Polynomial.eval x p) L).signVariations

signVarAt L x is Mathlib's List.signVariations of the values of L at x.