Cylindrical algebraic decomposition by recursive Lazard projection

Every finite family of real polynomials in n variables has a cylindrical algebraic decomposition of ℝ ^ n into analytic submanifolds on each cell of which every member has constant Lazard valuation, and hence constant sign. No well-orientedness or nonnullification hypothesis is needed: this is the validity of Lazard's projection-and-lifting method.

In the ambient convention of TauCeti.IsCAD, coordinate zero is the coordinate added by the last lifting step and Fin.tail projects to the base. The coordinate added first is therefore coordinate n - 1. The Lazard valuation is taken in the order in which Lazard evaluation treats the coordinates during the recursion, from the coordinate added first to the one added last: this is the reversed coordinate order Fin.revPerm, in which coordinate n - 1 is the most significant. Lazard valuation is not invariant under permutations of the coordinates, so this order is part of the statement.

The construction is the recursion of McCallum–Parusiński–Paunescu. A family in n + 1 variables is rewritten with its coordinates reversed and its new coordinate as distinguished variable, and an irreducible basis of the result is chosen. The recursion is applied to its Lazard projection with the base coordinates reversed back. On each base cell, read with its coordinates reversed, the Lazard projection is then valuation-invariant in the native order, so the Lazard lifting theorem gives a Lazard delineation of the family over the reordered cell. Pulling these delineations back to the original base cells gives the lifted decomposition. Sign-invariance follows from valuation-invariance on the connected cells.

Main results

• TauCeti.exists_isCAD_lazardValuationReindex_eq: every finite family has an analytic cylindrical algebraic decomposition on whose cells each member is Lazard valuation-invariant in the reversed coordinate order and sign-invariant.

References

• D. Lazard, An improved projection for cylindrical algebraic decomposition, in Algebraic Geometry and its Applications, Springer (1994), 467–476.
• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Section 5 and Theorem 5.1.

theorem TauCeti.exists_isCAD_lazardValuationReindex_eq {n : ℕ} (F : Finset (MvPolynomial (Fin n) ℝ)) : ∃ (𝓒 : Set (Set (Fin n → ℝ))), IsCAD n 𝓒 ∧ (∀ E ∈ 𝓒, ∃ (d : ℕ), IsAnalyticSubmanifold d E) ∧ (∀ f ∈ F, ∀ E ∈ 𝓒, ∀ x ∈ E, ∀ y ∈ E, f.lazardValuationReindex Fin.revPerm x = f.lazardValuationReindex Fin.revPerm y) ∧ ∀ f ∈ F, ∀ E ∈ 𝓒, SignInvariant (fun (x : Fin n → ℝ) => (MvPolynomial.eval x) f) E

Validity of Lazard's projection. Every finite family of real polynomials in n variables has a cylindrical algebraic decomposition of ℝ ^ n into analytic submanifolds on each cell of which every member has constant Lazard valuation, when the coordinates are read in reverse order, from the coordinate added first by the cylindrical structure to the one added last. Every member is also sign-invariant on each cell. No well-orientedness hypothesis is imposed, and members may be nullified over base cells of positive dimension.