Ring-homomorphism transport and univariate natDegree bounds for parity factors

This module provides ring-homomorphism transport and univariate natDegree bounds for the parity-amplifying series factors Polynomial.parityFactor and truncated coefficient sums Polynomial.sumCoeffsBelow defined in Complexity.Foundations.Data.Polynomial.ParityAmplifier.

When each input $L_i(T) \in R[T]$ is a univariate polynomial of natDegree at most $d$, the $V^s$-coefficient of $\prod_{i \in I} B_i(L_i(T), V)$ in $R[T][V]$ has natDegree at most $d (\#I + 2 s)$ (Polynomial.natDegree_coeff_prod_parityFactor_le), so every retained coefficient for $s < \ell$ and their sum sumCoeffsBelow ℓ have natDegree at most $d (\#I + 2 (\ell - 1))$ (Polynomial.natDegree_coeff_prod_parityFactor_le_of_lt, Polynomial.natDegree_sumCoeffsBelow_prod_parityFactor_le), matching Lemma 5.2 and equation (5.5) of OpenAI, The Exponential Time Hypothesis is False.

Main results

• Polynomial.map_evalInt, Polynomial.map_parityFactor, Polynomial.map_sumCoeffsBelow: ring-homomorphism transport for evalInt, parityFactor, and sumCoeffsBelow.
• Polynomial.eval_coeff_prod_parityFactor, Polynomial.eval_sumCoeffsBelow_prod_parityFactor: pointwise evaluation of coefficients and truncated sums of products of univariate parity factors.
• Polynomial.natDegree_evalInt_le, Polynomial.natDegree_coeff_parityFactor_le: univariate natDegree bounds for evalInt and single parity-factor coefficients.
• Polynomial.natDegree_coeff_prod_parityFactor_le, Polynomial.natDegree_coeff_prod_parityFactor_le_of_lt, Polynomial.natDegree_sumCoeffsBelow_prod_parityFactor_le: univariate natDegree bounds for products of parity factors and their truncated coefficient sums.

References

• OpenAI, The Exponential Time Hypothesis is False (Lemma 5.2 and Section 5.3)

theorem Polynomial.map_evalInt {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] (φ : A →+* B) (y : A) (p : Polynomial ℤ) : φ (evalInt y p) = evalInt (φ y) p

Any ring homomorphism φ : A →+* B commutes with Polynomial.evalInt.

theorem Polynomial.map_parityFactor {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] (φ : A →+* B) (ℓ : ℕ) (y : A) : map φ (parityFactor ℓ y) = parityFactor ℓ (φ y)

Mapping parityFactor ℓ y coefficientwise by φ : A →+* B yields parityFactor ℓ (φ y).

theorem Polynomial.map_sumCoeffsBelow {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] (φ : A →+* B) (P : Polynomial A) (m : ℕ) : φ (sumCoeffsBelow m P) = sumCoeffsBelow m (map φ P)

Any ring homomorphism φ : A →+* B commutes with sumCoeffsBelow.

theorem Polynomial.eval_coeff_prod_parityFactor {κ : Type u_1} {R : Type u_2} [CommRing R] (I : Finset κ) (ℓ : ℕ) (L : κ → Polynomial R) (s : ℕ) (t : R) : eval t ((∏ i ∈ I, parityFactor ℓ (L i)).coeff s) = (∏ i ∈ I, parityFactor ℓ (eval t (L i))).coeff s

Evaluating the s-th coefficient of ∏ i ∈ I, parityFactor ℓ (L i) at t : R agrees with the s-th coefficient of ∏ i ∈ I, parityFactor ℓ ((L i).eval t).

theorem Polynomial.eval_sumCoeffsBelow_prod_parityFactor {κ : Type u_1} {R : Type u_2} [CommRing R] (I : Finset κ) (ℓ : ℕ) (L : κ → Polynomial R) (m : ℕ) (t : R) : eval t (sumCoeffsBelow m (∏ i ∈ I, parityFactor ℓ (L i))) = sumCoeffsBelow m (∏ i ∈ I, parityFactor ℓ (eval t (L i)))

Evaluating sumCoeffsBelow m of ∏ i ∈ I, parityFactor ℓ (L i) at t : R agrees with sumCoeffsBelow m of ∏ i ∈ I, parityFactor ℓ ((L i).eval t).

theorem Polynomial.natDegree_evalInt_le {R : Type u_2} [CommRing R] (y : Polynomial R) (p : Polynomial ℤ) : (evalInt y p).natDegree ≤ p.natDegree * y.natDegree

For y : R[X] and p : ℤ[X], (evalInt y p).natDegree ≤ p.natDegree * y.natDegree.

theorem Polynomial.natDegree_evalInt_parityBaseDigit_le {R : Type u_2} [CommRing R] (ℓ j : ℕ) (y : Polynomial R) : (evalInt y (parityBaseDigit ℓ j)).natDegree ≤ y.natDegree

evalInt y (parityBaseDigit ℓ j) has natDegree ≤ y.natDegree.

theorem Polynomial.natDegree_evalInt_hPoly_le {R : Type u_2} [CommRing R] (y : Polynomial R) : (evalInt y hPoly).natDegree ≤ 2 * y.natDegree

evalInt y hPoly has natDegree ≤ 2 * y.natDegree.

theorem Polynomial.natDegree_coeff_parityFactor_le {R : Type u_2} [CommRing R] (ℓ : ℕ) (y : Polynomial R) (j : ℕ) : ((parityFactor ℓ y).coeff j).natDegree ≤ (1 + 2 * j) * y.natDegree

The j-th coefficient of parityFactor ℓ y has natDegree ≤ (1 + 2 * j) * y.natDegree.

theorem Polynomial.natDegree_coeff_prod_parityFactor_le {κ : Type u_1} {R : Type u_2} [CommRing R] (I : Finset κ) (ℓ : ℕ) (L : κ → Polynomial R) {d : ℕ} (hL : ∀ i ∈ I, (L i).natDegree ≤ d) (s : ℕ) : ((∏ i ∈ I, parityFactor ℓ (L i)).coeff s).natDegree ≤ d * (I.card + 2 * s)

If every L i (i ∈ I) has natDegree ≤ d, then the V ^ s-coefficient of ∏ i ∈ I, parityFactor ℓ (L i) has natDegree ≤ d * (#I + 2 * s).

theorem Polynomial.natDegree_coeff_prod_parityFactor_le_of_lt {κ : Type u_1} {R : Type u_2} [CommRing R] (I : Finset κ) (ℓ : ℕ) (L : κ → Polynomial R) {d : ℕ} (hL : ∀ i ∈ I, (L i).natDegree ≤ d) {s : ℕ} (hs : s < ℓ) : ((∏ i ∈ I, parityFactor ℓ (L i)).coeff s).natDegree ≤ d * (I.card + 2 * (ℓ - 1))

For s < ℓ, the V ^ s-coefficient of ∏ i ∈ I, parityFactor ℓ (L i) has natDegree ≤ d * (#I + 2 * (ℓ - 1)).

theorem Polynomial.natDegree_sumCoeffsBelow_prod_parityFactor_le {κ : Type u_1} {R : Type u_2} [CommRing R] (I : Finset κ) (ℓ : ℕ) (L : κ → Polynomial R) {d : ℕ} (hL : ∀ i ∈ I, (L i).natDegree ≤ d) : (sumCoeffsBelow ℓ (∏ i ∈ I, parityFactor ℓ (L i))).natDegree ≤ d * (I.card + 2 * (ℓ - 1))

The truncated sum sumCoeffsBelow ℓ (∏ i ∈ I, parityFactor ℓ (L i)) has natDegree ≤ d * (#I + 2 * (ℓ - 1)).