Multivariate degree bounds for polynomial coefficients

In Polynomial (MvPolynomial ι R), the outer variable is a Taylor variable z, and the coefficient variables are formal Xᵢ. If coefficient j of every substituted input has multivariate total degree at most j, the same is true after polynomial evaluation.

This is the algebraic closure behind equation (3.9), p24 of OpenAI, The Exponential Time Hypothesis is False. The coefficient ring can be any commutative ring. No Taylor reconstruction, truncation or quotient identification is used.

Main results

• MvPolynomial.totalDegree_coeff_eval₂_le: polynomial substitution preserves the coefficient degree bound.
• MvPolynomial.totalDegree_X_le: every formal variable X i has total degree at most 1.
• MvPolynomial.totalDegree_coeff_X_mul_map_le: a scalar polynomial with zero constant term can multiply a formal variable while preserving the bound.

theorem MvPolynomial.totalDegree_coeff_eval₂_le {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [CommRing R] (p : MvPolynomial κ R) (Q : κ → Polynomial (MvPolynomial ι R)) (hQ : ∀ (v : κ) (j : ℕ), ((Q v).coeff j).totalDegree ≤ j) (j : ℕ) : ((eval₂ (Polynomial.C.comp C) Q p).coeff j).totalDegree ≤ j

If every input's coefficient j has total degree at most j in the formal variables, then every coefficient of the substituted polynomial satisfies the same bound. Constants of R are embedded as constants in both polynomial layers.

theorem MvPolynomial.totalDegree_X_le {ι : Type u_4} {R : Type u_5} [CommSemiring R] (i : ι) : (X i).totalDegree ≤ 1

Every formal variable X i has total degree at most 1, without requiring Nontrivial R.

theorem MvPolynomial.totalDegree_coeff_X_mul_map_le {ι : Type u_1} {R : Type u_3} [CommRing R] (i : ι) (delta : Polynomial R) (hzero : delta.coeff 0 = 0) (j : ℕ) : ((Polynomial.C (X i) * Polynomial.map C delta).coeff j).totalDegree ≤ j

Every formal-variable occurrence in this correction carries a positive power of the outer variable: the scalar polynomial's constant coefficient must be zero. Higher outer powers are allowed, and no nontrivial-ring hypothesis is needed.