The Budan–Fourier theorem

For a nonzero real polynomial p and a < b with p a ≠ 0, p b ≠ 0, let V(x) be the number of sign variations of the derivative tower p, p', p'', …, p^(deg p) evaluated at x. Then the number of real roots of p in (a, b], counted with multiplicity, is at most V(a) - V(b), and the difference is even.

The local analysis at a point c where a whole block of the tower vanishes is done by the sign recursions BudanFourier.Rseq and BudanFourier.Lseq, which give the signs of the tower just to the right and just to the left of c. The sign-variation toolkit is the one of Sturm.

Main definitions

• BudanFourier.fourierSeq p: the derivative tower [p, p', …, p^(deg p)].
• BudanFourier.fourierVar p x: its number of sign variations at x.

Main results

• BudanFourier.budan_fourier: the Budan–Fourier inequality and the parity of the difference.
• BudanFourier.fourierVar_drop_at_critical_point: the drop of fourierVar at one critical point is the multiplicity of the root plus an even number.
• BudanFourier.signs_right_eq_Rseq, BudanFourier.signs_left_eq_Lseq: the signs of the tower on either side of a point.

References

• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, 2nd ed., Springer, 2006, §2.2.
• W. Li, L. C. Paulson, Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan–Fourier theorem, CPP 2019, 52–64.

noncomputable def BudanFourier.fourierSeq (p : Polynomial ℝ) : List (Polynomial ℝ)

The Fourier sequence (derivative tower) of p: p, p', p'', …, p^(deg p).

Equations

• BudanFourier.fourierSeq p = List.map (fun (k : ℕ) => (⇑Polynomial.derivative)^[k] p) (List.range (p.natDegree + 1))

theorem BudanFourier.fourierSeq_length (p : Polynomial ℝ) : (fourierSeq p).length = p.natDegree + 1

The Fourier sequence has deg p + 1 entries.

theorem BudanFourier.fourierSeq_ne_nil (p : Polynomial ℝ) : fourierSeq p ≠ []

The Fourier sequence is never empty (it always contains at least p).

theorem BudanFourier.fourierSeq_mem (p q : Polynomial ℝ) : q ∈ fourierSeq p ↔ ∃ k ≤ p.natDegree, q = (⇑Polynomial.derivative)^[k] p

Membership in the Fourier sequence: its entries are exactly the iterated derivatives p^(k) for 0 ≤ k ≤ deg p.

noncomputable def BudanFourier.fourierVar (p : Polynomial ℝ) (x : ℝ) : ℕ

Fourier sign variations of p at x: the number of sign changes in the derivative tower evaluated at x, with zeros dropped. The eval-analogue, on the derivative tower, of the count used for Sturm's theorem.

Equations

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

theorem BudanFourier.fourierVar_eq_signVarAt (p : Polynomial ℝ) (x : ℝ) : fourierVar p x = Sturm.signVarAt (fourierSeq p) x

Bridge to the Sturm toolkit. fourierVar p x is, definitionally, Sturm.signVarAt applied to the derivative tower. This single rfl makes the entire sign-variation toolkit from Sturm (locally-constant on root-free intervals, signChanges/wallCount parity engine, interior cancellation) act directly on the Fourier sequence.

theorem BudanFourier.fourierVar_eq_of_no_root {p : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) (hne : ∀ q ∈ fourierSeq p, ∀ x ∈ Set.Icc a b, Polynomial.eval x q ≠ 0) : fourierVar p a = fourierVar p b

fourierVar is locally constant. On a closed interval where no member of the derivative tower vanishes, the Fourier sign-variation count does not change. Reused verbatim from the generic Sturm.signVarAt_eq_of_no_root; this is the "nothing happens between critical points" half of the global telescoping argument.

theorem BudanFourier.fourierSeq_mem_ne_zero {p : Polynomial ℝ} (hp : p ≠ 0) (q : Polynomial ℝ) : q ∈ fourierSeq p → q ≠ 0

Every member of the derivative tower is nonzero. For k ≤ deg p, the k-th derivative p^(k) has nonzero coefficient (deg p).descFactorial k · leadingCoeff p in degree deg p − k (char 0), so it is nonzero. Unlike the Sturm chain this is the only nonvanishing we get — two consecutive tower members can still share a root, which is exactly why the local analysis differs from Sturm's coprime chain.

theorem BudanFourier.fourierSeq_prod_ne_zero {p : Polynomial ℝ} (hp : p ≠ 0) : (fourierSeq p).prod ≠ 0

The product of the derivative tower is nonzero (the analogue of Sturm.sturmSeq_prod_ne_zero): its roots are exactly the "critical points" where some p^(k) vanishes, the only places where fourierVar can move.

theorem BudanFourier.rootCount_split (M : Multiset ℝ) {a d b : ℝ} (had : a ≤ d) (hdb : d ≤ b) : (Multiset.filter (fun (x : ℝ) => a < x ∧ x ≤ b) M).card = (Multiset.filter (fun (x : ℝ) => a < x ∧ x ≤ d) M).card + (Multiset.filter (fun (x : ℝ) => d < x ∧ x ≤ b) M).card

Half-open root count splits additively (with multiplicity). For a ≤ d ≤ b, the roots of a multiset in (a, b] are those in (a, d] plus those in (d, b]. The multiplicity-aware companion of Sturm's Finset split; needed because Budan–Fourier counts roots with multiplicity.

The recursive monotonicity lemmas (foundation of the block analysis)

The derivative tower steps p^(k+1) = (p^(k))′. So if p^(k) vanishes at c and p^(k+1) keeps a constant nonzero sign just off c, then p^(k) is strictly monotone there and its sign just off c is determined: same sign as p^(k+1) on the right, opposite on the left. This one-step recursion replaces the Taylor/rootMultiplicity bookkeeping entirely.

theorem BudanFourier.sign_eval_right_of_deriv_sign {q : Polynomial ℝ} {c z : ℝ} {s : SignType} (hqc : Polynomial.eval c q = 0) (hcz : c < z) (hs : s ≠ 0) (hsign : ∀ w ∈ Set.Ioc c z, SignType.sign (Polynomial.eval w (Polynomial.derivative q)) = s) : SignType.sign (Polynomial.eval z q) = s

Sign just right of a root = sign of the derivative there. If q(c) = 0 and q′ keeps the constant nonzero sign s on (c, z], then sign (q z) = s.

theorem BudanFourier.sign_eval_left_of_deriv_sign {q : Polynomial ℝ} {c z : ℝ} {s : SignType} (hqc : Polynomial.eval c q = 0) (hzc : z < c) (hs : s ≠ 0) (hsign : ∀ w ∈ Set.Ico z c, SignType.sign (Polynomial.eval w (Polynomial.derivative q)) = s) : SignType.sign (Polynomial.eval z q) = -s

Sign just left of a root = opposite sign of the derivative there. If q(c) = 0 and q′ keeps the constant nonzero sign s on [z, c), then sign (q z) = -s.

Per-member off-c sign recursion

For each tower member, its sign just off c is fixed by whether it vanishes at c:

• kept (q(c) ≠ 0): the sign just off c equals sign (q c) (both sides), by local constancy;
• vanishing (q(c) = 0): on the right it copies the derivative's sign, on the left the opposite — one step of the lemma recursion. Iterated up a vanishing block, these give: right of c the block copies the first kept sign above it (no new sign change), left of c it alternates.

theorem BudanFourier.sign_eval_right_kept {q : Polynomial ℝ} {c b z : ℝ} (hqc : Polynomial.eval c q ≠ 0) (hcz : c < z) (hzb : z ≤ b) (hqno : ∀ w ∈ Set.Ioc c b, Polynomial.eval w q ≠ 0) : SignType.sign (Polynomial.eval z q) = SignType.sign (Polynomial.eval c q)

Kept member, right of c: constant sign.

theorem BudanFourier.sign_eval_left_kept {q : Polynomial ℝ} {a c z : ℝ} (hqc : Polynomial.eval c q ≠ 0) (hzc : z < c) (haz : a ≤ z) (hqno : ∀ w ∈ Set.Ico a c, Polynomial.eval w q ≠ 0) : SignType.sign (Polynomial.eval z q) = SignType.sign (Polynomial.eval c q)

Kept member, left of c: constant sign.

theorem BudanFourier.sign_eval_right_vanish {q : Polynomial ℝ} {c b z : ℝ} (hqc : Polynomial.eval c q = 0) (hcz : c < z) (hzb : z ≤ b) (hq'no : ∀ w ∈ Set.Ioc c b, Polynomial.eval w (Polynomial.derivative q) ≠ 0) : SignType.sign (Polynomial.eval z q) = SignType.sign (Polynomial.eval z (Polynomial.derivative q))

Vanishing member, right of c: copies the derivative's sign.

theorem BudanFourier.sign_eval_left_vanish {q : Polynomial ℝ} {a c z : ℝ} (hqc : Polynomial.eval c q = 0) (hzc : z < c) (haz : a ≤ z) (hq'no : ∀ w ∈ Set.Ico a c, Polynomial.eval w (Polynomial.derivative q) ≠ 0) : SignType.sign (Polynomial.eval z q) = -SignType.sign (Polynomial.eval z (Polynomial.derivative q))

Vanishing member, left of c: opposite of the derivative's sign.

The pure sign-list combinatorics (items 2+3, decoupled from polynomials)

The two off-c sign sequences are abstracted as list functions of the at-c sign list s (entry 0 = vanishing member, ±1 = kept). Building from the right with the item-1 recursions:

• Rseq (signs at b): a vanishing entry copies the value above it (headD);
• Lseq (signs at a): a vanishing entry negates the value above it. The right side collapses (signChanges (Rseq s) = signChanges s, i.e. V(b) = V(c)); the left side adds the leading-zero run plus an even surplus (the Budan–Fourier drop + parity).

def BudanFourier.Rseq : List SignType → List SignType

Signs just right of c: a vanishing member copies the sign above it.

Equations

• BudanFourier.Rseq [] = []
• BudanFourier.Rseq (σ :: rest) = if σ = 0 then (BudanFourier.Rseq rest).headD 0 :: BudanFourier.Rseq rest else σ :: BudanFourier.Rseq rest

def BudanFourier.Lseq : List SignType → List SignType

Signs just left of c: a vanishing member negates the sign above it.

Equations

• BudanFourier.Lseq [] = []
• BudanFourier.Lseq (σ :: rest) = if σ = 0 then -(BudanFourier.Lseq rest).headD 0 :: BudanFourier.Lseq rest else σ :: BudanFourier.Lseq rest

theorem BudanFourier.Rseq_spec (s : List SignType) : (∀ (h : s ≠ []), s.getLast h ≠ 0) → (∀ y ∈ Rseq s, y ≠ 0) ∧ (Rseq s).head? = (List.filter (fun (x : SignType) => decide (x ≠ 0)) s).head? ∧ Sturm.signChanges (Rseq s) = Sturm.signChanges s

Right side collapses to the at-c count. The vanishing members copy their kept successor, so they destutter away: signChanges (Rseq s) = signChanges s. (Also: Rseq s is all-nonzero and shares its leading surviving sign with s.) Needs the last entry nonzero (the leading coefficient never vanishes).

theorem BudanFourier.Rseq_length (s : List SignType) : (Rseq s).length = s.length

Rseq preserves length.

theorem BudanFourier.Lseq_length (s : List SignType) : (Lseq s).length = s.length

Lseq preserves length.

theorem BudanFourier.Lseq_spec (s : List SignType) : (∀ (h : s ≠ []), s.getLast h ≠ 0) → (∀ y ∈ Lseq s, y ≠ 0) ∧ (Lseq s).headD 0 = (-1) ^ (List.takeWhile (fun (x : SignType) => decide (x = 0)) s).length * (Rseq s).headD 0 ∧ ∃ (g : ℕ), Sturm.signChanges (Lseq s) = Sturm.signChanges (Rseq s) + (List.takeWhile (fun (x : SignType) => decide (x = 0)) s).length + 2 * g

Left side adds the leading-zero run plus an even surplus. The Budan–Fourier drop: the top vanishing block alternates (contributing its length = rootMult), interior blocks contribute an even amount. Carries the head sign-parity relation Lhead = (-1)^{leadingZeros} · Rhead as the induction invariant.

Plumbing: the polynomial tower realizes the abstract sign lists Rseq/Lseq

The two list lemmas Rseq_spec/Lseq_spec are stated about an abstract list of signs. Here we show that, for the derivative tower, the sign pattern at b (right of the critical point c) is Rseq of the pattern at c, and the pattern at a (left) is Lseq of it — the per-member recursion of the monotonicity lemmas, threaded up the tower via its derivative-chain structure.

theorem BudanFourier.iterate_derivative_natDegree_eval_ne {p : Polynomial ℝ} (hp : p ≠ 0) (x : ℝ) : Polynomial.eval x ((⇑Polynomial.derivative)^[p.natDegree] p) ≠ 0

The top derivative p^(deg p) is a nonzero constant, so it never vanishes.

theorem BudanFourier.fourierSeq_getLast {p : Polynomial ℝ} (h : fourierSeq p ≠ []) : (fourierSeq p).getLast h = (⇑Polynomial.derivative)^[p.natDegree] p

The last member of the Fourier sequence is p^(deg p).

theorem BudanFourier.fourierSeq_getLast_eval_ne {p : Polynomial ℝ} (hp : p ≠ 0) (x : ℝ) (h : fourierSeq p ≠ []) : Polynomial.eval x ((fourierSeq p).getLast h) ≠ 0

The last member of the Fourier sequence never vanishes.

theorem BudanFourier.fourierSeq_getElem? (p : Polynomial ℝ) (i : ℕ) (hi : i < p.natDegree + 1) : (fourierSeq p)[i]? = some ((⇑Polynomial.derivative)^[i] p)

The i-th member of the Fourier sequence is p^(i).

theorem BudanFourier.fourierSeq_isChain (p : Polynomial ℝ) : List.IsChain (fun (q q' : Polynomial ℝ) => q' = Polynomial.derivative q) (fourierSeq p)

The Fourier sequence is a derivative chain: each member is the derivative of the previous.

theorem BudanFourier.signs_right_eq_Rseq {c b : ℝ} (hcb : c < b) (L : List (Polynomial ℝ)) : List.IsChain (fun (q q' : Polynomial ℝ) => q' = Polynomial.derivative q) L → (∀ (h : L ≠ []), Polynomial.eval c (L.getLast h) ≠ 0) → (∀ q ∈ L, ∀ z ∈ Set.Ioc c b, Polynomial.eval z q ≠ 0) → List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval b q)) L = Rseq (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval c q)) L)

Right side = Rseq. For a derivative chain L whose last member is nonzero at c and none of whose members vanishes on (c, b], the sign pattern at b equals Rseq of the pattern at c.

theorem BudanFourier.signs_left_eq_Lseq {a c : ℝ} (hac : a < c) (L : List (Polynomial ℝ)) : List.IsChain (fun (q q' : Polynomial ℝ) => q' = Polynomial.derivative q) L → (∀ (h : L ≠ []), Polynomial.eval c (L.getLast h) ≠ 0) → (∀ q ∈ L, ∀ z ∈ Set.Ico a c, Polynomial.eval z q ≠ 0) → List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval a q)) L = Lseq (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval c q)) L)

