Uniform expansions along monomial curves

Suppose the Taylor coefficients of a polynomial p below an exponent v in lexicographic order vanish at every point of a set S. An evaluator c separates v from all larger exponents by weighted degree. There is then a single polynomial remainder, with coefficients polynomial in the center a, such that on S

p(a + y^c) = y^(weight c v) * (p_{a,v} + y * R(a,y)).

The coefficient ring can itself be a polynomial ring in a further variable. In that case the identity retains that variable, even when ordinary specialization vanishes identically. The least removed Lazard exponent on a set supplies the required vanishing of lower coefficients; for nonzero p, the leading term at every point attaining that minimum is its nonzero Lazard evaluation. This uniform identity is used to deform Lazard evaluations into ordinary fibers.

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. See arXiv:1607.00264v2, Section 5.1, Proposition 5.6, equation (8).

theorem MvPolynomial.exists_aeval_monomialCurve_eq_pow_mul {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [CommSemiring R] (p : MvPolynomial σ R) {S : Set (σ → R)} {V : Set (σ →₀ ℕ)} {v : σ →₀ ℕ} {c : σ → ℕ} (hv : v ∈ V) (hc : TauCeti.IsLazardEvaluator V c) (hzero : ∀ a ∈ S, ∀ (u : σ →₀ ℕ), toLex u < toLex v → ((taylor a) p).coeff u = 0) : ∃ (Q : Polynomial (MvPolynomial σ R)), ∀ a ∈ S, (aeval (monomialCurve a c)) p = Polynomial.X ^ (Finsupp.weight c) v * (Polynomial.C (((taylor a) p).coeff v) + Polynomial.X * Polynomial.map (eval a) Q)

If all Taylor coefficients lexicographically below v vanish on S, restriction to a monomial curve with evaluator c factors uniformly as X^(weight c v) times the sum of the coefficient at v and X times a remainder polynomial. The remainder is polynomial in the center and the curve parameter, not a separately chosen polynomial at each center. No nonvanishing of the coefficient at v is required.

theorem MvPolynomial.exists_isLazardEvaluator_aeval_monomialCurve_eq_pow_mul {R : Type u_1} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) {S : Set (Fin n → R)} (hS : S.Nonempty) {V : Set (Fin n →₀ ℕ)} (hV : V.Finite) : ∃ (c : Fin n → ℕ) (v : Fin n →₀ ℕ) (Q : Polynomial (MvPolynomial (Fin n) R)), TauCeti.IsLazardEvaluator (p.lazardExponent '' S ∪ V) c ∧ v ∈ p.lazardExponent '' S ∧ ∀ a ∈ S, toLex v ≤ toLex (p.lazardExponent a) ∧ (aeval (monomialCurve a c)) p = Polynomial.X ^ (Finsupp.weight c) v * (Polynomial.C (((taylor a) p).coeff v) + Polynomial.X * Polynomial.map (eval a) Q)

On any nonempty set of base points, choose an evaluator for all removed Lazard exponents and a prescribed finite set V of other exponents, and the lexicographic minimum of the removed exponents. The polynomial admits a single remainder expansion on the whole set with that minimum as the common factored exponent. For R = A[Z], the remainder retains Z as well as the center and the monomial-curve parameter. The coefficient at the minimum may vanish at points with a larger removed exponent. The extra set V allows the same curve to detect the valuations of leading coefficients, trailing coefficients, and discriminants.