Ambient polynomial orders on sectors

On a sector of a polynomial delineation, every member with a nonzero fiber has nonzero value, hence ambient Taylor order zero. For a squarefree basis whose fibers are nonzero, the ambient order of each original input on a sector is therefore exactly the order of its content at the base point. This includes inputs nullified by vanishing content: their ambient order need not be zero.

Consequently order-invariance of the McCallum projection gives order-invariance of the original family on every sector. Neither connectedness nor analyticity is needed for this implication. The order on root sections requires a separate argument; fiber root multiplicity is not identified with ambient Taylor order.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Sections 2–3 (content and order-invariant lifting).

theorem TauCeti.Delineation.orderAt_eq_zero_of_mem_sectorSet {n : ℕ} {ι : Type u_1} {P : ι → Polynomial (MvPolynomial (Fin n) ℝ)} {S : Set (Fin n → ℝ)} (D : Delineation fun (i : ι) (x : ↑S) => Polynomial.map (MvPolynomial.eval ↑x) (P i)) (i : ι) {j : Fin (D.count + 1)} {a : Fin (n + 1) → ℝ} (hi : Polynomial.map (MvPolynomial.eval (Fin.tail a)) (P i) ≠ 0) (ha : a ∈ cylinder S '' sectorSet D.root j) : ((MvPolynomial.finSuccEquiv ℝ n).symm (P i)).orderAt a = 0

A member with a nonzero fiber has ambient Taylor order zero at every point of a sector of its delineation. Only nonnullification at that point is needed.

theorem Finset.IsSquarefreeBasis.orderAt_eq_content_of_mem_sectorSet {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (hB : F.IsSquarefreeBasis B) (D : TauCeti.Delineation fun (b : ↥B) (x : ↑S) => Polynomial.map (MvPolynomial.eval ↑x) ↑b) {f : Polynomial (MvPolynomial (Fin n) ℝ)} (hf : f ∈ F) {j : Fin (D.count + 1)} {a : Fin (n + 1) → ℝ} (hb : ∀ b ∈ B, Polynomial.map (MvPolynomial.eval (Fin.tail a)) b ≠ 0) (ha : a ∈ TauCeti.cylinder S '' TauCeti.sectorSet D.root j) : ((MvPolynomial.finSuccEquiv ℝ n).symm f).orderAt a = f.content.orderAt (Fin.tail a)

On a sector of a delineation of the basis, the ambient order of an input is exactly the order of its content. All basis fibers at the base point are assumed nonzero; the input itself may be nullified by its content.

theorem Finset.IsSquarefreeBasis.orderAt_eq_of_mem_sectorSet {n : ℕ} [NormalizedGCDMonoid (MvPolynomial (Fin n) ℝ)] {F B : Finset (Polynomial (MvPolynomial (Fin n) ℝ))} {S : Set (Fin n → ℝ)} (hB : F.IsSquarefreeBasis B) (D : TauCeti.Delineation fun (b : ↥B) (x : ↑S) => Polynomial.map (MvPolynomial.eval ↑x) ↑b) {f : Polynomial (MvPolynomial (Fin n) ℝ)} (hf : f ∈ F) (hc : ∀ x ∈ S, ∀ y ∈ S, f.content.orderAt x = f.content.orderAt y) (hb : ∀ b ∈ B, ∀ x ∈ S, Polynomial.map (MvPolynomial.eval x) b ≠ 0) {j j' : Fin (D.count + 1)} {a a' : Fin (n + 1) → ℝ} (ha : a ∈ TauCeti.cylinder S '' TauCeti.sectorSet D.root j) (ha' : a' ∈ TauCeti.cylinder S '' TauCeti.sectorSet D.root j') : ((MvPolynomial.finSuccEquiv ℝ n).symm f).orderAt a = ((MvPolynomial.finSuccEquiv ℝ n).symm f).orderAt a'

Constant order of an input's content transfers to constant ambient order across all sectors of a basis delineation, provided no basis member is nullified. Vanishing contents and zero inputs are allowed. For McCallum lifting, the content order hypothesis follows from its membership in the projection.