Constructed Lazard root multisets

Real analytic centers with locally constant finite Lazard valuations of the formal leading coefficient, constant coefficient, and discriminant construct a complete Laurent splitting. The finite branch limits of this same splitting enumerate the roots, with multiplicity, of nearby Lazard evaluations. Ordinary fibers may be nullified. A common complexification, evaluator, analytic leading and formal-discriminant units, and pole-removed root functions are retained for subsequent analysis of the real roots.

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_complexification_isLazardEvaluator_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); ∃ ρ > 0, ∃ (Φ : (ι → ℂ) → Fin n → ℂ) (c : Fin n → ℕ), TauCeti.IsLazardEvaluator ({vLead, vConst, vDiscr} ∪ Set.range q.lazardExponent) c ∧ AnalyticOnNhd ℂ Φ (Metric.ball (fun (j : ι) => ↑(a j)) ρ) ∧ (∀ x ∈ Metric.ball a ρ, (Φ fun (j : ι) => ↑(x j)) = fun (i : Fin n) => ↑(φ x i)) ∧ (∀ (z : ι → ℂ), Φ (star z) = star (Φ z)) ∧ ∃ (u : (ι → ℂ) × ℂ → ℂ) (v : (ι → ℂ) × ℂ → ℂ), AnalyticOnNhd ℂ u (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 ρ) ∧ (∀ b ∈ Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 ρ, u b ≠ 0 ∧ MvPolynomial.eval₂ Complex.ofRealHom (fun (j : Fin n) => Φ b.1 j + b.2 ^ c j) p.leadingCoeff = b.2 ^ (Finsupp.weight c) vLead * u b) ∧ AnalyticOnNhd ℂ v (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 ρ) ∧ (∀ b ∈ Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 ρ, v b ≠ 0 ∧ MvPolynomial.eval₂ Complex.ofRealHom (fun (j : Fin n) => Φ b.1 j + b.2 ^ c j) p.discr = b.2 ^ (Finsupp.weight c) vDiscr * v b) ∧ ∃ R > 0, R ^ p.natDegree.factorial ≤ ρ ∧ ∃ (r : Fin p.natDegree → (ι → ℂ) × ℂ → ℂ) (g : Fin p.natDegree → (ι → ℂ) × ℂ → ℂ), (∀ (i : Fin p.natDegree), AnalyticOnNhd ℂ (r i) (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ (Metric.ball 0 R \ {0}))) ∧ (∀ (i : Fin p.natDegree), AnalyticOnNhd ℂ (g i) (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 R) ∧ Set.EqOn (g i) (fun (b : (ι → ℂ) × ℂ) => b.2 ^ (p.natDegree.factorial * (Finsupp.weight c) vLead) * r i b) (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ (Metric.ball 0 R \ {0}))) ∧ (∀ b ∈ Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ (Metric.ball 0 R \ {0}), (Function.Injective fun (i : Fin p.natDegree) => r i b) ∧ map (MvPolynomial.eval₂Hom Complex.ofRealHom fun (j : Fin n) => Φ b.1 j + b.2 ^ (p.natDegree.factorial * c j)) p = C (MvPolynomial.eval₂ Complex.ofRealHom (fun (j : Fin n) => Φ b.1 j + b.2 ^ (p.natDegree.factorial * c j)) p.leadingCoeff) * ∏ i : Fin p.natDegree, (X - C (r i b))) ∧ ∃ (e : Fin p.natDegree → ℤ) (w : Fin p.natDegree → (ι → ℂ) × ℂ → ℂ), (∀ (i : Fin p.natDegree), -(↑p.natDegree.factorial * ↑((Finsupp.weight c) vLead)) ≤ e i) ∧ (∀ (i : Fin p.natDegree), AnalyticAt ℂ (w i) (fun (j : ι) => ↑(a j), 0)) ∧ (∀ (i : Fin p.natDegree), w i (fun (j : ι) => ↑(a j), 0) ≠ 0) ∧ (∀ᶠ (b : (ι → ℂ) × ℂ) in nhds (fun (j : ι) => ↑(a j), 0), (∀ (i : Fin p.natDegree), w i b ≠ 0) ∧ (b.2 ≠ 0 → ∀ (i : Fin p.natDegree), r i b = b.2 ^ e i * w i b)) ∧ ∀ᶠ (x : ι → ℝ) in nhds a, (map Complex.ofRealHom (q.lazardEval (⇑C ∘ φ x))).roots = Multiset.map (fun (i : Fin p.natDegree) => if e i = 0 then w i (fun (j : ι) => ↑(x j), 0) else 0) {i : Fin p.natDegree | 0 ≤ e i}.val ∧ q.lazardExponent (⇑C ∘ φ x) = q.lazardExponent (⇑C ∘ φ a)

Finite locally constant valuations along real analytic centers construct Laurent branches whose finite limits give the complete complex root multiset of the Lazard evaluation near the center. The leading and formal-discriminant units and all branch data belong to the same monomial deformation. The local branch-unit family is fixed at the central parameter and works for every nearby real parameter. Poles contribute no finite root and positive branch exponents contribute zero. The same Laurent exponents force the removed Lazard exponent to be locally constant.