Recursive sign-invariant McCallum decompositions

Construct a sign-invariant CAD with analytic cells when the McCallum projection is well-oriented. The top-level basis may be any squarefree, pairwise relatively prime primitive basis. Recursive order-invariant decomposition is applied to the projection, and sign-invariant lifting is used at the final level. Thus the input basis may be nullified on positive-dimensional base cells; the finite-nullification condition is required only at the lower levels. The resulting CAD retains order-invariance of the projection on its base cells.

In three variables the projection is bivariate and hence always well-oriented. Consequently McCallum projection gives a sign-invariant analytic CAD for every three-variable family, even without a well-orientedness hypothesis on that family.

References

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

theorem TauCeti.exists_isCAD_signInvariant_of_isMcCallumWellOriented_projection {n : ℕ} (polynomialGCD : (m : ℕ) → NormalizedGCDMonoid (MvPolynomial (Fin m) ℝ)) {F : Finset (MvPolynomial (Fin (n + 1)) ℝ)} {B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} (_hB : (Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).IsSquarefreeBasis B) (_hproj : IsMcCallumWellOriented polynomialGCD n ((Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).mcCallumProjection B)) : ∃ (𝒞 : Set (Set (Fin (n + 1) → ℝ))), IsCAD (n + 1) 𝒞 ∧ (∀ E ∈ 𝒞, ∃ (d : ℕ), IsAnalyticSubmanifold d E) ∧ (∀ f ∈ F, ∀ E ∈ 𝒞, SignInvariant (fun (x : Fin (n + 1) → ℝ) => (MvPolynomial.eval x) f) E) ∧ ∀ q ∈ (Finset.map (MvPolynomial.finSuccEquiv ℝ n).toEmbedding F).mcCallumProjection B, ∀ C ∈ Set.image Fin.tail '' 𝒞, ∀ x ∈ C, ∀ y ∈ C, q.orderAt x = q.orderAt y

Recursive sign-invariant McCallum correctness. If the McCallum projection of a squarefree basis of F is well-oriented, there is a sign-invariant CAD for F with analytic cells. Its base CAD is order-invariant for that projection. No restriction is imposed on nullification of the top-level basis, including over positive-dimensional base cells.