Analytic delineability from constant discriminant order

A real polynomial family with nonzero fibers of constant degree over a connected analytic submanifold has a global analytic delineation when its nonzero formal discriminant has constant ambient order on the base. The ordered real root functions are intrinsically analytic, their positive multiplicities are constant, and the polynomial has constant sign on every section and sector. Moreover, the polynomial, read in all coordinates of the cylinder, has constant ambient order of vanishing along each root section. The formal leading coefficient may vanish on the base, so the fiber degree need not equal the formal degree. Constant polynomials and families without real roots are included.

The chart-local step TauCeti.IsAnalyticChart.exists_delineation_orderAt_prod_eq treats a finite family through its product: it combines the local discriminant-order theorem Polynomial.exists_delineation_of_orderAt_discr_eq with constancy of ambient order on root sections over connected open bases. The global theorem glues these chart-local stacks and adds the intrinsic analytic root-section API. Constancy of ambient order along a section is distinct from constancy of fiber root multiplicity, and is the form needed when McCallum lifting is iterated over the resulting sections.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), 242–268, Sections 2–3.
• 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.IsAnalyticChart.exists_delineation_orderAt_prod_eq {n d : ℕ} {κ : Type u_1} [Fintype κ] {P : κ → Polynomial (MvPolynomial (Fin n) ℝ)} {S : Set (Fin n → ℝ)} {e : OpenPartialHomeomorph (Fin n → ℝ) (Fin n → ℝ)} {x : Fin n → ℝ} (he : IsAnalyticChart d S e) (hxe : x ∈ e.source) (hx : x ∈ S) (hfiber : ∀ (k : κ), ∀ y ∈ S, Polynomial.map (MvPolynomial.eval y) (P k) ≠ 0) (hdegree : ∀ (k : κ), ∀ y ∈ S, ∀ z ∈ S, (Polynomial.map (MvPolynomial.eval y) (P k)).natDegree = (Polynomial.map (MvPolynomial.eval z) (P k)).natDegree) (hdiscr_ne : (∏ k : κ, P k).discr ≠ 0) (hdiscr : ∀ y ∈ S, ∀ z ∈ S, (∏ k : κ, P k).discr.orderAt y = (∏ k : κ, P k).discr.orderAt z) : ∃ (V : Set (Fin d → ℝ)), IsOpen V ∧ (firstCoords ℝ n d) (↑e x) ∈ V ∧ ∃ (D : Delineation fun (k : κ) (u : ↑V) => Polynomial.map (MvPolynomial.eval (↑e.symm ((firstCoords ℝ d n) ↑u))) (P k)), ∀ (i : Fin D.count) (u v : ↑V), ((MvPolynomial.finSuccEquiv ℝ n).symm (∏ k : κ, P k)).orderAt (Fin.cons (D.root i u) (↑e.symm ((firstCoords ℝ d n) ↑u))) = ((MvPolynomial.finSuccEquiv ℝ n).symm (∏ k : κ, P k)).orderAt (Fin.cons (D.root i v) (↑e.symm ((firstCoords ℝ d n) ↑v)))

Chart-local lifting of a non-nullified family. Let e be an analytic chart of S around x ∈ S. If every member of a finite family has nonzero fibers of constant degree over S, and the formal discriminant of the product is nonzero with constant ambient order on S, then the family has a delineation over an open neighbourhood of the chart coordinates of x. Along each of its root sections, the product has constant ambient order.

theorem TauCeti.exists_analytic_delineation_of_orderAt_discr_eq {n d : ℕ} {S : Set (Fin n → ℝ)} {p : Polynomial (MvPolynomial (Fin n) ℝ)} (hS : IsAnalyticSubmanifold d S) (hconn : IsPreconnected S) (hp : ∀ x ∈ S, Polynomial.map (MvPolynomial.eval x) p ≠ 0) (hdegree : ∀ x ∈ S, ∀ y ∈ S, (Polynomial.map (MvPolynomial.eval x) p).natDegree = (Polynomial.map (MvPolynomial.eval y) p).natDegree) (hdiscr : p.discr ≠ 0) (horder : ∀ x ∈ S, ∀ y ∈ S, p.discr.orderAt x = p.discr.orderAt y) : ∃ (D : Delineation fun (x : Unit) (x_1 : ↑S) => Polynomial.map (MvPolynomial.eval ↑x_1) p), (∀ (i : Fin D.count), ∃ (r : (Fin n → ℝ) → ℝ), AnalyticOnSubmanifold d r S ∧ ∀ (x : ↑S), r ↑x = D.root i x) ∧ ∀ (i : Fin D.count) (x y : ↑S), ((MvPolynomial.finSuccEquiv ℝ n).symm p).orderAt (Fin.cons (D.root i x) ↑x) = ((MvPolynomial.finSuccEquiv ℝ n).symm p).orderAt (Fin.cons (D.root i y) ↑y)

Analytic delineability from constant discriminant order. A polynomial with nonzero fibers of constant degree over a preconnected analytic submanifold, whose nonzero formal discriminant has constant ambient order on the base, has a global delineation with intrinsically analytic root functions. Each root function is represented by an ambient function whose values off the base are immaterial. Along each root section, the polynomial, viewed as a polynomial in all n + 1 variables, has constant ambient order of vanishing.

No preservation of the formal degree or nonvanishing of the discriminant values is required. Multiple roots are allowed, and their fiber multiplicities are constant.