Lazard evaluations from Laurent branches

A complete Laurent splitting along an evaluator's monomial curve determines the roots of the Lazard evaluation, counted with multiplicity. Divide out the lowest monomial-curve power using the uniform Taylor expansion, then specialize the resulting analytic family. Its central fiber is the nonzero Lazard evaluation. In the central-fiber factorization, pole branches contribute a nonzero scalar factor but no finite roots; the other branches contribute exactly their finite limits, counted with multiplicity. The same normalization identifies the evaluator weight of the removed base exponent as the scalar Laurent exponent plus the sum of the negative root exponents.

No nonnullification or preservation of ordinary fiber degree is assumed. This supplies root coverage and multiplicities when descending a Puiseux Laurent splitting to Lazard evaluation; it does not yet prove constancy of these multiplicities along a base manifold.

References

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

theorem MvPolynomial.lazardEval_eq_C_mul_prod_of_laurent {𝕜 : Type u_1} {ι : Type u_2} [NontriviallyNormedField 𝕜] [Fintype ι] {n : ℕ} (p : MvPolynomial (Fin n) (Polynomial 𝕜)) (hp : p ≠ 0) (x : Fin n → 𝕜) (c : Fin n → ℕ) (hc : TauCeti.IsLazardEvaluator {p.lazardExponent (⇑Polynomial.C ∘ x)} c) {a : ℤ} {e : ι → ℤ} {u : 𝕜 → 𝕜} {w : ι → 𝕜 → 𝕜} (hu : AnalyticAt 𝕜 u 0) (hu0 : u 0 ≠ 0) (hw : ∀ (i : ι), AnalyticAt 𝕜 (w i) 0) (hw0 : ∀ (i : ι), e i < 0 → w i 0 ≠ 0) (hfac : ∀ᶠ (y : 𝕜) in nhdsWithin 0 {0}ᶜ, Polynomial.eval (Polynomial.C y) ((aeval (monomialCurve (⇑Polynomial.C ∘ x) c)) p) = Polynomial.C (y ^ a * u y) * ∏ i : ι, (Polynomial.X - Polynomial.C (y ^ e i * w i y))) : ↑((Finsupp.weight c) (p.lazardExponent (⇑Polynomial.C ∘ x))) = a + ∑ i : ι, min (e i) 0 ∧ p.lazardEval (⇑Polynomial.C ∘ x) = Polynomial.C (u 0 * ∏ i : ι with e i < 0, -w i 0) * ∏ i : ι with 0 ≤ e i, (Polynomial.X - Polynomial.C (if e i = 0 then w i 0 else 0))

A complete Laurent splitting along a Lazard evaluator determines the evaluator weight of the removed base exponent and the full Lazard evaluation. The removed weight is the scalar exponent plus the sum of the negative branch exponents. Pole branches contribute nonzero scalar factors; the other branches contribute their finite limits, with repetitions.

theorem MvPolynomial.weight_lazardExponent_eq_of_laurent {𝕜 : Type u_1} {ι : Type u_2} [NontriviallyNormedField 𝕜] [Fintype ι] {n : ℕ} (p : MvPolynomial (Fin n) (Polynomial 𝕜)) (hp : p ≠ 0) (x : Fin n → 𝕜) (c : Fin n → ℕ) (hc : TauCeti.IsLazardEvaluator {p.lazardExponent (⇑Polynomial.C ∘ x)} c) {a : ℤ} {e : ι → ℤ} {u : 𝕜 → 𝕜} {w : ι → 𝕜 → 𝕜} (hu : AnalyticAt 𝕜 u 0) (hu0 : u 0 ≠ 0) (hw : ∀ (i : ι), AnalyticAt 𝕜 (w i) 0) (hw0 : ∀ (i : ι), e i < 0 → w i 0 ≠ 0) (hfac : ∀ᶠ (y : 𝕜) in nhdsWithin 0 {0}ᶜ, Polynomial.eval (Polynomial.C y) ((aeval (monomialCurve (⇑Polynomial.C ∘ x) c)) p) = Polynomial.C (y ^ a * u y) * ∏ i : ι, (Polynomial.X - Polynomial.C (y ^ e i * w i y))) : ↑((Finsupp.weight c) (p.lazardExponent (⇑Polynomial.C ∘ x))) = a + ∑ i : ι, min (e i) 0

