Validity proof of Lazard's method for CAD construction (Q1757004)

The authors provide a proof of Lazard's method for cylindrical algebraic decomposition. This method was introduced by \textit{D. Lazard} [in: Algebraic geometry and its applications. Collections of papers from Shreeram S. Abhyankar's 60th birthday conference held at Purdue University, West Lafayette, IN, USA, June 1-4, 1990. New York: Springer-Verlag. 467--476 (1994; Zbl 0822.68118)]. It can be applied to any finite family of polynomials, without any assumption on the system of coordinates. The method therefore has wider applicability and may be more efficient than other projection and lifting schemes for cylindrical algebraic decomposition. However, the proof presented in the aforementioned article was not complete due to a gap in one of the key supporting results. In [\textit{S. McCallum} and \textit{H. Hong}, J. Symb. Comput. 72, 65--81 (2016; Zbl 1325.13026)] it was shown that Lazard's projection is valid for cylindrical algebraic decomposition construction for so-called well oriented polynomial sets. The present article provides a complete validity proof of Lazard's method using Lazard's notion of valuation. The proof is based on the classical parametrized version of Puiseux's theorem and basic properties of Lazard's valuation.