Ambient order from Puiseux root contacts

If a plane polynomial splits after y = a 0 + t ^ N into analytic roots r i t, with a nonvanishing analytic leading factor, its ambient order at a specified point is computed by their contact orders with the second coordinate of that point:

N * order(p, a) = ∑ i, min N (analyticOrderAt (r i · - a 1) 0).

The formula includes repeated roots and branches identically zero. It differs from the multiplicity in the vertical fiber: for z² - y, the fiber has multiplicity two at zero but the ambient order is one. Generic lines avoid cancellation at roots whose contact order equals the ramification exponent. This is the transverse-slice calculation used to recover ambient order on root sections from ramified splittings.

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 MvPolynomial.orderAt_mul_eq_sum_min_of_puiseux {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_2} [Fintype ι] (p : MvPolynomial (Fin 2) 𝕜) (a : Fin 2 → 𝕜) {N : ℕ} (hN : 0 < N) {r : ι → 𝕜 → 𝕜} {u : 𝕜 → 𝕜} (hr : ∀ (i : ι), AnalyticAt 𝕜 (r i) 0) (hu : AnalyticAt 𝕜 u 0) (hu0 : u 0 ≠ 0) (hsplit : ∀ᶠ (t : 𝕜) in nhds 0, ∀ (z : 𝕜), (eval ![a 0 + t ^ N, z]) p = u t * ∏ i : ι, (z - r i t)) : p.orderAt a * ↑N = ∑ i : ι, min (↑N) (analyticOrderAt (fun (t : 𝕜) => r i t - a 1) 0)

An analytic Puiseux splitting computes the ambient order of a plane polynomial from the contact orders of all root labels with the second coordinate of the point. The leading factor is a unit; root labels may repeat or vanish identically.