Lazard delineation of the distinguished coordinate

Every nonzero constant multiple of the last coordinate polynomial has one constant root section, at zero, over every nonempty base. Its Lazard evaluation in the base variables is the corresponding constant multiple of the univariate polynomial X: no base power is removed, and its root has multiplicity one. This supplies the exceptional coordinate factor in Lazard lifting, for which the usual nonzero-trailing-coefficient preparation does not apply.

Such coordinate members can be adjoined to a Lazard delineation of the remaining members over a preconnected base, provided that for each remaining member, 0 is a root of its Lazard evaluations either over every base point or over none. Then either some root function vanishes identically, and the root list is kept, or 0 lies in one fixed sector over every base point (since no root function changes sign), and the zero section is inserted there. Without the hypothesis on the root 0, a root function could cross zero, as for Xₙ - X₀ over ℝ. The hypothesis holds for every member whose formal constant coefficient has constant Lazard valuation on the base. In particular, a Lazard delineation of q gives one of X * q when the constant coefficient of q has constant Lazard valuation.

Main results

• TauCeti.lazardDelineationCMulLastCoordinate: the one-section Lazard delineation of a nonzero constant multiple of the last coordinate polynomial.
• TauCeti.nonempty_lazardDelineation_lastCoordinate: the specialization to the monic coordinate.
• TauCeti.nonempty_lazardDelineation_of_comp: adjoining nonzero multiples of the last coordinate to a family with a Lazard delineation.
• TauCeti.LazardDelineation.isRoot_zero_of_lazardValuation_coeff_zero_eq: constant valuation of the constant coefficient decides the root 0 uniformly.
• TauCeti.nonempty_lazardDelineation_X_mul: multiplying a delineated polynomial by the distinguished coordinate.

References

S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), Section 5.

noncomputable def TauCeti.lazardDelineationCMulLastCoordinate {n : ℕ} {S : Set (Fin n → ℝ)} (hS : S.Nonempty) {a : ℝ} (ha : a ≠ 0) : LazardDelineation (fun (x : Unit) => MvPolynomial.C a * MvPolynomial.X (Fin.last n)) S

A nonzero constant multiple of the distinguished (last) coordinate polynomial has the constant root section zero as its Lazard delineation over every nonempty base. No base-variable powers are removed, and the root has multiplicity one. This includes every associate of the coordinate polynomial over ℝ.

@[simp]

theorem TauCeti.lazardDelineationCMulLastCoordinate_count {n : ℕ} {S : Set (Fin n → ℝ)} (hS : S.Nonempty) {a : ℝ} (ha : a ≠ 0) : (lazardDelineationCMulLastCoordinate hS ha).count = 1

@[simp]

theorem TauCeti.lazardDelineationCMulLastCoordinate_root {n : ℕ} {S : Set (Fin n → ℝ)} (hS : S.Nonempty) {a : ℝ} (ha : a ≠ 0) (i : Fin (lazardDelineationCMulLastCoordinate hS ha).count) (x : ↑S) : (lazardDelineationCMulLastCoordinate hS ha).root i x = 0

@[simp]

theorem TauCeti.lazardDelineationCMulLastCoordinate_exponent {n : ℕ} {S : Set (Fin n → ℝ)} (hS : S.Nonempty) {a : ℝ} (ha : a ≠ 0) (k : Unit) : (lazardDelineationCMulLastCoordinate hS ha).exponent k = 0

@[simp]

theorem TauCeti.lazardDelineationCMulLastCoordinate_multiplicity {n : ℕ} {S : Set (Fin n → ℝ)} (hS : S.Nonempty) {a : ℝ} (ha : a ≠ 0) (k : Unit) (i : Fin (lazardDelineationCMulLastCoordinate hS ha).count) : (lazardDelineationCMulLastCoordinate hS ha).multiplicity k i = 1

theorem TauCeti.nonempty_lazardDelineation_lastCoordinate {n : ℕ} {S : Set (Fin n → ℝ)} (hS : S.Nonempty) : Nonempty (LazardDelineation (fun (x : Unit) => MvPolynomial.X (Fin.last n)) S)

The distinguished coordinate itself has the constant root section zero over every nonempty base.

theorem TauCeti.nonempty_lazardDelineation_of_comp {n : ℕ} {S : Set (Fin n → ℝ)} {ι : Type u_1} {κ : Type u_2} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {f : κ → ι} (D : LazardDelineation (F ∘ f) S) (hS : IsPreconnected S) (hcoord : ∀ k ∉ Set.range f, ∃ (a : ℝ), a ≠ 0 ∧ F k = MvPolynomial.C a * MvPolynomial.X (Fin.last n)) (hzero : ∀ (j : κ) (x y : ↑S), (((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F (f j)))).lazardEval (⇑Polynomial.C ∘ ↑x)).IsRoot 0 → (((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F (f j)))).lazardEval (⇑Polynomial.C ∘ ↑y)).IsRoot 0) : Nonempty (LazardDelineation F S)

Adjoining the distinguished coordinate. Let D be a Lazard delineation of the members F ∘ f of a family over a preconnected base, and suppose every member of F outside the range of f is a nonzero constant multiple of the last coordinate polynomial. If, for each member of F ∘ f, whether 0 is a root of its Lazard evaluation does not depend on the base point, then the whole family F has a Lazard delineation over the base.

Its root functions are those of D, together with the zero section when coordinate members occur and 0 is not already a root function of D.

theorem TauCeti.LazardDelineation.isRoot_zero_of_lazardValuation_coeff_zero_eq {n : ℕ} {S : Set (Fin n → ℝ)} {ι : Type u_1} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} (D : LazardDelineation F S) {k : ι} {f : Polynomial (MvPolynomial (Fin n) ℝ)} (hf : F k = (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm f)) (hval : ∀ x ∈ S, ∀ y ∈ S, (f.coeff 0).lazardValuation x = (f.coeff 0).lazardValuation y) (x y : ↑S) (hx : (((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F k))).lazardEval (⇑Polynomial.C ∘ ↑x)).IsRoot 0) : (((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F k))).lazardEval (⇑Polynomial.C ∘ ↑y)).IsRoot 0

The root 0 from the constant coefficient. Let F k be the polynomial in n + 1 variables corresponding to a polynomial f in the distinguished variable. Over the base of a Lazard delineation of F, if the formal constant coefficient of f has constant Lazard valuation, then 0 is a root of the Lazard evaluations of F k over every base point or over none.

theorem TauCeti.nonempty_lazardDelineation_X_mul {n : ℕ} {S : Set (Fin n → ℝ)} {q : Polynomial (MvPolynomial (Fin n) ℝ)} (hq : q ≠ 0) (D : LazardDelineation (fun (x : Unit) => (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm q)) S) (hS : IsPreconnected S) (hval : ∀ x ∈ S, ∀ y ∈ S, (q.coeff 0).lazardValuation x = (q.coeff 0).lazardValuation y) : Nonempty (LazardDelineation (fun (x : Unit) => (MvPolynomial.rename ⇑finSuccEquivLast.symm) ((MvPolynomial.optionEquivLeft ℝ (Fin n)).symm (Polynomial.X * q))) S)

Multiplying by the distinguished coordinate. Let q be a nonzero polynomial in the distinguished variable whose formal constant coefficient has constant Lazard valuation on a preconnected base. A Lazard delineation of q over the base gives one of X * q: the zero section is adjoined unless 0 is already a root function.