Central fibers of Laurent root factorizations

For an analytic polynomial family with nonzero central fiber, a complete Laurent factorization off the origin determines the central fiber, including multiplicities. Branches with negative exponents escape to infinity and contribute only a nonzero scalar; branches with positive exponents tend to zero; branches with exponent zero tend to their amplitude values. The exponent of the leading scalar balances the sum of the pole exponents.

This applies to the divided monomial deformation of a Lazard evaluation: its central fiber is nonzero even when the ordinary fiber is nullified. It identifies all finite branch limits with that evaluation's root multiset, without assuming a root count or a matching at the center. Repeated limits and an empty family of branches are allowed. The scalar balance uses Mathlib’s AnalyticAt.unique_eventuallyEq_zpow_smul_ne_zero.

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 TauCeti.eq_C_mul_prod_of_laurent {𝕜 : Type u_1} {ι : Type u_2} [NontriviallyNormedField 𝕜] [Fintype ι] {F : 𝕜 → Polynomial 𝕜} {d : ℕ} {a : ℤ} {e : ι → ℤ} {u : 𝕜 → 𝕜} {w : ι → 𝕜 → 𝕜} (hF : ∀ j ≤ d, AnalyticAt 𝕜 (fun (y : 𝕜) => (F y).coeff j) 0) (hdeg : ∀ᶠ (y : 𝕜) in nhds 0, (F y).natDegree ≤ d) (hF0 : F 0 ≠ 0) (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}ᶜ, F y = Polynomial.C (y ^ a * u y) * ∏ i : ι, (Polynomial.X - Polynomial.C (y ^ e i * w i y))) : a + ∑ i : ι, min (e i) 0 = 0 ∧ F 0 = 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 root factorization of an analytic polynomial family with nonzero central fiber determines its factorization at the origin. Only the amplitudes of pole branches are required to be nonzero at the origin. Branches with nonnegative exponents remain as roots. Negative exponents contribute their nonzero unit values to the scalar, and their sum cancels the exponent of the original scalar.

theorem TauCeti.roots_eq_map_of_laurent {𝕜 : Type u_1} {ι : Type u_2} [NontriviallyNormedField 𝕜] [Fintype ι] {F : 𝕜 → Polynomial 𝕜} {d : ℕ} {a : ℤ} {e : ι → ℤ} {u : 𝕜 → 𝕜} {w : ι → 𝕜 → 𝕜} (hF : ∀ j ≤ d, AnalyticAt 𝕜 (fun (y : 𝕜) => (F y).coeff j) 0) (hdeg : ∀ᶠ (y : 𝕜) in nhds 0, (F y).natDegree ≤ d) (hF0 : F 0 ≠ 0) (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}ᶜ, F y = Polynomial.C (y ^ a * u y) * ∏ i : ι, (Polynomial.X - Polynomial.C (y ^ e i * w i y))) : (F 0).roots = Multiset.map (fun (i : ι) => if e i = 0 then w i 0 else 0) {i : ι | 0 ≤ e i}.val

The root multiset of the nonzero central fiber consists precisely of the finite Laurent branch limits, with each label counted once. Coincident limits retain their multiplicity.