Counting with the Derivative Tower: the Budan-Fourier Theorem, Machine-Checked in Lean 4

A machine-checked, sorry-free proof, in Lean 4 over Mathlib, of the Budan-Fourier theorem: for a nonzero real polynomial p and a < b with p(a), p(b) ≠ 0, the number of real roots of p in (a, b] counted with multiplicity is at most the drop V(a) − V(b) in the sign variations of the derivative tower p, p′, p″, …, and the difference V(a) − V(b) − #roots is even. The even surplus is the fingerprint of the complex roots the interval cannot see; the b → ∞ shadow is Descartes' rule of signs, which the same engine reaches through the identity fourierVar(p, 0) = Polynomial.signVariations p, Mathlib's own coefficient sign count. The contribution is the formalization: to the best of the author's knowledge the first Budan-Fourier theorem in Lean (not first in any system — a prior Isabelle/HOL formalization is by W. Li). It runs on the same sign-variation engine as the companion Sturm formalization, but its local analysis must resolve a whole vanishing block of the derivative tower at once — the tower is not a coprime (Sturm) chain at a multiple root — handled by the Rseq/Lseq block law. The headline theorem depends only on the three standard axioms (propext, Classical.choice, Quot.sound). This is the Budan-Fourier paper of the godsil-gutman-lean series (real-root-counting strand: Newton's inequalities, Sturm, Budan-Fourier). English and Spanish versions are included. Formalized with AI assistance (Claude, Anthropic); the mathematics and all claims are the author's responsibility.