Root collisions and multiplicities on the Puiseux hyperplane

Suppose a polynomial family has a complete analytic splitting near (x₀, y₀) and its discriminant is (y - y₀)^a times an analytic unit. On the distinguished hyperplane y = y₀, the equivalence relation identifying coincident root labels is locally constant. Consequently the multiplicity of each labelled root of the specialized polynomial is locally constant, even when several labels collide there.

These conclusions supply the multiplicity information needed to pass from a ramified analytic splitting to distinct root sections. No constancy of multiplicities or collisions is assumed. The splitting itself is an input; its construction is separate.

The proof uses TauCeti.exists_root_sub_eq_pow_mul_unit: a root difference with positive exponent vanishes identically on the hyperplane, whereas one with exponent zero is a unit.

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, Section 4.

theorem TauCeti.eventually_root_eq_iff_on_hyperplane {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {r : Fin n → E × 𝕜 → 𝕜} {P : E × 𝕜 → Polynomial 𝕜} {x₀ : E} {y₀ : 𝕜} {a : ℕ} {u : E × 𝕜 → 𝕜} (hr : ∀ (i : Fin n), AnalyticAt 𝕜 (r i) (x₀, y₀)) (hP : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), P p = ∏ i : Fin n, (Polynomial.X - Polynomial.C (r i p))) (hu : AnalyticAt 𝕜 u (x₀, y₀)) (hu0 : u (x₀, y₀) ≠ 0) (hdiscr : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), (P p).discr = (p.2 - y₀) ^ a * u p) (i j : Fin n) : ∀ᶠ (x : E) in nhds x₀, r i (x, y₀) = r j (x, y₀) ↔ r i (x₀, y₀) = r j (x₀, y₀)

Coincidence of two root labels is locally constant on the distinguished hyperplane when the discriminant is a centered power times an analytic unit. Collisions at the hyperplane are allowed.

theorem TauCeti.eventually_rootMultiplicity_eq_on_hyperplane {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {r : Fin n → E × 𝕜 → 𝕜} {P : E × 𝕜 → Polynomial 𝕜} {x₀ : E} {y₀ : 𝕜} {a : ℕ} {u : E × 𝕜 → 𝕜} (hr : ∀ (i : Fin n), AnalyticAt 𝕜 (r i) (x₀, y₀)) (hP : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), P p = ∏ i : Fin n, (Polynomial.X - Polynomial.C (r i p))) (hu : AnalyticAt 𝕜 u (x₀, y₀)) (hu0 : u (x₀, y₀) ≠ 0) (hdiscr : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), (P p).discr = (p.2 - y₀) ^ a * u p) : ∀ᶠ (x : E) in nhds x₀, ∀ (i : Fin n), Polynomial.rootMultiplicity (r i (x, y₀)) (P (x, y₀)) = Polynomial.rootMultiplicity (r i (x₀, y₀)) (P (x₀, y₀))

On one common neighborhood of the central parameter, every labelled root on the distinguished hyperplane has its central multiplicity. This multiplicity counts all labels coinciding there and may be greater than one.