Local delineability from constant discriminant order

A polynomial with real polynomial coefficients has a local delineation along an analytic parametrization on which its fibers are nonzero of constant degree and its formal discriminant has constant finite ambient order. The sections extend to real analytic functions, have constant positive root multiplicities, and account for all real roots; signs are constant on every section and sector.

The formal leading coefficient may vanish along the parametrization, so the fiber degree may be smaller than the formal degree at which the discriminant is taken; monic polynomials are a special case. The construction starts with the real discriminant-order condition, not a supplied complex splitting or a hypothesis of constant root multiplicities. Multiple roots at the center, constant polynomials and families without real roots are included. This is the local analytic delineability conclusion, not a theorem about ambient order on the root sections.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer (1998).
• 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.exists_delineation_of_orderAt_discr_eq {σ : Type u_1} {ι : Type u_2} [Fintype σ] [Fintype ι] (p : Polynomial (MvPolynomial σ ℝ)) {φ : (ι → ℝ) → σ → ℝ} {a : ι → ℝ} {d m : ℕ} (hφ : AnalyticAt ℝ φ a) (hp : map (MvPolynomial.eval₂Hom (RingHom.id ℝ) (φ a)) p ≠ 0) (hd : ∀ᶠ (x : ι → ℝ) in nhds a, (map (MvPolynomial.eval₂Hom (RingHom.id ℝ) (φ x)) p).natDegree = d) (hm : ∀ᶠ (x : ι → ℝ) in nhds a, p.discr.orderAt (φ x) = ↑m) : ∃ ε > 0, ∃ (D : TauCeti.Delineation fun (x : Unit) (x_1 : ↑(Metric.ball a ε)) => map (MvPolynomial.eval₂Hom (RingHom.id ℝ) (φ ↑x_1)) p), ∀ (i : Fin D.count), ∃ (s : (ι → ℝ) → ℝ), AnalyticOnNhd ℝ s (Metric.ball a ε) ∧ ∀ (x : ↑(Metric.ball a ε)), D.root i x = s ↑x

Local delineability from constant discriminant order. Let p be a polynomial whose coefficients are real polynomials, specialized along a real analytic parametrization φ. If the fiber at a is nonzero, the fibers near a have constant degree, and the formal discriminant of p has constant finite ambient order near a, then the fibers have a delineation on some positive-radius ball around a, and all root sections admit analytic extensions to that ball.

The formal leading coefficient of p may vanish at a, so the constant degree of the fibers can be smaller than the formal degree at which the discriminant is taken.