Left side = Lseq. Symmetric to signs_right_eq_Rseq: the sign pattern at a (left of c) equals Lseq of the pattern at c.

theorem BudanFourier.takeWhile_eq_zero_length (l : List SignType) (r : ℕ) : r ≤ l.length → (∀ i < r, l[i]? = some 0) → (∀ (x : SignType), l[r]? = some x → x ≠ 0) → (List.takeWhile (fun (x : SignType) => decide (x = 0)) l).length = r

The leading-zero run of a sign list has the prescribed length. If the first r entries are 0 and entry r (when present) is nonzero, then takeWhile (· = 0) has length exactly r.

theorem BudanFourier.fourierVar_drop_at_critical_point {p : Polynomial ℝ} (hp : p ≠ 0) {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 ∈ fourierSeq p, ∀ z ∈ Set.Icc a b, Polynomial.eval z q = 0 → z = c) : ∃ (e : ℕ), fourierVar p a = fourierVar p b + (Multiset.filter (fun (x : ℝ) => a < x ∧ x ≤ b) p.roots).card + 2 * e

Local drop at a critical point — the analytic core. The one piece with no Sturm analogue: the derivative tower is not a coprime chain, so a whole block of consecutive members p^(i), …, p^(j) may vanish at c. Stated in additive form V(a) = V(b) + #roots(a,b] + 2e, which packages BOTH the Budan–Fourier inequality #roots ≤ V(a)−V(b) and the even-difference parity into a single existential that adds cleanly across the global induction (the locally-constant case is e = 0, #roots = 0).

