Constructing ordered analytic roots of Lazard evaluations

Locally constant finite Lazard valuations of the leading coefficient, constant coefficient, and discriminant along real analytic centers construct strictly ordered real analytic root sections of the Lazard evaluations. Their multiplicities are positive and locally constant, and the vector of removed base exponents is constant on the same neighborhood. The ordinary fibers may be nullified: the sections enumerate the nonzero Lazard evaluations.

The sections include repeated finite Laurent limits with their multiplicities; branches with poles contribute no finite root. Finite-valuation hypotheses exclude zero formal polynomials, but neither preservation of the ordinary fiber degree nor nonnullification is required.

References

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

theorem Polynomial.exists_analyticOnNhd_ordered_lazardEval_roots {ι : Type u_1} [Fintype ι] {n : ℕ} (p : Polynomial (MvPolynomial (Fin n) ℝ)) {φ : (ι → ℝ) → Fin n → ℝ} {a : ι → ℝ} (hφ : AnalyticAt ℝ φ a) (vLead vConst vDiscr : Fin n →₀ ℕ) (hlead : ∀ᶠ (x : ι → ℝ) in nhds a, p.leadingCoeff.lazardValuation (φ x) = ↑(toLex vLead)) (hconst : ∀ᶠ (x : ι → ℝ) in nhds a, (p.coeff 0).lazardValuation (φ x) = ↑(toLex vConst)) (hdiscr : ∀ᶠ (x : ι → ℝ) in nhds a, p.discr.lazardValuation (φ x) = ↑(toLex vDiscr)) : have q := (MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm p); have F := fun (x : ι → ℝ) => q.lazardEval (⇑C ∘ φ x); ∃ (k : ℕ) (t : Fin k → (ι → ℝ) → ℝ) (U : Set (ι → ℝ)), IsOpen U ∧ a ∈ U ∧ (∀ x ∈ U, F x ≠ 0) ∧ (∀ x ∈ U, q.lazardExponent (⇑C ∘ φ x) = q.lazardExponent (⇑C ∘ φ a)) ∧ (∀ (i : Fin k), AnalyticOnNhd ℝ (t i) U) ∧ (∀ x ∈ U, StrictMono fun (i : Fin k) => t i x) ∧ (∀ x ∈ U, ∀ (z : ℝ), (F x).IsRoot z ↔ ∃ (i : Fin k), t i x = z) ∧ (∀ (i : Fin k), 0 < rootMultiplicity (t i a) (F a)) ∧ ∀ x ∈ U, ∀ (i : Fin k), rootMultiplicity (t i x) (F x) = rootMultiplicity (t i a) (F a)

Finite locally constant Lazard valuations of the formal leading coefficient, constant coefficient, and discriminant along analytic centers construct all real roots of nearby Lazard evaluations as a strictly ordered analytic list, with constant removed base exponent and constant positive multiplicities. The number of real roots is constructed and may be zero. Ordinary fibers may be nullified, and no positive-degree assumption is needed.