A machine-checked, sorry-free formalization, in Lean 4 over Mathlib, of the virtual roots of a real polynomial (Gonzalez-Vega, Lombardi and Mahe; Coste, Lajous, Lombardi and Roy). A real polynomial of degree d may have fewer than d real roots, but it always has exactly d virtual roots rho₃, ₁ ≤ … ≤ rho₃, ₃: continuous semialgebraic substitutes that coincide with the real roots when these exist and otherwise sit where the polynomial comes closest to vanishing. The development covers the structural theory — the recursive Rd construction (an |p|-minimiser on each cell where p' keeps a constant sign), the count (exactly d of them), sortedness and the bracketing interval, Rd capturing actual roots, and the Rolle interlacing rho₃, ₑ (p) ≤ rho₃-₁, ₑ (p') ≤ rho₃, ₑ+₁ (p) — and, built on it, the exact Budan-Fourier count: the number of virtual roots in (a, b] equals the sign-variation drop V (a) − V (b) of the derivative tower (cardᵥrootsIocₑqfourierVar), turning the classical Budan-Fourier inequality into an equality — the surplus was never a defect of the count, only of which roots one was counting. The contribution is the formalization: to the best of the author's knowledge, neither virtual roots nor this exact count through them had been formalized in any interactive theorem prover before (searches of Mathlib, Coq mathcomp-real-closed, the Isabelle AFP, and HOL Light). Headline theorems depend only on the three standard axioms (propext, Classical. choice, Quot. sound). Part of the godsil-gutman-lean series (real-root-counting strand: Newton, Sturm, Budan-Fourier, virtual roots). 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.