Real roots on the exceptional hyperplane of a Puiseux splitting

A complete analytic complex splitting with discriminant a power of the distinguished coordinate times an analytic unit yields analytic real root branches on the hyperplane. Restrict to an analytic real parametrization on which the polynomial has real coefficients. The labels that are real at the central parameter stay real nearby, and they cover exactly the real roots. The first construction retains repeated labels. The ordered construction removes repeated labels on a common open neighborhood and retains constant positive root multiplicities.

The discriminant condition prevents a collision class from splitting along the hyperplane. Conjugation and continuity then prevent a real class from leaving the real line. This is the descent step from complex root splittings to real analytic sections, including sections of multiplicity greater than one. Construction of the complex splitting is a separate input.

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.exists_analyticAt_real_roots_on_hyperplane {E : Type u_1} {B : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup B] [NormedSpace ℝ B] {n a : ℕ} {P : E × ℂ → Polynomial ℂ} {r : Fin n → E × ℂ → ℂ} {φ : B → E} {b₀ : B} {F : B → Polynomial ℝ} {u : E × ℂ → ℂ} (hr : ∀ (i : Fin n), AnalyticAt ℂ (r i) (φ b₀, 0)) (hP : ∀ᶠ (p : E × ℂ) in nhds (φ b₀, 0), P p = ∏ i : Fin n, (Polynomial.X - Polynomial.C (r i p))) (hu : AnalyticAt ℂ u (φ b₀, 0)) (hu0 : u (φ b₀, 0) ≠ 0) (hdiscr : ∀ᶠ (p : E × ℂ) in nhds (φ b₀, 0), (P p).discr = p.2 ^ a * u p) (hφ : AnalyticAt ℝ φ b₀) (hreal : ∀ᶠ (b : B) in nhds b₀, P (φ b, 0) = Polynomial.map (algebraMap ℝ ℂ) (F b)) : ∃ (s : { i : Fin n // (r i (φ b₀, 0)).im = 0 } → B → ℝ), (∀ (i : { i : Fin n // (r i (φ b₀, 0)).im = 0 }), AnalyticAt ℝ (s i) b₀) ∧ ∀ᶠ (b : B) in nhds b₀, (∀ (i : { i : Fin n // (r i (φ b₀, 0)).im = 0 }), ↑(s i b) = r ↑i (φ b, 0)) ∧ ∀ (t : ℝ), (F b).IsRoot t ↔ ∃ (i : { i : Fin n // (r i (φ b₀, 0)).im = 0 }), s i b = t

A complete analytic complex splitting with power-times-unit discriminant restricts on the distinguished hyperplane to a complete local list of analytic real roots. The list is indexed by precisely the labels real at the central parameter and agrees with those complex branches on one common neighborhood. Collisions on the hyperplane are allowed; repeated labels are retained. No conjugation permutation or constancy of the real labels is assumed.

theorem TauCeti.exists_analyticOnNhd_ordered_real_roots_on_hyperplane {E : Type u_1} {B : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup B] [NormedSpace ℝ B] {n a : ℕ} {P : E × ℂ → Polynomial ℂ} {r : Fin n → E × ℂ → ℂ} {φ : B → E} {b₀ : B} {F : B → Polynomial ℝ} {u : E × ℂ → ℂ} (hr : ∀ (i : Fin n), AnalyticAt ℂ (r i) (φ b₀, 0)) (hP : ∀ᶠ (p : E × ℂ) in nhds (φ b₀, 0), P p = ∏ i : Fin n, (Polynomial.X - Polynomial.C (r i p))) (hu : AnalyticAt ℂ u (φ b₀, 0)) (hu0 : u (φ b₀, 0) ≠ 0) (hdiscr : ∀ᶠ (p : E × ℂ) in nhds (φ b₀, 0), (P p).discr = p.2 ^ a * u p) (hφ : AnalyticAt ℝ φ b₀) (hreal : ∀ᶠ (b : B) in nhds b₀, P (φ b, 0) = Polynomial.map (algebraMap ℝ ℂ) (F b)) : ∃ (k : ℕ) (s : Fin k → B → ℝ) (U : Set B), IsOpen U ∧ b₀ ∈ U ∧ (∀ (i : Fin k), AnalyticOnNhd ℝ (s i) U) ∧ (∀ b ∈ U, StrictMono fun (i : Fin k) => s i b) ∧ (∀ b ∈ U, ∀ (t : ℝ), (F b).IsRoot t ↔ ∃ (i : Fin k), s i b = t) ∧ (∀ (i : Fin k), 0 < Polynomial.rootMultiplicity (s i b₀) (F b₀)) ∧ ∀ b ∈ U, ∀ (i : Fin k), Polynomial.rootMultiplicity (s i b) (F b) = Polynomial.rootMultiplicity (s i b₀) (F b₀)

A prepared analytic complex splitting gives a complete, strictly ordered analytic list of real roots on the distinguished hyperplane, with constant positive multiplicities. The neighborhood, distinct root count, and multiplicities are conclusions.