Gluing local Lazard delineations

Lazard delineations on ambient open neighborhoods glue over a nonempty preconnected base. The increasing order of the real roots removes any permutation ambiguity on overlaps. Consequently, the number and multiplicities of the roots, as well as the exponent vectors removed by Lazard evaluation, are globally constant.

Unlike gluing ordinary delineations, this argument does not require the ordinary fibers, or even the degrees of the Lazard evaluations, to be locally constant. It uses only the complete ordered root lists and exponent data already contained in each local Lazard delineation. This is the local-to-global step used when analytic preparation constructs roots in charts of a connected analytic submanifold.

The root lists are glued by TauCeti.exists_roots_of_locally from TauCeti.Analysis.Polynomial.RealRoots.Common, which is shared with TauCeti.nonempty_delineation_of_locally; the gluing of the removed exponent vectors adapts the same locally-constant argument.

Main result

• TauCeti.nonempty_lazardDelineation_of_locally: local Lazard delineations on ambient open neighborhoods glue to a Lazard delineation over a nonempty preconnected base.

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 5.2.

theorem TauCeti.nonempty_lazardDelineation_of_locally {n : ℕ} {ι : Type u_1} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (hS : IsPreconnected S) (hSne : S.Nonempty) (hlocal : ∀ (x : ↑S), ∃ (U : Set (Fin n → ℝ)), IsOpen U ∧ ↑x ∈ U ∧ Nonempty (LazardDelineation F (S ∩ U))) : Nonempty (LazardDelineation F S)

Local Lazard delineations on ambient open neighborhoods glue over a nonempty preconnected base. The local root counts, root multiplicities, and removed base-exponent vectors may depend on the neighborhood; their global constancy is a conclusion.