Constant ambient order on root sections from discriminant order

Let p be a polynomial in a distinguished variable whose coefficients are real polynomials in n variables, with nonzero fiber at a point of a real analytic parametrization of the base, and suppose its formal discriminant has constant finite ambient order along the parametrization. Then along every real root of the fibers which is continuous at that point, the ambient order of p, as a polynomial in all n + 1 variables, is locally constant. This is the order-invariance of p on root sections in McCallum's local discriminant theorem; fiber root multiplicity is not substituted for ambient order. The formal leading coefficient may vanish, so the fiber degree may drop.

For monic p the argument works in transverse planes, which keep the root coordinate and move the base along an affine line. For every real direction in an open dense set, the discriminant becomes a power of the line parameter times a unit after complexification, and the fibers split into analytic branches after a ramified substitution (Polynomial.exists_analyticAt_prod_X_sub_C_of_orderAt_discr_eq). The plane order of p at each branch on the base is then locally constant (TauCeti.eventually_orderAt_root_eq_of_puiseux). A real root which is continuous at the central point eventually meets only branches through its central value, so its plane orders are locally constant too. Finitely many directions in the open set detect ambient order (TauCeti.eventually_orderAt_eq_of_transverse), which gives the conclusion.

The general case reduces to the monic one in normalized reciprocal coordinates centered at a nonroot τ of the central fiber. The normalized reversal of p is monic, its discriminant has the same ambient order near the point (Polynomial.discr_integralNormalization_reverse_comp_X_add_C), and the coordinate change preserves ambient order away from τ (Polynomial.orderAt_integralNormalization_reverse_comp_X_add_C).

Main results

• Polynomial.eventually_orderAt_root_eq_of_orderAt_discr_eq: constant finite ambient order of the formal discriminant gives locally constant ambient order along continuous real roots.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer (1998), Sections 2–3.
• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), Section 4.

theorem Polynomial.eventually_orderAt_root_eq_of_orderAt_discr_eq {n : ℕ} {ι : Type u_1} [Fintype ι] {p : Polynomial (MvPolynomial (Fin n) ℝ)} {φ : (ι → ℝ) → Fin n → ℝ} {θ : (ι → ℝ) → ℝ} {a : ι → ℝ} {m : ℕ} (hφ : AnalyticAt ℝ φ a) (hp : map (MvPolynomial.eval (φ a)) p ≠ 0) (hm : ∀ᶠ (x : ι → ℝ) in nhds a, p.discr.orderAt (φ x) = ↑m) (hθ : ContinuousAt θ a) (hroot : ∀ᶠ (x : ι → ℝ) in nhds a, (map (MvPolynomial.eval (φ x)) p).IsRoot (θ x)) : ∀ᶠ (x : ι → ℝ) in nhds a, ((MvPolynomial.finSuccEquiv ℝ n).symm p).orderAt (Fin.cons (θ x) (φ x)) = ((MvPolynomial.finSuccEquiv ℝ n).symm p).orderAt (Fin.cons (θ a) (φ a))

Constant ambient order on root sections. Let p be a polynomial whose coefficients are real polynomials in n variables, specialized along a real analytic parametrization φ, with nonzero fiber at a, and suppose its formal discriminant has constant finite ambient order near a. Along a real root θ of the fibers which is continuous at a, the ambient order of p, viewed as a polynomial in n + 1 variables with the root coordinate first, is constant near a.

The formal leading coefficient of p may vanish at a, so the fiber degree may be smaller than the formal degree at which the discriminant is taken. The fibers may have multiple roots, and distinct real roots may meet at a.