McCallum lifting over an order-invariant base

A squarefree polynomial basis, in particular an irreducible basis, is analytically delineable over a connected analytic submanifold when none of its fibers is nullified and the McCallum projection is order-invariant there. Every input polynomial reconstructed from the basis then has constant ambient order, and hence constant sign, on every section and sector of the resulting stack.

This is the non-nullified lifting step of McCallum's projection-correctness argument, used at each positive-dimensional cell whose base is already order-invariant for the projection. Nullified fibers over zero-dimensional cells are not covered; they require refinement by delineating polynomials.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Sections 2–3.

theorem TauCeti.exists_delineation_orderAt_prod_eq_of_mcCallumProjection {n d : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (hB : F.IsSquarefreeBasis B) {A : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} (hAB : A ⊆ B) (hS : IsAnalyticSubmanifold d S) (hconn : IsPreconnected S) (hfiber : ∀ b ∈ A, ∀ x ∈ S, Polynomial.map (MvPolynomial.eval x) b ≠ 0) (hproj : ∀ q ∈ F.mcCallumProjection B, ∀ x ∈ S, ∀ y ∈ S, q.orderAt x = q.orderAt y) : ∃ (D : Delineation fun (b : ↥A) (x : ↑S) => Polynomial.map (MvPolynomial.eval ↑x) ↑b), ∀ (i : Fin D.count) (x y : ↑S), ((MvPolynomial.finSuccEquiv ℝ n).symm (∏ b : ↥A, ↑b)).orderAt (Fin.cons (D.root i x) ↑x) = ((MvPolynomial.finSuccEquiv ℝ n).symm (∏ b : ↥A, ↑b)).orderAt (Fin.cons (D.root i y) ↑y)

Any nonnullified subfamily of a squarefree basis has a common delineation over a preconnected analytic submanifold on which the original McCallum projection is order-invariant. The product of the subfamily has constant ambient order along each section. Nullified members outside the subfamily cause no obstruction.

theorem Finset.IsSquarefreeBasis.exists_delineation_orderAt_eq_of_mcCallumProjection {n d : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (hB : F.IsSquarefreeBasis B) (hS : TauCeti.IsAnalyticSubmanifold d S) (hconn : IsPreconnected S) (hfiber : ∀ b ∈ B, ∀ x ∈ S, Polynomial.map (MvPolynomial.eval x) b ≠ 0) (hproj : ∀ q ∈ F.mcCallumProjection B, ∀ x ∈ S, ∀ y ∈ S, q.orderAt x = q.orderAt y) : ∃ (D : TauCeti.Delineation fun (b : ↥B) (x : ↑S) => Polynomial.map (MvPolynomial.eval ↑x) ↑b), ∀ E ∈ TauCeti.stackCells S D.root, (∃ (e : ℕ), (e = d ∨ e = d + 1) ∧ TauCeti.IsAnalyticSubmanifold e E) ∧ ∀ f ∈ F, (∀ y ∈ E, ∀ y' ∈ E, ((MvPolynomial.finSuccEquiv ℝ n).symm f).orderAt y = ((MvPolynomial.finSuccEquiv ℝ n).symm f).orderAt y') ∧ TauCeti.SignInvariant (fun (y : Fin (n + 1) → ℝ) => (MvPolynomial.eval y) ((MvPolynomial.finSuccEquiv ℝ n).symm f)) E

McCallum lifting over an order-invariant base. If a squarefree basis has no nullified fiber over a connected analytic submanifold and every member of its McCallum projection has constant ambient order there, then the basis has a common delineation. Every stack cell is an analytic submanifold, and every original input has constant ambient order and sign on that cell.