Capped contacts of Puiseux branches

A complete analytic splitting after y = t ^ N is permuted by t ↦ ζ * t for a primitive Nth root of unity. If its discriminant is a power of t times an analytic unit, the orders of differences between distinct labels are locally constant. Rotation then shows that the orders of contact with each branch's value at t = 0, capped at N, are locally constant too.

The capped contacts with any labelled root on the hyperplane are also locally constant, including when several labels coincide there. These are the summands in the Puiseux formula for ambient polynomial order at a root section.

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.existsUnique_root_rotation_perm {E : Type u_1} [TopologicalSpace E] {U : Set E} {R : ℝ} {N n : ℕ} {ζ : ℂ} {P : E × ℂ → Polynomial ℂ} {r : Fin n → E × ℂ → ℂ} (hU : IsPreconnected U) (hR : 0 < R) (hζ : ζ ^ N = 1) (hζnorm : ‖ζ‖ = 1) (hr : ∀ (i : Fin n), ContinuousOn (r i) (U ×ˢ Metric.ball 0 R)) (hinj : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), Function.Injective fun (i : Fin n) => r i b) (hP : ∀ b ∈ U ×ˢ Metric.ball 0 R, P (b.1, b.2 ^ N) = ∏ i : Fin n, (Polynomial.X - Polynomial.C (r i b))) (x₀ : ↑U) : ∃! σ : Equiv.Perm (Fin n), ∀ (i : Fin n), ∀ b ∈ U ×ˢ Metric.ball 0 R, r (σ i) b = r i (b.1, ζ * b.2)

Rotation permutes a complete continuous splitting of a power-substituted polynomial family. The permutation is unique even if roots collide at t = 0; distinctness is required only on the punctured disc.

theorem TauCeti.eventually_min_analyticOrderAt_root_sub_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {N n a : ℕ} {P : E × ℂ → Polynomial ℂ} {r : Fin n → E × ℂ → ℂ} {u : E × ℂ → ℂ} {x₀ : E} (hr : ∀ (i : Fin n), AnalyticAt ℂ (r i) (x₀, 0)) (hP : ∀ᶠ (b : E × ℂ) in nhds (x₀, 0), P (b.1, b.2 ^ N) = ∏ 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), (P (b.1, b.2 ^ N)).discr = b.2 ^ a * u b) : ∀ᶠ (x : E) in nhds x₀, ∀ (i j : Fin n), min (↑N) (analyticOrderAt (fun (t : ℂ) => r j (x, t) - r i (x, 0)) 0) = min (↑N) (analyticOrderAt (fun (t : ℂ) => r j (x₀, t) - r i (x₀, 0)) 0)

All capped contacts of ramified branches with labelled roots on the hyperplane are locally constant, including contacts between labels colliding there. Analyticity, splitting, and the power-times-unit discriminant identity are only required as germs at the central point.