Validity proof of Lazard's method for CAD construction

TL;DR

This paper provides a complete proof of Lazard's improved CAD construction method, which is more broadly applicable and potentially more efficient than previous methods, by leveraging classical valuation and Puiseux's theorem.

Contribution

It offers a full validity proof of Lazard's CAD method, addressing previous gaps and demonstrating its wider applicability and efficiency.

Findings

Complete validity proof of Lazard's method provided

Lazard's method applies to any polynomial family without coordinate assumptions

Potential for more efficient CAD construction methods

Abstract

In 1994 Lazard proposed an improved method for cylindrical algebraic decomposition (CAD). The method comprised a simplified projection operation together with a generalized cell lifting (that is, stack construction) technique. For the proof of the method's validity Lazard introduced a new notion of valuation of a multivariate polynomial at a point. However a gap in one of the key supporting results for his proof was subsequently noticed. In the present paper we provide a complete validity proof of Lazard's method. Our proof is based on the classical parametrized version of Puiseux's theorem and basic properties of Lazard's valuation. This result is significant because Lazard's method can be applied to any finite family of polynomials, without any assumption on the system of coordinates. It therefore has wider applicability and may be more efficient than other projection and lifting schemes for CAD.