Ambient order in a McCallum family stack

Suppose a squarefree basis has a common delineation over a preconnected base. If the ambient order of the product of the basis members is constant on every root section, then the ambient order of each basis member is constant there as well. This is a topological consequence of product order constancy: a factor's order can only jump upwards, and the sum of all factor orders is fixed. The content and basis factorization then give constant ambient order for every original input. On sectors the order is determined by content alone.

This transfers the conclusion of a single-polynomial discriminant theorem for the active basis product to the whole family. The hypothesis concerns ambient Taylor order in all variables. Fiber root multiplicity is not a substitute for it. Members of the basis must have nonzero fibers over the base, as in well-oriented McCallum lifting; contents and original inputs may vanish.

References

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

theorem Finset.IsSquarefreeBasis.orderAt_eq_of_prod_delineation {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (hB : F.IsSquarefreeBasis B) (hS : IsPreconnected S) (D : TauCeti.Delineation fun (b : ↥B) (x : ↑S) => Polynomial.map (MvPolynomial.eval ↑x) ↑b) (hfiber : ∀ b ∈ B, ∀ x ∈ S, Polynomial.map (MvPolynomial.eval x) b ≠ 0) (hcontent : ∀ f ∈ F, ∀ x ∈ S, ∀ y ∈ S, f.content.orderAt x = f.content.orderAt y) (hprod : ∀ (i : Fin D.count), ∀ a ∈ TauCeti.cylinder S '' TauCeti.sectionSet D.root i, ∀ a' ∈ TauCeti.cylinder S '' TauCeti.sectionSet D.root i, (∏ b ∈ B, (MvPolynomial.finSuccEquiv ℝ n).symm b).orderAt a = (∏ b ∈ B, (MvPolynomial.finSuccEquiv ℝ n).symm b).orderAt a') (E : Set (Fin (n + 1) → ℝ)) : E ∈ TauCeti.stackCells S D.root → ∀ f ∈ F, (∀ a ∈ E, ∀ a' ∈ E, ((MvPolynomial.finSuccEquiv ℝ n).symm f).orderAt a = ((MvPolynomial.finSuccEquiv ℝ n).symm f).orderAt a') ∧ TauCeti.SignInvariant (fun (a : Fin (n + 1) → ℝ) => (MvPolynomial.eval a) ((MvPolynomial.finSuccEquiv ℝ n).symm f)) E

If the active basis product has constant ambient order on each section of a common delineation, then every original input has constant ambient order and sign on every stack cell. Content order is required to be constant on the base, and basis fibers must be nonzero. The product order need only be controlled on sections: on sectors, every basis member has ambient order zero.