Lifting cylindrical decompositions by Lazard delineations

A cylindrical algebraic decomposition of the base lifts through a family of Lazard delineations, one over each base cell. The resulting sections and sectors are semialgebraic, form a cylindrical algebraic decomposition of the cylinder, and remain analytic submanifolds when the base cells are analytic submanifolds.

The Lazard valuation of every input is constant on each lifted cell when the new cylinder coordinate is read last, as required by Lazard evaluation. In the ambient CAD convention the new coordinate is coordinate zero. Rotating the input variables reconciles these conventions; the rotated inputs are sign-invariant, and MvPolynomial.lazardValuationReindex records the inverse rotation in their valuation, on every lifted cell.

The delineation over a base cell may also be given in a reordered presentation of the base: over the cell read through a permutation of its coordinates. The stacks are then pulled back to the original cells, and the Lazard valuation is constant when the base coordinates are read through that permutation. This is how a recursive construction, whose base valuations are taken in a coordinate order other than the native one, feeds its base cells to Lazard lifting. Constant Lazard valuation in any coordinate order gives sign-invariance on connected sets.

This is the CAD-level assembly step in Lazard's projection-and-lifting construction. The separate analytic lifting theorem supplies the Lazard delineation over each base cell.

Main results

• TauCeti.IsCAD.exists_isCAD_lazardValuation_eq_of_lazardDelineation_reindex: lifting a CAD through Lazard delineations over its cells read in a permuted coordinate order.
• TauCeti.IsCAD.exists_isCAD_lazardValuation_eq_of_lazardDelineation: lifting a CAD through Lazard delineations over its cells in the native coordinate order.

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.

theorem TauCeti.IsCAD.exists_isCAD_lazardValuation_eq_of_lazardDelineation_reindex {n : ℕ} {ι : Type u_1} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {𝓓 : Set (Set (Fin n → ℝ))} (h𝓓 : IsCAD n 𝓓) (e : Equiv.Perm (Fin n)) (hanalytic : ∀ C ∈ 𝓓, ∃ (d : ℕ), IsAnalyticSubmanifold d C) (hD : ∀ C ∈ 𝓓, Nonempty (LazardDelineation F ((fun (x : Fin n → ℝ) => x ∘ ⇑(Equiv.symm e)) ⁻¹' C))) : ∃ (𝓒 : Set (Set (Fin (n + 1) → ℝ))), IsCAD (n + 1) 𝓒 ∧ Set.image Fin.tail '' 𝓒 = 𝓓 ∧ (∀ E ∈ 𝓒, ∃ (d : ℕ), IsAnalyticSubmanifold d E) ∧ ∀ (k : ι), ∀ E ∈ 𝓒, ∀ x ∈ E, ∀ y ∈ E, (F k).lazardValuation (Fin.snoc (Fin.tail x ∘ ⇑e) (x 0)) = (F k).lazardValuation (Fin.snoc (Fin.tail y ∘ ⇑e) (y 0))

CAD lifting by Lazard delineations in a reordered base. Suppose every cell C of a cylindrical algebraic decomposition of ℝ ^ n is an analytic submanifold, and its reordering (· ∘ e.symm) ⁻¹' C by a permutation e of the base coordinates carries a Lazard delineation of a fixed polynomial family. Then the stacks of those delineations, pulled back to the original cells, form a cylindrical algebraic decomposition of ℝ ^ (n + 1) with the original decomposition as its projection.

Every lifted cell is an analytic submanifold. On it, every family member has constant Lazard valuation when the base coordinates are read through e and the new coordinate is read last.

theorem TauCeti.IsCAD.exists_isCAD_lazardValuation_eq_of_lazardDelineation {n : ℕ} {ι : Type u_1} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {𝓓 : Set (Set (Fin n → ℝ))} (h𝓓 : IsCAD n 𝓓) (hanalytic : ∀ C ∈ 𝓓, ∃ (d : ℕ), IsAnalyticSubmanifold d C) (hD : ∀ C ∈ 𝓓, Nonempty (LazardDelineation F C)) : ∃ (𝓒 : Set (Set (Fin (n + 1) → ℝ))), IsCAD (n + 1) 𝓒 ∧ Set.image Fin.tail '' 𝓒 = 𝓓 ∧ (∀ E ∈ 𝓒, ∃ (d : ℕ), IsAnalyticSubmanifold d E) ∧ (∀ (k : ι), ∀ E ∈ 𝓒, ∀ x ∈ E, ∀ y ∈ E, ((MvPolynomial.rename ⇑(finRotate (n + 1))) (F k)).lazardValuationReindex (Equiv.symm (finRotate (n + 1))) x = ((MvPolynomial.rename ⇑(finRotate (n + 1))) (F k)).lazardValuationReindex (Equiv.symm (finRotate (n + 1))) y) ∧ ∀ (k : ι), ∀ E ∈ 𝓒, SignInvariant (fun (x : Fin (n + 1) → ℝ) => (MvPolynomial.eval x) ((MvPolynomial.rename ⇑(finRotate (n + 1))) (F k))) E

CAD lifting by Lazard delineations. Suppose every cell of a cylindrical algebraic decomposition of ℝ ^ n is an analytic submanifold and carries a Lazard delineation of a fixed polynomial family. Then the stacks of those delineations form a cylindrical algebraic decomposition of ℝ ^ (n + 1) with the original decomposition as its projection.

Every lifted cell is an analytic submanifold. For each rotated family member, its valuation in the coordinate order given by the inverse rotation is constant there, and the same rotated member is sign-invariant in the ambient coordinate order.