Sign-invariant McCallum lifting with nullified members

Over a connected semialgebraic analytic base on which the McCallum projection is order-invariant, construct a sign-invariant semialgebraic stack for the original family. No nonnullification hypothesis is required: coefficient orders make nullification constant on the base, and only the nonnullified basis members participate in root lifting. The remaining members vanish on the entire cylinder. Contents are retained when reconstructing input signs.

This is suitable for the final lift of a sign-invariant CAD. It does not assert ambient order-invariance on the lifted cells, which nullified members need not satisfy, and thus cannot replace order-invariant lifting at intermediate levels.

Nor can its hypothesis be weakened to sign-invariance of the projection. For the squarefree cubic (T - 1)² (T - 1 - x₀²) + x₁ over the line x₁ = 0, the McCallum projection is sign-invariant, its discriminant vanishing identically there, but the two fibre roots 1 and 1 + x₀² merge at the origin, and no stack over the line makes the cubic sign-invariant (TauCeti.exists_signInvariant_mcCallumProjection_stackCells_not_signInvariant). So on the lower levels of a CAD built by McCallum projection, sign-invariance cannot replace order-invariance.

Main results

• Finset.IsSquarefreeBasis.exists_isSemialgebraicStack_signInvariant_of_mcCallumProjection: sign-invariant lifting over a base on which the McCallum projection is order-invariant.
• TauCeti.exists_signInvariant_mcCallumProjection_stackCells_not_signInvariant: sign-invariance of the McCallum projection does not suffice.

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 Finset.IsSquarefreeBasis.exists_isSemialgebraicStack_signInvariant_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) (hsemi : TauCeti.IsSemialgebraic S) (hproj : ∀ q ∈ F.mcCallumProjection B, ∀ x ∈ S, ∀ y ∈ S, q.orderAt x = q.orderAt y) : ∃ (k : ℕ) (θ : Fin k → ↑S → ℝ), TauCeti.IsSemialgebraicStack S θ ∧ ∀ E ∈ TauCeti.stackCells S θ, (∃ (e : ℕ), (e = d ∨ e = d + 1) ∧ TauCeti.IsAnalyticSubmanifold e E) ∧ ∀ f ∈ F, TauCeti.SignInvariant (fun (y : Fin (n + 1) → ℝ) => (MvPolynomial.eval y) ((MvPolynomial.finSuccEquiv ℝ n).symm f)) E

Final sign-invariant McCallum lifting. Order-invariance of the projection on a preconnected semialgebraic analytic submanifold gives a semialgebraic stack with analytic cells on which every input is sign-invariant. Basis members may be nullified, even on a positive-dimensional base; no ambient-order conclusion is asserted for the lifted inputs.

Sign-invariance of the projection does not suffice

theorem TauCeti.exists_signInvariant_mcCallumProjection_stackCells_not_signInvariant (polynomialGCD : NormalizedGCDMonoid (MvPolynomial (Fin 2) ℝ)) : ∃ (f : Polynomial (MvPolynomial (Fin 2) ℝ)) (S : Set (Fin 2 → ℝ)), {f}.IsSquarefreeBasis {f} ∧ IsSemialgebraic S ∧ IsAnalyticSubmanifold 1 S ∧ IsConnected S ∧ (∀ x ∈ S, Polynomial.map (MvPolynomial.eval x) f ≠ 0) ∧ (∀ q ∈ {f}.mcCallumProjection {f}, SignInvariant (fun (x : Fin 2 → ℝ) => (MvPolynomial.eval x) q) S) ∧ (∃ q ∈ {f}.mcCallumProjection {f}, ∃ x ∈ S, ∃ y ∈ S, q.orderAt x ≠ q.orderAt y) ∧ ∀ (k : ℕ) (θ : Fin k → ↑S → ℝ), (∀ (x : ↑S), StrictMono fun (i : Fin k) => θ i x) → ∃ E ∈ stackCells S θ, ¬SignInvariant (fun (y : Fin (2 + 1) → ℝ) => (MvPolynomial.eval y) ((MvPolynomial.finSuccEquiv ℝ 2).symm f)) E

Sign-invariance of the McCallum projection does not suffice for lifting. In Finset.IsSquarefreeBasis.exists_isSemialgebraicStack_signInvariant_of_mcCallumProjection, the hypothesis that the McCallum projection is order-invariant on the base cannot be weakened to sign-invariance, even for a nonnullified squarefree basis over a connected semialgebraic analytic submanifold. So a lower level of a CAD that is merely sign-invariant for the projection cannot replace an order-invariant one.

Explicitly, let f = (T - 1)² (T - 1 - x₀²) + x₁, a monic cubic in the distinguished variable T over ℝ[x₀, x₁], and let S ⊆ ℝ ^ 2 be the line x₁ = 0. As f is squarefree, it is its own squarefree basis. Over S its coefficients 1, -(3 + x₀²), 3 + 2 x₀² and -(1 + x₀²) have constant signs, its content is 1, and its discriminant vanishes, because each fibre (T - 1)² (T - 1 - x₀²) has a double root. So the McCallum projection of {f} is sign-invariant on S, and some member of it has nonconstant order on S; since the other members do not vanish on S, this is the discriminant. But the fibre has the two roots 1 and 2 over (1, 0) and the single root 1 over the origin. In the coordinates (T, x₀, x₁), every cell of a stack over S lies over all of S, so the cells through the zeros (1, 1, 0) and (2, 1, 0) of f would both contain its only zero (1, 0, 0) over the origin, hence coincide, and then also contain (3 / 2, 1, 0), where f is negative. So no stack over S, given by pointwise strictly increasing functions, continuous or not, has f sign-invariant on each cell.