A complete Laurent splitting along a Lazard evaluator determines the evaluator-weight of the removed Lazard exponent. It is the exponent of the leading scalar plus the sum of the negative root exponents. In particular, the right-hand side depends only on the Laurent exponents, not on their analytic unit factors or their finite limits.

theorem MvPolynomial.lazardExponent_eq_of_laurent {𝕜 : Type u_1} {ι : Type u_2} [NontriviallyNormedField 𝕜] [Fintype ι] {n : ℕ} (p : MvPolynomial (Fin n) (Polynomial 𝕜)) (hp : p ≠ 0) (c : Fin n → ℕ) {V : Set (Fin n →₀ ℕ)} (hc : TauCeti.IsLazardEvaluator V c) {S : Set (Fin n → 𝕜)} {a : ℤ} {e : ι → ℤ} (hexponent : ∀ x ∈ S, p.lazardExponent (⇑Polynomial.C ∘ x) ∈ V) (hLaurent : ∀ x ∈ S, ∃ (u : 𝕜 → 𝕜) (w : ι → 𝕜 → 𝕜), AnalyticAt 𝕜 u 0 ∧ u 0 ≠ 0 ∧ (∀ (i : ι), AnalyticAt 𝕜 (w i) 0) ∧ (∀ (i : ι), e i < 0 → w i 0 ≠ 0) ∧ ∀ᶠ (y : 𝕜) in nhdsWithin 0 {0}ᶜ, Polynomial.eval (Polynomial.C y) ((aeval (monomialCurve (⇑Polynomial.C ∘ x) c)) p) = Polynomial.C (y ^ a * u y) * ∏ i : ι, (Polynomial.X - Polynomial.C (y ^ e i * w i y))) (x : Fin n → 𝕜) : x ∈ S → ∀ y ∈ S, p.lazardExponent (⇑Polynomial.C ∘ x) = p.lazardExponent (⇑Polynomial.C ∘ y)

Constant removed exponents from global Laurent exponents. Suppose one evaluator controls the removed Lazard exponents of p on S, and at every point of S the monomial-curve specialization has a Laurent factorization with the same scalar exponent a and the same root exponents e. The removed Lazard exponent of p is then constant on S.

The analytic unit factors and the finite root limits may vary with the point. Their only role is to make each Laurent factorization nondegenerate; the preceding weight formula shows that all removed exponents have the same evaluator-weight, and evaluator injectivity recovers equality of the exponent vectors.

theorem MvPolynomial.roots_lazardEval_eq_map_of_laurent {𝕜 : Type u_1} {ι : Type u_2} [NontriviallyNormedField 𝕜] [Fintype ι] {n : ℕ} (p : MvPolynomial (Fin n) (Polynomial 𝕜)) (hp : p ≠ 0) (x : Fin n → 𝕜) (c : Fin n → ℕ) (hc : TauCeti.IsLazardEvaluator {p.lazardExponent (⇑Polynomial.C ∘ x)} c) {a : ℤ} {e : ι → ℤ} {u : 𝕜 → 𝕜} {w : ι → 𝕜 → 𝕜} (hu : AnalyticAt 𝕜 u 0) (hu0 : u 0 ≠ 0) (hw : ∀ (i : ι), AnalyticAt 𝕜 (w i) 0) (hw0 : ∀ (i : ι), e i < 0 → w i 0 ≠ 0) (hfac : ∀ᶠ (y : 𝕜) in nhdsWithin 0 {0}ᶜ, Polynomial.eval (Polynomial.C y) ((aeval (monomialCurve (⇑Polynomial.C ∘ x) c)) p) = Polynomial.C (y ^ a * u y) * ∏ i : ι, (Polynomial.X - Polynomial.C (y ^ e i * w i y))) : (p.lazardEval (⇑Polynomial.C ∘ x)).roots = Multiset.map (fun (i : ι) => if e i = 0 then w i 0 else 0) {i : ι | 0 ≤ e i}.val

A complete Laurent splitting along a Lazard evaluator determines the Lazard evaluation's root multiset. A branch of exponent zero contributes its unit value at the origin, a branch of positive exponent contributes zero, and a branch with a pole contributes no finite root. Coincident limits are counted separately, so the equality includes root multiplicities.