Final sign-invariant CAD lifting by McCallum projection

Lift an analytic CAD adapted to the ambient orders of a McCallum projection to a sign-invariant CAD for the original family. The projection of the new CAD is exactly the supplied base CAD, and every lifted cell is an analytic submanifold. Basis members nullified on a base cell are omitted from its root stack and have sign zero throughout its cylinder.

Unlike an intermediate order-invariant lift, this final sign-invariant lift needs no well-orientedness assumption at the top level. The lower CAD must still be order-invariant for the projection; mere sign-invariance of that projection does not suffice (TauCeti.exists_signInvariant_mcCallumProjection_stackCells_not_signInvariant).

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Sections 2–3.
• C. W. Brown, The McCallum projection, lifting, and order-invariance (2005).

theorem TauCeti.IsCAD.exists_isCAD_signInvariant_of_mcCallumProjection {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {𝒟 : Set (Set (Fin n → ℝ))} (h𝒟 : IsCAD n 𝒟) (hB : F.IsSquarefreeBasis B) (hanalytic : ∀ C ∈ 𝒟, ∃ (d : ℕ), IsAnalyticSubmanifold d C) (hproj : ∀ q ∈ F.mcCallumProjection B, ∀ C ∈ 𝒟, ∀ x ∈ C, ∀ y ∈ C, q.orderAt x = q.orderAt y) : ∃ (𝒞 : Set (Set (Fin (n + 1) → ℝ))), IsCAD (n + 1) 𝒞 ∧ Set.image Fin.tail '' 𝒞 = 𝒟 ∧ ∀ E ∈ 𝒞, (∃ (e : ℕ), IsAnalyticSubmanifold e E) ∧ ∀ f ∈ F, SignInvariant (fun (y : Fin (n + 1) → ℝ) => (MvPolynomial.eval y) ((MvPolynomial.finSuccEquiv ℝ n).symm f)) E

Final sign-invariant CAD lifting. An analytic base CAD that is order-invariant for McCallum's projection of a squarefree basis lifts to a sign-invariant CAD for the original family, with analytic cells and exactly the given base projections. Nullified basis members are allowed at this final level, including over positive-dimensional cells.