Collisions and multiplicities of finite nonmonic branches

Suppose a nonmonic polynomial family's leading coefficient and discriminant are powers of a distinguished coordinate times analytic units, and its normalized roots extend analytically. Any two original branches that extend analytically have locally constant contact order, and hence locally persistent collisions, on the exceptional hyperplane. Collision persistence also holds for independent analytic extensions of selected labels. Other branches may have poles there.

For Laurent branches, the nonnegative-exponent labels have explicit analytic extensions. If a polynomial's root multiset consists of their finite limits, its multiplicity at each labelled limit is locally constant. In particular this applies to the root multisets of Lazard evaluations identified by MvPolynomial.roots_lazardEval_eq_map_of_laurent. Repeated finite limits and an empty set of finite branches are allowed. No preservation of the original central fiber's degree, or nonnullification of that fiber, is required.

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.eventually_analyticOrderAt_finite_root_sub_eq {𝕜 : 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) (hi : AnalyticAt 𝕜 (r i) (x₀, y₀)) (hj : AnalyticAt 𝕜 (r j) (x₀, y₀)) (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) : ∀ᶠ (x : E) in nhds x₀, analyticOrderAt (fun (y : 𝕜) => r i (x, y) - r j (x, y)) y₀ = analyticOrderAt (fun (y : 𝕜) => r i (x₀, y) - r j (x₀, y)) y₀

Two finite analytic branches of a nonmonic splitting have locally constant contact order on the exceptional hyperplane. Only the selected branches need analytic extensions; the other original branches may have poles.

theorem TauCeti.eventually_finite_root_eq_iff_on_hyperplane {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {d a c : ℕ} {P : E × 𝕜 → Polynomial 𝕜} {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) {f g : E × 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f (x₀, y₀)) (hg : AnalyticAt 𝕜 g (x₀, y₀)) (hscale : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → (P p).coeff d * f p = s i p ∧ (P p).coeff d * g p = s j p) : ∀ᶠ (x : E) in nhds x₀, f (x, y₀) = g (x, y₀) ↔ f (x₀, y₀) = g (x₀, y₀)

Coincidence of two finite analytic extensions of nonmonic root labels is locally constant on the exceptional hyperplane. Only the chosen branches must have finite extensions; all other labels may have poles and central fibers may be nullified.

theorem TauCeti.eventually_finite_laurent_limit_eq_iff {𝕜 : 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) {e : Fin d → ℤ} {w : Fin d → E × 𝕜 → 𝕜} (hscale : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → ∀ (i : Fin d), 0 ≤ e i → (P p).coeff d * r i p = s i p) (hw : ∀ (i : Fin d), 0 ≤ e i → AnalyticAt 𝕜 (w i) (x₀, y₀)) (hLaurent : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → ∀ (i : Fin d), 0 ≤ e i → r i p = (p.2 - y₀) ^ e i * w i p) : ∀ᶠ (x : E) in nhds x₀, ∀ i ∈ {i : Fin d | 0 ≤ e i}, ∀ j ∈ {i : Fin d | 0 ≤ e i}, ((if e i = 0 then w i (x, y₀) else 0) = if e j = 0 then w j (x, y₀) else 0) ↔ (if e i = 0 then w i (x₀, y₀) else 0) = if e j = 0 then w j (x₀, y₀) else 0

Collisions among the finite limits of Laurent branches are locally constant on the exceptional hyperplane. Only nonnegative-exponent amplitudes need be analytic, and the other branches may have poles.

theorem TauCeti.eventually_rootMultiplicity_eq_of_finite_laurent_limits {𝕜 : 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) {e : Fin d → ℤ} {w : Fin d → E × 𝕜 → 𝕜} (hscale : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → ∀ (i : Fin d), 0 ≤ e i → (P p).coeff d * r i p = s i p) (hw : ∀ (i : Fin d), 0 ≤ e i → AnalyticAt 𝕜 (w i) (x₀, y₀)) (hLaurent : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → ∀ (i : Fin d), 0 ≤ e i → r i p = (p.2 - y₀) ^ e i * w i p) {Q : E → Polynomial 𝕜} (hroots : ∀ᶠ (x : E) in nhds x₀, (Q x).roots = Multiset.map (fun (i : Fin d) => if e i = 0 then w i (x, y₀) else 0) {i : Fin d | 0 ≤ e i}.val) : ∀ᶠ (x : E) in nhds x₀, ∀ (i : Fin d), 0 ≤ e i → Polynomial.rootMultiplicity (if e i = 0 then w i (x, y₀) else 0) (Q x) = Polynomial.rootMultiplicity (if e i = 0 then w i (x₀, y₀) else 0) (Q x₀)

Multiplicities of finite Laurent limits are locally constant when the nonmonic leading coefficient and discriminant have power-times-unit forms. The root multiset identity is an input, so the polynomial Q can be a divided central fiber, such as a Lazard evaluation, rather than the possibly nullified ordinary fiber.