Roots That Are Always There: the Virtual Roots of a Real Polynomial, Machine-Checked in Lean 4

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_{d,1} ≤ … ≤ rho_{d,d}: 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 R_d construction (an |p|-minimiser on each cell where p' keeps a constant sign), the count (exactly d of them), sortedness and the bracketing interval, R_d capturing actual roots, and the Rolle interlacing rho_{d,r}(p) ≤ rho_{d-1,r}(p') ≤ rho_{d,r+1}(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_vroots_Ioc_eq_fourierVar), 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.