A synthesis note, companion to the Budan-Fourier formalization, showing in Lean 4 over Mathlib that Descartes' rule, Sturm's theorem and the Budan-Fourier theorem are three instances of one sign-variation engine and one local-drop law V (c-) = V (c+) + muc + 2e. It does three things, all sorry-free: (1) exhibits the shared engine (a sign-variation count, locally constant off critical points, telescoping over (a, b]) and runs all three counts through it — the first Lean formalizations of Sturm and of Budan-Fourier, plus the bridge fourierVar (p, 0) = Polynomial. signVariations p tying the engine's V (0) to Mathlib's own Descartes count; (2) states their common local-drop law; (3) locates the exact axiom where the three diverge — Eisermann's Sturm-chain axiom forbids two consecutive members vanishing together, and the derivative tower violates it at every multiple root, so the tower is not a Sturm chain, its local law being the block collapse/alternation (Rseq/Lseq). The unification is classical (Akritas; Basu-Pollack-Roy; the Cauchy index and Eisermann's abstract Sturm chains; the Cauchy-index route machine-checked in Isabelle/HOL by Li and Paulson). The contribution is the explicit shared Lean engine, the two first-in-Lean formalizations it carries, the Descartes bridge to Mathlib, and the precise axiomatic placement of the derivative tower. Headline results depend only on the three standard axioms (propext, Classical. choice, Quot. sound). English and Spanish versions included. Formalized with AI assistance (Claude, Anthropic) ; the mathematics and all claims are the author's responsibility.
CARLES MARÍN MUÑOZ (Wed,) studied this question.