Analytic Lazard lifting for one polynomial

A nonzero polynomial in one distinguished variable has a global Lazard delineation over a connected real analytic submanifold when its discriminant is nonzero and its formal leading coefficient, trailing coefficient, and discriminant have constant Lazard valuation there. Ordinary fibers may vanish: the sections enumerate the roots of the nonzero Lazard evaluations instead.

The construction applies the local Puiseux preparation theorem in analytic chart coordinates. That theorem supplies ordered analytic roots, constant multiplicities, and a locally constant vector of removed base exponents on one common neighborhood. These local Lazard delineations then glue because their increasing root lists describe the same intrinsic fibers.

The distinguished-coordinate factor is treated separately. Since the discriminant is nonzero, the distinguished variable divides the polynomial at most once. If it does not divide it, the trailing coefficient is the constant coefficient and the local construction applies directly. Otherwise the polynomial is X * q with q of nonzero constant coefficient. The invariants of q are constant because those of X * q are (Polynomial.discr_X_mul), and the delineation of q extends to X * q by TauCeti.nonempty_lazardDelineation_X_mul.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Section 5.2, Theorem 5.1.

theorem Polynomial.nonempty_lazardDelineation_of_lazardValuation_eq {n d : ℕ} {S : Set (Fin n → ℝ)} (p : Polynomial (MvPolynomial (Fin n) ℝ)) (hS : TauCeti.IsAnalyticSubmanifold d S) (hconn : IsPreconnected S) (hp : p ≠ 0) (hdiscr : p.discr ≠ 0) (hlead_eq : ∀ x ∈ S, ∀ y ∈ S, p.leadingCoeff.lazardValuation x = p.leadingCoeff.lazardValuation y) (htrail_eq : ∀ x ∈ S, ∀ y ∈ S, p.trailingCoeff.lazardValuation x = p.trailingCoeff.lazardValuation y) (hdiscr_eq : ∀ x ∈ S, ∀ y ∈ S, p.discr.lazardValuation x = p.discr.lazardValuation y) : Nonempty (TauCeti.LazardDelineation (fun (x : Unit) => (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm p)) S)

Analytic Lazard lifting for one polynomial. Let p be a nonzero polynomial in a distinguished variable with coefficients in ℝ[X₀, …, Xₙ₋₁]. If its formal leading coefficient, trailing coefficient, and discriminant each have constant Lazard valuation on a preconnected analytic submanifold S, and its discriminant is nonzero, then the corresponding polynomial in n + 1 variables has a Lazard delineation over S.

The conclusion concerns Lazard evaluations, so ordinary fibers may be zero and their degrees may drop. Constant polynomials, polynomials without real Lazard roots, and polynomials divisible by the distinguished variable are included.