theorem BudanFourier.budan_fourier (p : Polynomial ℝ) (hp : p ≠ 0) {a b : ℝ} (hab : a < b) (ha : Polynomial.eval a p ≠ 0) (hb : Polynomial.eval b p ≠ 0) : (Multiset.filter (fun (x : ℝ) => a < x ∧ x ≤ b) p.roots).card ≤ fourierVar p a - fourierVar p b ∧ Even (fourierVar p a - fourierVar p b - (Multiset.filter (fun (x : ℝ) => a < x ∧ x ≤ b) p.roots).card)

The Budan–Fourier theorem. For nonzero p and a < b with neither endpoint a root, the number of real roots of p in (a, b] counted with multiplicity is bounded by the drop in Fourier sign variations, and has the same parity as that drop.

Proof: strong induction on the number of distinct critical points (roots of the tower's product Pc) in (a, b]; peel the maximum one, split just below it, recurse left and apply the local drop fourierVar_drop_at_critical_point on the right, combining the two additive existentials.

theorem BudanFourier.not_sturm_at_multiple_root {p : Polynomial ℝ} {r : ℝ} (hr : 1 < Polynomial.rootMultiplicity r p) : 2 < (fourierSeq p).length ∧ Polynomial.eval r (Polynomial.derivative p) = 0 ∧ Polynomial.eval r p * Polynomial.eval r ((⇑Polynomial.derivative)^[2] p) = 0

The derivative tower is not a Sturm chain. An abstract Sturm chain (Eisermann, Def. 3.10) asks that whenever an interior member vanishes at a point, its two neighbours there have product < 0. At a root r of multiplicity at least 2, the member p' (index 1 of fourierSeq p) is interior, since the tower has at least three members, and vanishes at r; yet the product of its neighbours p (r) * p'' (r) is 0, because p vanishes at r too.

theorem BudanFourier.not_sturm_example : Polynomial.eval 1 (Polynomial.derivative ((Polynomial.X - Polynomial.C 1) ^ 2 * (Polynomial.X + Polynomial.C 1))) = 0 ∧ Polynomial.eval 1 ((Polynomial.X - Polynomial.C 1) ^ 2 * (Polynomial.X + Polynomial.C 1)) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[2] ((Polynomial.X - Polynomial.C 1) ^ 2 * (Polynomial.X + Polynomial.C 1))) = 0

The paper's witness: for p_A = (x - 1)^2 (x + 1), the interior member p_A' vanishes at x = 1 and p_A (1) * p_A'' (1) = 0, so the antipodal axiom fails there.