Constant order and constant sign

A polynomial p has constant order on a set S when its order of vanishing p.orderAt x is the same at every point x ∈ S. On a preconnected set this forces p to be sign-invariant: constant order zero means that p has no zero on S, so its sign is locally constant there, while a constant positive order means that p vanishes on all of S.

The converse fails, even on a connected set: X₀ * X₁ vanishes identically on the line x₀ = 0 of the plane, but its order of vanishing there is 2 at the origin and 1 at every other point. This is why order-invariant decompositions, used for McCallum's projection, ask for more than sign-invariant ones.

Main results

• IsPreconnected.signInvariant_eval_of_orderAt_eq: constant order on a preconnected set implies sign-invariance.
• TauCeti.exists_signInvariant_orderAt_ne: sign-invariance on a connected set does not imply constant order.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer (1998), pp. 242–268, Section 2.

theorem IsPreconnected.signInvariant_eval_of_orderAt_eq {σ : Type u_1} {R : Type u_2} [CommSemiring R] [LinearOrder R] [TopologicalSpace R] [OrderTopology R] [IsTopologicalSemiring R] {p : MvPolynomial σ R} {S : Set (σ → R)} (hS : IsPreconnected S) (h : ∀ x ∈ S, ∀ y ∈ S, p.orderAt x = p.orderAt y) : TauCeti.SignInvariant (fun (x : σ → R) => (MvPolynomial.eval x) p) S

A polynomial whose order of vanishing is the same at all points of a preconnected set S is sign-invariant on S.

theorem TauCeti.exists_signInvariant_orderAt_ne : ∃ (p : MvPolynomial (Fin 2) ℝ) (S : Set (Fin 2 → ℝ)), IsConnected S ∧ SignInvariant (fun (x : Fin 2 → ℝ) => (MvPolynomial.eval x) p) S ∧ ∃ x ∈ S, ∃ y ∈ S, p.orderAt x ≠ p.orderAt y

Sign-invariance does not imply constant order, even on a connected set: the polynomial X₀ * X₁ vanishes on the line x₀ = 0, but its order of vanishing there is 2 at the origin and 1 at (0, 1).