Laurent unit forms of nonmonic root differences

Let the leading coefficient and discriminant of a nonmonic polynomial family be centered powers of a distinguished variable times analytic units. If its leading-coefficient-scaled roots extend analytically across the distinguished hyperplane, every difference of distinct root labels is a Laurent power times an analytic unit. The exponent is independent of the other parameters. Negative exponents permit poles; positive exponents permit collisions.

The normalized roots are supplied by a splitting of the integral normalization off the hyperplane. No splitting of the original family on the hyperplane is required, where its degree may drop or it may be nullified. Parameter-independent orders of root differences are used in analytic preparation of nonmonic polynomial families, including those whose branches have poles. The original coefficient and discriminant formulas are required only off the hyperplane: recomputing a discriminant after a degree drop need not preserve the formal discriminant. No constant-coefficient hypothesis is needed for differences.

References

S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, J. Symbolic Comput. 92 (2019), §4, Corollary 4.2.

theorem TauCeti.exists_root_sub_eq_zpow_mul_unit {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {d a c : ℕ} {P : E × 𝕜 → Polynomial 𝕜} {r s : Fin d → E × 𝕜 → 𝕜} {x₀ : E} {y₀ : 𝕜} {u v : E × 𝕜 → 𝕜} (hs : ∀ (i : Fin d), AnalyticAt 𝕜 (s i) (x₀, y₀)) (hu : AnalyticAt 𝕜 u (x₀, y₀)) (hu0 : u (x₀, y₀) ≠ 0) (hv : AnalyticAt 𝕜 v (x₀, y₀)) (hv0 : v (x₀, y₀) ≠ 0) (hnorm : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → (P p).integralNormalization = ∏ i : Fin d, (Polynomial.X - Polynomial.C (s i p))) (hlead : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → (P p).coeff d = (p.2 - y₀) ^ c * v p) (hdiscr : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → (P p).discr = (p.2 - y₀) ^ a * u p) {i j : Fin d} (hscale : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → (P p).coeff d * r i p = s i p ∧ (P p).coeff d * r j p = s j p) (hij : i ≠ j) : ∃ (b : ℤ) (w : E × 𝕜 → 𝕜), AnalyticAt 𝕜 w (x₀, y₀) ∧ w (x₀, y₀) ≠ 0 ∧ ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), w p ≠ 0 ∧ (p.2 ≠ y₀ → r i p - r j p = (p.2 - y₀) ^ b * w p)

Differences of nonmonic root branches are Laurent powers times analytic units when the leading coefficient and discriminant are centered powers times analytic units. The scaled roots s i must extend analytically and split the integral normalization off the hyperplane. Only the selected pair of original roots must satisfy the scaling identities, and they may have poles there. The exponent is constant in the parameters, and the unit is nonzero on a neighborhood including the hyperplane.