Constant plane order on Puiseux root sections

A family of plane polynomials admits a ramified analytic splitting near the distinguished hyperplane. If its discriminant is a power of the ramification parameter times an analytic unit, the ambient order of each plane polynomial at each labelled root section is locally constant in the family parameter. On a preconnected parameter set these orders are constant everywhere, assuming the splitting and discriminant hypotheses as germs at each point.

These are orders in both coordinates of the plane polynomial, rather than multiplicities in its vertical fiber. The plane polynomials may themselves be transverse restrictions of polynomials in more variables; identifying their orders with those of the original polynomials requires order-detecting slices. Root labels may collide on the distinguished hyperplane.

The results combine TauCeti.eventually_min_analyticOrderAt_root_sub_eq with MvPolynomial.orderAt_mul_eq_sum_min_of_puiseux.

References

S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), Section 4.

theorem TauCeti.eventually_orderAt_root_eq_of_puiseux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {p : E → MvPolynomial (Fin 2) ℂ} {c : E → ℂ} {N n a : ℕ} {r : Fin n → E × ℂ → ℂ} {u : E × ℂ → ℂ} {x₀ : E} (hN : 0 < N) (hr : ∀ (i : Fin n), AnalyticAt ℂ (r i) (x₀, 0)) (hsplit : ∀ᶠ (b : E × ℂ) in nhds (x₀, 0), (MvPolynomial.aeval ![Polynomial.C (c b.1 + b.2 ^ N), Polynomial.X]) (p b.1) = ∏ i : Fin n, (Polynomial.X - Polynomial.C (r i b))) (hu : AnalyticAt ℂ u (x₀, 0)) (hu0 : u (x₀, 0) ≠ 0) (hdiscr : ∀ᶠ (b : E × ℂ) in nhds (x₀, 0), ((MvPolynomial.aeval ![Polynomial.C (c b.1 + b.2 ^ N), Polynomial.X]) (p b.1)).discr = b.2 ^ a * u b) : ∀ᶠ (x : E) in nhds x₀, ∀ (i : Fin n), (p x).orderAt ![c x, r i (x, 0)] = (p x₀).orderAt ![c x₀, r i (x₀, 0)]

In a ramified analytic splitting with power-times-unit discriminant, the ambient orders of the plane polynomials at all labelled root sections are locally constant on one common parameter neighborhood. Collisions of root labels on the hyperplane are allowed.

theorem TauCeti.orderAt_root_eq_of_puiseux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {p : E → MvPolynomial (Fin 2) ℂ} {c : E → ℂ} {N n : ℕ} {r : Fin n → E × ℂ → ℂ} {u : E × ℂ → ℂ} {U : Set E} (hUc : IsPreconnected U) (hN : 0 < N) (hr : ∀ x ∈ U, ∀ (i : Fin n), AnalyticAt ℂ (r i) (x, 0)) (hsplit : ∀ x ∈ U, ∀ᶠ (b : E × ℂ) in nhds (x, 0), (MvPolynomial.aeval ![Polynomial.C (c b.1 + b.2 ^ N), Polynomial.X]) (p b.1) = ∏ i : Fin n, (Polynomial.X - Polynomial.C (r i b))) (hu : ∀ x ∈ U, AnalyticAt ℂ u (x, 0)) (hu0 : ∀ x ∈ U, u (x, 0) ≠ 0) (hdiscr : ∀ x ∈ U, ∃ (a : ℕ), ∀ᶠ (b : E × ℂ) in nhds (x, 0), ((MvPolynomial.aeval ![Polynomial.C (c b.1 + b.2 ^ N), Polynomial.X]) (p b.1)).discr = b.2 ^ a * u b) {x y : E} (hx : x ∈ U) (hy : y ∈ U) (i : Fin n) : (p x).orderAt ![c x, r i (x, 0)] = (p y).orderAt ![c y, r i (y, 0)]

On a preconnected parameter set, a ramified analytic splitting with power-times-unit discriminant has constant ambient plane order on every labelled root section. Analyticity, splitting, and the discriminant identity are only required as germs at each point of the distinguished hyperplane. The discriminant exponent may depend on the parameter point. The order can differ between sections.