Analytic real roots in reciprocal coordinates

An analytic enumeration of the distinct real roots of a fixed-bound reflection descends locally to an ordered analytic enumeration of the original polynomial's roots. The original fibers must have nonzero constant coefficient and constant degree. The excess of the reflection bound over that degree produces a zero root, which is discarded before taking reciprocals. All remaining roots retain their multiplicities.

This allows a monic root construction in reciprocal coordinates to give finite root sections of a nonmonic family, even when its degree is smaller than the formal reflection bound. The root sections of the reflected family are inputs; no root enumeration of the original family is assumed. No continuity of the coefficients is needed for this transport.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), Sections 2–3 (local delineability in reciprocal coordinates).

theorem TauCeti.exists_analyticOnNhd_ordered_roots_of_reflect {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Finite ι] {F : E → Polynomial ℝ} {r : ι → E → ℝ} {x₀ : E} {N d : ℕ} (hr : ∀ (i : ι), AnalyticAt ℝ (r i) x₀) (hinj : Function.Injective fun (i : ι) => r i x₀) (hdN : d ≤ N) (hdeg : ∀ᶠ (x : E) in nhds x₀, (F x).natDegree = d) (hzero : ∀ᶠ (x : E) in nhds x₀, Polynomial.eval 0 (F x) ≠ 0) (hroots : ∀ᶠ (x : E) in nhds x₀, ∀ (t : ℝ), (Polynomial.reflect N (F x)).IsRoot t ↔ ∃ (i : ι), r i x = t) (hmult : ∀ᶠ (x : E) in nhds x₀, ∀ (i : ι), r i x₀ ≠ 0 → Polynomial.rootMultiplicity (r i x) (Polynomial.reflect N (F x)) = Polynomial.rootMultiplicity (r i x₀) (Polynomial.reflect N (F x₀))) : ∃ (k : ℕ) (s : Fin k → E → ℝ) (U : Set E), IsOpen U ∧ x₀ ∈ U ∧ (∀ (i : Fin k), AnalyticOnNhd ℝ (s i) U) ∧ (∀ x ∈ U, StrictMono fun (i : Fin k) => s i x) ∧ (∀ x ∈ U, ∀ (t : ℝ), (F x).IsRoot t ↔ ∃ (i : Fin k), s i x = t) ∧ (∀ (i : Fin k), 0 < Polynomial.rootMultiplicity (s i x₀) (F x₀)) ∧ ∀ x ∈ U, ∀ (i : Fin k), Polynomial.rootMultiplicity (s i x) (F x) = Polynomial.rootMultiplicity (s i x₀) (F x₀)

Descend analytic distinct real root sections of a fixed-bound reflection by discarding its zero section and taking reciprocals. On a common open neighborhood the resulting roots are strictly ordered, cover every real root of the original family, and have constant positive multiplicities. Constant fibers and an empty list of finite roots are included.

theorem TauCeti.exists_analyticOnNhd_ordered_roots_of_reflect_comp_X_add_C {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Finite ι] {F : E → Polynomial ℝ} {r : ι → E → ℝ} {x₀ : E} {N d : ℕ} {τ : ℝ} (hr : ∀ (i : ι), AnalyticAt ℝ (r i) x₀) (hinj : Function.Injective fun (i : ι) => r i x₀) (hdN : d ≤ N) (hdeg : ∀ᶠ (x : E) in nhds x₀, (F x).natDegree = d) (hτ : ∀ᶠ (x : E) in nhds x₀, Polynomial.eval τ (F x) ≠ 0) (hroots : ∀ᶠ (x : E) in nhds x₀, ∀ (t : ℝ), (Polynomial.reflect N ((F x).comp (Polynomial.X + Polynomial.C τ))).IsRoot t ↔ ∃ (i : ι), r i x = t) (hmult : ∀ᶠ (x : E) in nhds x₀, ∀ (i : ι), r i x₀ ≠ 0 → Polynomial.rootMultiplicity (r i x) (Polynomial.reflect N ((F x).comp (Polynomial.X + Polynomial.C τ))) = Polynomial.rootMultiplicity (r i x₀) (Polynomial.reflect N ((F x₀).comp (Polynomial.X + Polynomial.C τ)))) : ∃ (k : ℕ) (s : Fin k → E → ℝ) (U : Set E), IsOpen U ∧ x₀ ∈ U ∧ (∀ (i : Fin k), AnalyticOnNhd ℝ (s i) U) ∧ (∀ x ∈ U, StrictMono fun (i : Fin k) => s i x) ∧ (∀ x ∈ U, ∀ (t : ℝ), (F x).IsRoot t ↔ ∃ (i : Fin k), s i x = t) ∧ (∀ (i : Fin k), 0 < Polynomial.rootMultiplicity (s i x₀) (F x₀)) ∧ ∀ x ∈ U, ∀ (i : Fin k), Polynomial.rootMultiplicity (s i x) (F x) = Polynomial.rootMultiplicity (s i x₀) (F x₀)

Descend from translated reciprocal coordinates. The translation center τ is chosen away from the roots of the original fibers. Reflection uses a fixed bound N, allowing fiber degrees strictly below that bound. The finite roots of the original family form a strictly ordered analytic list with constant positive multiplicities on a neighborhood.