Semialgebraicity of Lazard stacks

Every Lazard delineation of a real polynomial family over a semialgebraic base has semialgebraic sections and sectors. Its fixed removed base exponents express the Lazard evaluations as specializations of polynomial families. Choose one witnessing member for each section to obtain a finite family with exactly the same shared roots. The uniform descriptions of shared ordered roots then describe each cell by its root membership and the number of roots below it.

Ordinary fibers may be nullified, and the degrees of the Lazard evaluations need not be constant. Neither connectedness nor an analytic submanifold hypothesis is needed here. This supplies the semialgebraic cells required when lifting a cylindrical decomposition using Lazard evaluations rather than ordinary specialization.

References

S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Sections 2 and 5. S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapters 10–11 (uniform sign descriptions of ordered roots).

theorem TauCeti.LazardDelineation.isSemialgebraicStack {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hS : IsSemialgebraic S) : IsSemialgebraicStack S D.root

A Lazard delineation over a semialgebraic base is a semialgebraic stack, even where the ordinary fibers are nullified. Repeated and shared roots are counted once, and zero members and an empty root list are allowed. The input family may be infinite: one witnessing member per section suffices to describe the cells.