Integer parity-amplifying polynomials and shared-total-order truncation

For ℓ ≥ 1, the complement of the Beigel–Tarui modulus-amplifying polynomial Toda, Arora and Barak, Section 17.4, $$p_\ell(Y) = (1 - Y)^\ell \sum_{j=0}^{\ell-1} \binom{\ell - 1 + j}{j} Y^j \in \mathbb{Z}[Y],$$ satisfies $p_\ell(Y) \equiv 1 \pmod{Y^\ell}$ and $p_\ell(Y) \equiv 0 \pmod{(1 - Y)^\ell}$, so for every integer $y \in \mathbb{Z}$, $p_\ell(y) \equiv \mathbf{1}_{\{2 \mid y\}} \pmod{2^\ell}$ (Polynomial.parityAmplifier_eval_modEq_two_pow).

Following Lemma 5.1 and Lemma B.1 of OpenAI, The Exponential Time Hypothesis is False, writing $p_\ell$ in powers of the monic quadratic $h(Y) = Y^2 - Y = Y(Y - 1)$ (Polynomial.hPoly) by successive monic division produces remainders $e_0, \dots, e_{\ell-1} \in \mathbb{Z}[Y]$ (Polynomial.parityBaseDigit) of degree at most $1$ with $p_\ell(Y) = \sum_{j=0}^{\ell-1} e_j(Y) h(Y)^j$ (Polynomial.parityAmplifier_eq_sum_baseDigit) and explicit coefficient bounds (Polynomial.natAbs_coeff_parityBaseDigit_le, Polynomial.coeffNorm1_parityBaseDigit_le).

