Ordered real roots of finite nonmonic Laurent limits

The finite limits of a nonmonic Puiseux splitting give strictly ordered real analytic root sections of a nonzero divided central-fiber family, with constant positive multiplicities. Branches with negative Laurent exponent contribute no finite root. Repeated finite limits are allowed and are removed by one fixed selection of labels on a common open neighborhood.

The complex root multiset of the real divided family is an input along the real parameter space: for Lazard evaluations it is supplied by MvPolynomial.roots_lazardEval_eq_map_of_laurent. This family need not be the ordinary central fiber, which can be nullified. Nonzeroness of the divided family is required separately, including when there are no finite branches. Reality of the selected labels, their strict ordering, and constancy of their multiplicities are conclusions.

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, §5.2, proof of Theorem 5.1.

theorem TauCeti.exists_analyticOnNhd_ordered_real_roots_of_finite_laurent_limits {E : Type u_1} {B : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup B] [NormedSpace ℝ B] {d a c : ℕ} {P : E × ℂ → Polynomial ℂ} {r s : Fin d → E × ℂ → ℂ} {φ : B → E} {b₀ : B} {F : B → Polynomial ℝ} {u v : E × ℂ → ℂ} {e : Fin d → ℤ} {w : Fin d → E × ℂ → ℂ} (hs : ∀ (i : Fin d), AnalyticAt ℂ (s i) (φ b₀, 0)) (hu : AnalyticAt ℂ u (φ b₀, 0)) (hu0 : u (φ b₀, 0) ≠ 0) (hv : AnalyticAt ℂ v (φ b₀, 0)) (hv0 : v (φ b₀, 0) ≠ 0) (hnorm : ∀ᶠ (p : E × ℂ) in nhds (φ b₀, 0), p.2 ≠ 0 → (P p).integralNormalization = ∏ i : Fin d, (Polynomial.X - Polynomial.C (s i p))) (hlead : ∀ᶠ (p : E × ℂ) in nhds (φ b₀, 0), p.2 ≠ 0 → (P p).coeff d = p.2 ^ c * v p) (hdiscr : ∀ᶠ (p : E × ℂ) in nhds (φ b₀, 0), p.2 ≠ 0 → (P p).discr = p.2 ^ a * u p) (hscale : ∀ᶠ (p : E × ℂ) in nhds (φ b₀, 0), p.2 ≠ 0 → ∀ (i : Fin d), 0 ≤ e i → (P p).coeff d * r i p = s i p) (hw : ∀ (i : Fin d), 0 ≤ e i → AnalyticAt ℂ (w i) (φ b₀, 0)) (hLaurent : ∀ᶠ (p : E × ℂ) in nhds (φ b₀, 0), p.2 ≠ 0 → ∀ (i : Fin d), 0 ≤ e i → r i p = p.2 ^ e i * w i p) (hroots : ∀ᶠ (b : B) in nhds b₀, (Polynomial.map (algebraMap ℝ ℂ) (F b)).roots = Multiset.map (fun (i : Fin d) => if e i = 0 then w i (φ b, 0) else 0) {i : Fin d | 0 ≤ e i}.val) (hF : ∀ᶠ (b : B) in nhds b₀, F b ≠ 0) (hφ : AnalyticAt ℝ φ b₀) : ∃ (k : ℕ) (t : Fin k → B → ℝ) (U : Set B), IsOpen U ∧ b₀ ∈ U ∧ (∀ b ∈ U, F b ≠ 0) ∧ (∀ (i : Fin k), AnalyticOnNhd ℝ (t i) U) ∧ (∀ b ∈ U, StrictMono fun (i : Fin k) => t i b) ∧ (∀ b ∈ U, ∀ (z : ℝ), (F b).IsRoot z ↔ ∃ (i : Fin k), t i b = z) ∧ (∀ (i : Fin k), 0 < Polynomial.rootMultiplicity (t i b₀) (F b₀)) ∧ ∀ b ∈ U, ∀ (i : Fin k), Polynomial.rootMultiplicity (t i b) (F b) = Polynomial.rootMultiplicity (t i b₀) (F b₀)

Finite Laurent limits of a prepared nonmonic splitting descend to a complete, strictly ordered analytic list of real roots of a nonzero divided central-fiber family. Every section has constant positive multiplicity on one open neighborhood. The real label set and distinct root count are derived, and an empty finite-label set or an empty real-root set is allowed.

For Lazard evaluation, MvPolynomial.roots_lazardEval_eq_map_of_laurent supplies the root multiset identity; this statement concerns the real divided family F, not a possibly zero ordinary central fiber of P. Analyticity of the Laurent amplitudes w i is required only for the finite branches.