Since $h(y) = y(y - 1)$ is even for every $y \in \mathbb{Z}$, introducing a shared formal variable $V$ (Polynomial.parityFactor) across a family of equations and discarding powers $V^s$ with $s \ge \ell$ via Polynomial.sumCoeffsBelow (Lemma 5.2 of [OAI26c]) preserves the product of evenness indicators modulo $2^\ell$ (Polynomial.sumCoeffsBelow_prod_parityFactor_modEq), while bounding the multivariate total degree of every retained coefficient and of their sum by $d_* (\#I + 2(\ell - 1))$ when each input polynomial has total degree at most $d_*$ (Polynomial.totalDegree_sumCoeffsBelow_prod_parityFactor_le).

Main definitions

• Polynomial.hPoly: the monic quadratic X ^ 2 - X in ℤ[X].
• Polynomial.parityKernel: the partial binomial series ∑ j < ℓ, choose (ℓ - 1 + j) j * X ^ j.
• Polynomial.parityAmplifier: the even-parity amplifying polynomial p_ℓ(X) ∈ ℤ[X].
• Polynomial.iterDivByH, Polynomial.baseDigitByH, Polynomial.parityBaseDigit: successive monic quotients and linear remainders e_j(X) on division by X ^ 2 - X.
• Polynomial.coeffNorm1: the ℓ₁ coefficient norm ∑ i ∈ p.support, (p.coeff i).natAbs.
• Polynomial.parityFactor: the V-series factor B(y; V) = ∑ j < ℓ, e_j(y) h(y)^j V^j.
• Polynomial.sumCoeffsBelow: the truncated coefficient sum S_ℓ(P) = ∑ s < ℓ, P.coeff s.

Main results

• Polynomial.parityAmplifier_add_X_pow_mul_eq_one: Bezout identity p_ℓ(X) + X ^ ℓ * ∑ m < ℓ, choose (m + ℓ - 1) (ℓ - 1) * (1 - X) ^ m = 1 for ℓ ≥ 1.
• Polynomial.parityAmplifier_eval_modEq_two_pow: p_ℓ(y) ≡ (if Even y then 1 else 0) [ZMOD 2 ^ ℓ].
• Polynomial.parityAmplifier_eq_sum_baseDigit: p_ℓ = ∑ j < ℓ, e_j * (X ^ 2 - X) ^ j.
• Polynomial.coeffNorm1_parityAmplifier_le: ‖p_ℓ‖₁ ≤ 2 ^ (3 * ℓ).
• Polynomial.natAbs_coeff_parityBaseDigit_le: |coeff k (e_j)| ≤ (2 * ℓ) ^ j * 2 ^ (3 * ℓ).
• Polynomial.coeffNorm1_parityBaseDigit_le: ‖e_j‖₁ ≤ 2 * ((2 * ℓ) ^ j * 2 ^ (3 * ℓ)).
• Polynomial.sumCoeffsBelow_prod_parityFactor_modEq: shared-V truncation modulo 2 ^ ℓ.
• Polynomial.totalDegree_sumCoeffsBelow_prod_parityFactor_le: linear total-degree bound totalDegree ≤ d_* * (#I + 2 * (ℓ - 1)).

References

• S. Toda, PP is as hard as the polynomial-time hierarchy
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• OpenAI, The Exponential Time Hypothesis is False (Lemmas 5.1, 5.2, and B.1)

1. The univariate even-parity amplifier p_ℓ(X)

noncomputable def Polynomial.paritySeriesAux (m K : ℕ) : Polynomial ℤ

The partial binomial series g(m, K) = ∑ j ∈ range K, choose (m + j) j * X ^ j in ℤ[X].

noncomputable def Polynomial.parityKernel (ℓ : ℕ) : Polynomial ℤ

The kernel ∑ j ∈ range ℓ, choose (ℓ - 1 + j) j * X ^ j of the even-parity amplifier.

noncomputable def Polynomial.parityAmplifier (ℓ : ℕ) : Polynomial ℤ

The even-parity amplifying polynomial p_ℓ(X) = (1 - X) ^ ℓ * ∑ j ∈ range ℓ, choose (ℓ - 1 + j) j * X ^ j in ℤ[X].

@[simp]

theorem Polynomial.parityAmplifier_zero : parityAmplifier 0 = 0

At precision 0, parityAmplifier 0 is 0.

theorem Polynomial.parityAmplifier_one : parityAmplifier 1 = 1 - X

At precision 1, parityAmplifier 1 = 1 - X.

theorem Polynomial.parityAmplifier_two : parityAmplifier 2 = 1 - 3 * X ^ 2 + 2 * X ^ 3

At precision 2, parityAmplifier 2 = 1 - 3 * X ^ 2 + 2 * X ^ 3.

theorem Polynomial.one_sub_X_pow_dvd_parityAmplifier (ℓ : ℕ) : (1 - X) ^ ℓ ∣ parityAmplifier ℓ

(1 - X) ^ ℓ divides parityAmplifier ℓ in ℤ[X].

theorem Polynomial.parityAmplifier_add_X_pow_mul_eq_one {ℓ : ℕ} (hℓ : 1 ≤ ℓ) : parityAmplifier ℓ + X ^ ℓ * ∑ i ∈ Finset.range ℓ, ↑((i + (ℓ - 1)).choose (ℓ - 1)) * (1 - X) ^ i = 1

Exact Bezout identity for parityAmplifier ℓ (ℓ ≥ 1): p_ℓ(X) + X ^ ℓ * ∑ i ∈ range ℓ, choose (i + ℓ - 1) (ℓ - 1) * (1 - X) ^ i = 1.

theorem Polynomial.X_pow_dvd_one_sub_parityAmplifier {ℓ : ℕ} (hℓ : 1 ≤ ℓ) : X ^ ℓ ∣ 1 - parityAmplifier ℓ

For ℓ ≥ 1, X ^ ℓ divides 1 - parityAmplifier ℓ in ℤ[X].

theorem Polynomial.parityAmplifier_eval_modEq_one_of_even {ℓ : ℕ} (hℓ : 1 ≤ ℓ) {y : ℤ} (hy : Even y) : eval y (parityAmplifier ℓ) ≡ 1 [ZMOD 2 ^ ℓ]

At any even integer y, parityAmplifier ℓ (ℓ ≥ 1) evaluates to 1 modulo 2 ^ ℓ.

theorem Polynomial.parityAmplifier_eval_modEq_zero_of_odd (ℓ : ℕ) {y : ℤ} (hy : Odd y) : eval y (parityAmplifier ℓ) ≡ 0 [ZMOD 2 ^ ℓ]

At any odd integer y, parityAmplifier ℓ evaluates to 0 modulo 2 ^ ℓ.

theorem Polynomial.parityAmplifier_eval_modEq_two_pow {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (y : ℤ) [Decidable (Even y)] : eval y (parityAmplifier ℓ) ≡ if Even y then 1 else 0 [ZMOD 2 ^ ℓ]

Lemma 5.1 (parity congruence): for ℓ ≥ 1 and y ∈ ℤ, p_ℓ(y) ≡ (if Even y then 1 else 0) (mod 2 ^ ℓ).

2. Base-h(X) expansion (h(X) = X ^ 2 - X) and degree bounds

noncomputable def Polynomial.hPoly : Polynomial ℤ

The monic quadratic h(X) = X ^ 2 - X = X * (X - 1) in ℤ[X].

theorem Polynomial.monic_hPoly : hPoly.Monic

hPoly = X ^ 2 - X is monic.

@[simp]

theorem Polynomial.natDegree_hPoly : hPoly.natDegree = 2

hPoly has degree 2.

theorem Polynomial.hPoly_ne_one : hPoly ≠ 1

hPoly is not equal to 1.

def Polynomial.evalInt {A : Type u_1} [CommRing A] (y : A) (P : Polynomial ℤ) : A

Evaluation of an integer polynomial P : ℤ[X] at y : A via the canonical cast ℤ →+* A.

@[simp]

theorem Polynomial.evalInt_int (y : ℤ) (P : Polynomial ℤ) : evalInt y P = eval y P

On ℤ, evalInt coincides with Polynomial.eval.

@[simp]

theorem Polynomial.evalInt_hPoly {A : Type u_1} [CommRing A] (y : A) : evalInt y hPoly = y ^ 2 - y

Evaluating hPoly at y : A gives y ^ 2 - y.

@[simp]

theorem Polynomial.eval_hPoly (y : ℤ) : eval y hPoly = y ^ 2 - y

Evaluating hPoly at y : ℤ gives y ^ 2 - y.

theorem Polynomial.two_dvd_eval_hPoly (y : ℤ) : 2 ∣ eval y hPoly

For every integer y, h(y) = y ^ 2 - y is even.

def Polynomial.iterDivByH (P : Polynomial ℤ) : ℕ → Polynomial ℤ

Iterated monic quotient of P : ℤ[X] on division by hPoly = X ^ 2 - X.

noncomputable def Polynomial.baseDigitByH (P : Polynomial ℤ) (j : ℕ) : Polynomial ℤ

The j-th remainder (iterDivByH P j) %ₘ hPoly in the base-hPoly expansion of P.

noncomputable def Polynomial.parityBaseDigit (ℓ j : ℕ) : Polynomial ℤ

The j-th linear remainder e_j(X) in the base-(X ^ 2 - X) expansion of p_ℓ(X).

theorem Polynomial.natDegree_modByMonic_hPoly_le (P : Polynomial ℤ) : (P %ₘ hPoly).natDegree ≤ 1

Remainder modulo hPoly has degree at most 1.

theorem Polynomial.natDegree_baseDigitByH_le (P : Polynomial ℤ) (j : ℕ) : (P.baseDigitByH j).natDegree ≤ 1

Each baseDigitByH P j has degree at most 1.

theorem Polynomial.natDegree_parityBaseDigit_le (ℓ j : ℕ) : (parityBaseDigit ℓ j).natDegree ≤ 1

Each parityBaseDigit ℓ j (e_j) has degree at most 1.

theorem Polynomial.parityBaseDigit_eq_C_add_C_mul_X (ℓ j : ℕ) : parityBaseDigit ℓ j = C ((parityBaseDigit ℓ j).coeff 0) + C ((parityBaseDigit ℓ j).coeff 1) * X

Explicit affine decomposition e_j(X) = a_j + b_j X of parityBaseDigit ℓ j.

theorem Polynomial.eq_sum_baseDigitByH_add_iterDivByH (P : Polynomial ℤ) (m : ℕ) : P = ∑ j ∈ Finset.range m, P.baseDigitByH j * hPoly ^ j + P.iterDivByH m * hPoly ^ m

Division expansion after m steps of monic division by hPoly: P = (∑ j ∈ range m, baseDigitByH P j * hPoly ^ j) + iterDivByH P m * hPoly ^ m.

theorem Polynomial.natDegree_iterDivByH (P : Polynomial ℤ) (j : ℕ) : (P.iterDivByH j).natDegree = P.natDegree - 2 * j

iterDivByH P j has degree P.natDegree - 2 * j.

theorem Polynomial.iterDivByH_eq_zero_of_natDegree_lt {P : Polynomial ℤ} {j : ℕ} (h : P = 0 ∨ P.natDegree < 2 * j) : P.iterDivByH j = 0

iterDivByH P j vanishes once P.natDegree < 2 * j (or P = 0).

theorem Polynomial.natDegree_parityKernel_le (ℓ : ℕ) : (parityKernel ℓ).natDegree ≤ ℓ - 1

parityKernel ℓ has degree at most ℓ - 1.

theorem Polynomial.natDegree_parityAmplifier_le (ℓ : ℕ) : (parityAmplifier ℓ).natDegree ≤ 2 * ℓ - 1

parityAmplifier ℓ has degree at most 2 * ℓ - 1.

theorem Polynomial.iterDivByH_parityAmplifier_self (ℓ : ℕ) : (parityAmplifier ℓ).iterDivByH ℓ = 0

After ℓ divisions by hPoly, the quotient of parityAmplifier ℓ is 0.

theorem Polynomial.parityAmplifier_eq_sum_baseDigit (ℓ : ℕ) : parityAmplifier ℓ = ∑ j ∈ Finset.range ℓ, parityBaseDigit ℓ j * hPoly ^ j

Lemma 5.1 (base-h decomposition): for every ℓ : ℕ, parityAmplifier ℓ = ∑ j ∈ range ℓ, parityBaseDigit ℓ j * hPoly ^ j.

theorem Polynomial.evalInt_parityAmplifier_eq_sum {A : Type u_1} [CommRing A] (ℓ : ℕ) (y : A) : evalInt y (parityAmplifier ℓ) = ∑ j ∈ Finset.range ℓ, evalInt y (parityBaseDigit ℓ j) * (y ^ 2 - y) ^ j

Evaluation of parityAmplifier ℓ in any commutative ring A via parityBaseDigit.

3. Coefficient and ℓ₁-norm bounds (Lemma B.1)

theorem Polynomial.coeffNorm1_parityKernel_le (ℓ : ℕ) : (parityKernel ℓ).coeffNorm1 ≤ 2 ^ (2 * ℓ)

The ℓ₁ norm of parityKernel ℓ is at most 2 ^ (2 * ℓ).

theorem Polynomial.coeffNorm1_parityAmplifier_le (ℓ : ℕ) : (parityAmplifier ℓ).coeffNorm1 ≤ 2 ^ (3 * ℓ)

Lemma B.1 (ℓ₁-norm of p_ℓ): ‖p_ℓ‖₁ ≤ 2 ^ (3 * ℓ).

theorem Polynomial.coeff_divByMonic_hPoly_rec (p : Polynomial ℤ) (n : ℕ) : (p /ₘ hPoly).coeff n = p.coeff (n + 2) + (p /ₘ hPoly).coeff (n + 1)

Recurrence for the coefficients of the quotient p /ₘ hPoly.

theorem Polynomial.coeff_divByMonic_hPoly_sum (p : Polynomial ℤ) (n m : ℕ) : (p /ₘ hPoly).coeff n = ∑ t ∈ Finset.range m, p.coeff (n + 2 + t) + (p /ₘ hPoly).coeff (n + m)

Telescoping sum formula for the coefficients of p /ₘ hPoly.

theorem Polynomial.coeff_modByMonic_hPoly_zero (p : Polynomial ℤ) : (p %ₘ hPoly).coeff 0 = p.coeff 0

The constant coefficient of p %ₘ hPoly equals p.coeff 0.

theorem Polynomial.coeff_modByMonic_hPoly_one (p : Polynomial ℤ) : (p %ₘ hPoly).coeff 1 = p.coeff 1 + (p /ₘ hPoly).coeff 0

The linear coefficient of p %ₘ hPoly equals p.coeff 1 + (p /ₘ hPoly).coeff 0.

theorem Polynomial.natAbs_coeff_divByMonic_hPoly_le (p : Polynomial ℤ) (n : ℕ) : ((p /ₘ hPoly).coeff n).natAbs ≤ p.coeffNorm1

Every coefficient of p /ₘ hPoly has absolute value at most coeffNorm1 p.

theorem Polynomial.natAbs_coeff_modByMonic_hPoly_le (p : Polynomial ℤ) (k : ℕ) : ((p %ₘ hPoly).coeff k).natAbs ≤ p.coeffNorm1

Every coefficient of p %ₘ hPoly has absolute value at most coeffNorm1 p.

theorem Polynomial.coeffNorm1_modByMonic_hPoly_le (p : Polynomial ℤ) : (p %ₘ hPoly).coeffNorm1 ≤ 2 * p.coeffNorm1

The ℓ₁ norm of p %ₘ hPoly is at most 2 * coeffNorm1 p.

theorem Polynomial.coeffNorm1_divByMonic_hPoly_le (p : Polynomial ℤ) : (p /ₘ hPoly).coeffNorm1 ≤ p.natDegree * p.coeffNorm1

The ℓ₁ norm of p /ₘ hPoly is at most p.natDegree * coeffNorm1 p.

theorem Polynomial.coeffNorm1_iterDivByH_le (p : Polynomial ℤ) (j : ℕ) : (p.iterDivByH j).coeffNorm1 ≤ p.natDegree ^ j * p.coeffNorm1

After j monic divisions by hPoly, coeffNorm1 (iterDivByH p j) is at most p.natDegree ^ j * coeffNorm1 p.

theorem Polynomial.natAbs_coeff_parityBaseDigit_le (ℓ j k : ℕ) : ((parityBaseDigit ℓ j).coeff k).natAbs ≤ (2 * ℓ) ^ j * 2 ^ (3 * ℓ)

Lemma B.1 (coefficient bound for e_j): every coefficient of parityBaseDigit ℓ j has absolute value at most (2 * ℓ) ^ j * 2 ^ (3 * ℓ).

theorem Polynomial.coeffNorm1_parityBaseDigit_le (ℓ j : ℕ) : (parityBaseDigit ℓ j).coeffNorm1 ≤ 2 * ((2 * ℓ) ^ j * 2 ^ (3 * ℓ))

Lemma B.1 (ℓ₁-norm bound for e_j): ‖parityBaseDigit ℓ j‖₁ is at most 2 * ((2 * ℓ) ^ j * 2 ^ (3 * ℓ)).

4. Shared-total-order truncation and multivariate total-degree bound (Lemma 5.2)

noncomputable def Polynomial.parityFactor {A : Type u_1} [CommRing A] (ℓ : ℕ) (y : A) : Polynomial A

The V-series factor B(y; V) = ∑ j ∈ range ℓ, e_j(y) h(y)^j V^j in A[X], where the polynomial indeterminate X represents the shared formal truncation marker V.

def Polynomial.sumCoeffsBelow {A : Type u_1} [Semiring A] (ℓ : ℕ) (P : Polynomial A) : A

The linear map S_ℓ(∑_s b_s V^s) = ∑ s ∈ range ℓ, b_s summing the coefficients of V ^ 0, …, V ^ (ℓ - 1).

theorem Polynomial.coeff_parityFactor {A : Type u_1} [CommRing A] (ℓ : ℕ) (y : A) (s : ℕ) : (parityFactor ℓ y).coeff s = if s < ℓ then evalInt y (parityBaseDigit ℓ s) * evalInt y hPoly ^ s else 0

The s-th coefficient of parityFactor ℓ y is e_s(y) h(y)^s for s < ℓ and 0 otherwise.

theorem Polynomial.eval_one_parityFactor {A : Type u_1} [CommRing A] (ℓ : ℕ) (y : A) : eval 1 (parityFactor ℓ y) = evalInt y (parityAmplifier ℓ)

Evaluating parityFactor ℓ y at V = 1 recovers p_ℓ(y).

theorem Polynomial.two_pow_dvd_coeff_parityFactor (ℓ : ℕ) (y : ℤ) (s : ℕ) : 2 ^ s ∣ (parityFactor ℓ y).coeff s

At an integer y, the s-th coefficient of parityFactor ℓ y is divisible by 2 ^ s.

theorem Polynomial.two_pow_dvd_coeff_mul {P Q : Polynomial ℤ} (hP : ∀ (s : ℕ), 2 ^ s ∣ P.coeff s) (hQ : ∀ (s : ℕ), 2 ^ s ∣ Q.coeff s) (s : ℕ) : 2 ^ s ∣ (P * Q).coeff s

Graded divisibility 2 ^ s ∣ coeff s is preserved under polynomial multiplication.

theorem Polynomial.two_pow_dvd_coeff_prod_parityFactor {ι : Type u_1} (I : Finset ι) (ℓ : ℕ) (y : ι → ℤ) (s : ℕ) : 2 ^ s ∣ (∏ i ∈ I, parityFactor ℓ (y i)).coeff s

Every V ^ s-coefficient of ∏ i ∈ I, parityFactor ℓ (y i) at integer arguments y i is divisible by 2 ^ s.

theorem Polynomial.sumCoeffsBelow_modEq_eval_one {P : Polynomial ℤ} {ℓ : ℕ} (hP : ∀ (s : ℕ), 2 ^ s ∣ P.coeff s) : sumCoeffsBelow ℓ P ≡ eval 1 P [ZMOD 2 ^ ℓ]

If 2 ^ s ∣ P.coeff s for all s, then sumCoeffsBelow ℓ P ≡ P.eval 1 (mod 2 ^ ℓ).

theorem Polynomial.sumCoeffsBelow_prod_parityFactor_modEq {ι : Type u_1} (I : Finset ι) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (y : ι → ℤ) [(i : ι) → Decidable (Even (y i))] : sumCoeffsBelow ℓ (∏ i ∈ I, parityFactor ℓ (y i)) ≡ ∏ i ∈ I, if Even (y i) then 1 else 0 [ZMOD 2 ^ ℓ]

Lemma 5.2 (shared-V truncation congruence): for ℓ ≥ 1 and integers y i, S_ℓ(∏ i ∈ I, B_i(V)) ≡ ∏ i ∈ I, (if Even (y i) then 1 else 0) (mod 2 ^ ℓ).

theorem Polynomial.totalDegree_evalInt_of_natDegree_le_one {σ : Type u_1} {R : Type u_2} [CommRing R] {q : Polynomial ℤ} (hq : q.natDegree ≤ 1) {y : MvPolynomial σ R} {d : ℕ} (hy : y.totalDegree ≤ d) : (evalInt y q).totalDegree ≤ d

Evaluating an affine integer polynomial (natDegree ≤ 1) at y : MvPolynomial σ R preserves any upper bound d on y.totalDegree.

theorem Polynomial.totalDegree_evalInt_hPoly_le {σ : Type u_1} {R : Type u_2} [CommRing R] {y : MvPolynomial σ R} {d : ℕ} (hy : y.totalDegree ≤ d) : (evalInt y hPoly).totalDegree ≤ 2 * d

Evaluating hPoly = X ^ 2 - X at y : MvPolynomial σ R of total degree at most d gives a polynomial of total degree at most 2 * d.

theorem Polynomial.totalDegree_coeff_parityFactor_le {σ : Type u_1} {R : Type u_2} [CommRing R] (ℓ : ℕ) {y : MvPolynomial σ R} {d : ℕ} (hy : y.totalDegree ≤ d) (s : ℕ) : ((parityFactor ℓ y).coeff s).totalDegree ≤ d + 2 * d * s

For y : MvPolynomial σ R of total degree at most d, the V ^ s-coefficient of parityFactor ℓ y has total degree at most d + 2 * d * s.

theorem Polynomial.totalDegree_coeff_mul_le {σ : Type u_1} {R : Type u_2} [CommRing R] {P Q : Polynomial (MvPolynomial σ R)} {M₁ M₂ d : ℕ} (hP : ∀ (s : ℕ), (P.coeff s).totalDegree ≤ M₁ + 2 * d * s) (hQ : ∀ (s : ℕ), (Q.coeff s).totalDegree ≤ M₂ + 2 * d * s) (s : ℕ) : ((P * Q).coeff s).totalDegree ≤ M₁ + M₂ + 2 * d * s

Graded total-degree bounds totalDegree (coeff s) ≤ M + 2 * d * s add in the offset M under multiplication in (MvPolynomial σ R)[X].

theorem Polynomial.totalDegree_coeff_prod_parityFactor_le {ι : Type u_1} {σ : Type u_2} {R : Type u_3} [CommRing R] (I : Finset ι) (ℓ : ℕ) {y : ι → MvPolynomial σ R} {d : ℕ} (hy : ∀ i ∈ I, (y i).totalDegree ≤ d) (s : ℕ) : ((∏ i ∈ I, parityFactor ℓ (y i)).coeff s).totalDegree ≤ d * (I.card + 2 * s)

Lemma 5.2 (graded total-degree bound): if every y i (i ∈ I) has multivariate total degree at most d, then the V ^ s-coefficient of ∏ i ∈ I, parityFactor ℓ (y i) has total degree at most d * (#I + 2 * s).

theorem Polynomial.totalDegree_coeff_prod_parityFactor_le_of_lt {ι : Type u_1} {σ : Type u_2} {R : Type u_3} [CommRing R] (I : Finset ι) {ℓ s : ℕ} (hs : s < ℓ) {y : ι → MvPolynomial σ R} {d : ℕ} (hy : ∀ i ∈ I, (y i).totalDegree ≤ d) : ((∏ i ∈ I, parityFactor ℓ (y i)).coeff s).totalDegree ≤ d * (I.card + 2 * (ℓ - 1))

Lemma 5.2 (retained coefficient total-degree bound): for s < ℓ, the V ^ s-coefficient of ∏ i ∈ I, parityFactor ℓ (y i) has total degree at most d * (#I + 2 * (ℓ - 1)).

theorem Polynomial.totalDegree_sumCoeffsBelow_prod_parityFactor_le {ι : Type u_1} {σ : Type u_2} {R : Type u_3} [CommRing R] (I : Finset ι) (ℓ : ℕ) {y : ι → MvPolynomial σ R} {d : ℕ} (hy : ∀ i ∈ I, (y i).totalDegree ≤ d) : (sumCoeffsBelow ℓ (∏ i ∈ I, parityFactor ℓ (y i))).totalDegree ≤ d * (I.card + 2 * (ℓ - 1))

Lemma 5.2 (truncated sum total-degree bound): the truncated coefficient sum sumCoeffsBelow ℓ (∏ i ∈ I, parityFactor ℓ (y i)) has total degree at most d * (#I + 2 * (ℓ - 1)).