Affine Taylor substitutions and restricted-subset jet coefficients

Given scalar replacement rows P f v : ι → Polynomial A for multivariate polynomial factors Φ f : MvPolynomial (κ f) A over any commutative ring A, equation (3.3) of OpenAI, The Exponential Time Hypothesis is False forms the univariate sum replacedSum s Φ P = ∑ x : ι → Bool, ∏ f ∈ s, Φ_f(⟨P_{f,v}(T), x⟩) in Polynomial A.

In §3.4 (equations (3.7)–(3.10), p. 24), fixing an evaluation node t : A and an original Boolean assignment x : ι → Bool, each factor input is split into its scalar baseline at t plus formal variables X i multiplied by the scalar Taylor corrections taylor t (P f v i) - C ((P f v i).eval t) (Cslib.AffineTaylor.affineInput). Because every scalar Taylor correction has zero constant coefficient (Cslib.AffineTaylor.coeff_zero_taylor_sub_C_eval), the j-th outer Taylor coefficient of the full factor product Cslib.AffineTaylor.factorProduct has multivariate total degree at most j (Cslib.AffineTaylor.totalDegree_coeff_factorProduct_le). Evaluating the formal variables diagonally at x recovers Polynomial.taylor t (replacedSum s Φ P) (Cslib.AffineTaylor.taylor_replacedSum_eq_sum_map_eval), and Boolean Möbius reconstruction then expresses every jet coefficient of order j ≤ q through restricted sums with G_x still indexed by the original assignment x (Cslib.AffineTaylor.coeff_taylor_replacedSum_eq_restricted_subsets).

No quotient ring truncation, Hermite interpolation, or enumeration complexity claim is made here.

Main definitions

• Cslib.AffineTaylor.affineInput: the affine/Taylor input polynomial in Polynomial (MvPolynomial ι A) (equation (3.7)).
• Cslib.AffineTaylor.affineFactor: a single multivariate factor evaluated at affineInput.
• Cslib.AffineTaylor.factorProduct: the full affine/Taylor factor product G_x(X, z) over f ∈ s (equation (3.8)).
• Cslib.AffineTaylor.replacedSum: the scalar polynomial H(T) summed over the Boolean cube (equation (3.3)).

Main results

• Cslib.AffineTaylor.coeff_zero_taylor_sub_C_eval, Cslib.AffineTaylor.X_dvd_taylor_sub_C_eval: every scalar Taylor correction has zero constant term and is divisible by X.
• Cslib.AffineTaylor.totalDegree_coeff_affineInput_le, Cslib.AffineTaylor.totalDegree_coeff_affineFactor_le, Cslib.AffineTaylor.totalDegree_coeff_factorProduct_le: multivariate degree bound ≤ j on the j-th Taylor coefficient (equation (3.9)).
• Cslib.AffineTaylor.map_eval_self_factorProduct, Cslib.AffineTaylor.taylor_replacedSum_eq_sum_map_eval: diagonal evaluation at x recovers the Taylor shift H(t + z) (equation (3.8)).
• Cslib.AffineTaylor.coeff_taylor_replacedSum_eq_restricted_subsets: exact restricted-subset identity for [z^j] H(t + z) whenever j ≤ q (equations (3.9)–(3.10)).

References

• OpenAI, The Exponential Time Hypothesis is False, §3.1 equation (3.3) and §3.4 equations (3.7)–(3.10), p. 24.

Scalar Taylor corrections

theorem Cslib.AffineTaylor.coeff_zero_taylor_sub_C_eval {A : Type u_1} [CommRing A] (t : A) (p : Polynomial A) : ((Polynomial.taylor t) p - Polynomial.C (Polynomial.eval t p)).coeff 0 = 0

Subtracting p.eval t from the Taylor shift Polynomial.taylor t p kills the constant coefficient ([z^0] (p(t + z) - p(t)) = 0).

theorem Cslib.AffineTaylor.X_dvd_taylor_sub_C_eval {A : Type u_1} [CommRing A] (t : A) (p : Polynomial A) : Polynomial.X ∣ (Polynomial.taylor t) p - Polynomial.C (Polynomial.eval t p)

Every scalar Taylor correction p(t + z) - p(t) is divisible by the outer variable X.

Affine/Taylor inputs and factor products

noncomputable def Cslib.AffineTaylor.affineInput {A : Type u_1} [CommRing A] {ι : Type u_2} [Fintype ι] (row : ι → Polynomial A) (t : A) (x : ι → Bool) : Polynomial (MvPolynomial ι A)

The affine/Taylor input polynomial ⟨row(t), x⟩ + ⟨Δrow(z), X⟩ in Polynomial (MvPolynomial ι A) (equation (3.7) of [OAI26c]). The outer indeterminate is the Taylor variable z, the constant baseline captures x at node t, and each formal variable X i carries the zero-constant scalar correction taylor t (row i) - C ((row i).eval t).

noncomputable def Cslib.AffineTaylor.affineFactor {A : Type u_1} [CommRing A] {ι : Type u_2} [Fintype ι] {σ : Type u_5} (Φ : MvPolynomial σ A) (rows : σ → ι → Polynomial A) (t : A) (x : ι → Bool) : Polynomial (MvPolynomial ι A)

A single multivariate factor Φ evaluated at the affine/Taylor input rows for node t and Boolean assignment x.

noncomputable def Cslib.AffineTaylor.factorProduct {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) (x : ι → Bool) : Polynomial (MvPolynomial ι A)

The full affine/Taylor factor product G_x(X, z) over all factors f ∈ s (equation (3.8) of [OAI26c]).

noncomputable def Cslib.AffineTaylor.replacedSum {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) : Polynomial A

The univariate polynomial H(T) = ∑ x, ∏ f ∈ s, Φ_f(⟨P_{f,v}(T), x⟩) summed over all Boolean assignments x : ι → Bool (equation (3.3) of [OAI26c]).

@[simp]

theorem Cslib.AffineTaylor.factorProduct_empty {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) (x : ι → Bool) : factorProduct ∅ Φ P t x = 1

@[simp]

theorem Cslib.AffineTaylor.replacedSum_empty {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) : replacedSum ∅ Φ P = 2 ^ Fintype.card ι

theorem Cslib.AffineTaylor.affineInput_congr_baseline {A : Type u_1} [CommRing A] {ι : Type u_2} [Fintype ι] {row : ι → Polynomial A} {t : A} {x x' : ι → Bool} (h : ∑ i : ι, Polynomial.eval t (row i) * BitString.bitVal A (x i) = ∑ i : ι, Polynomial.eval t (row i) * BitString.bitVal A (x' i)) : affineInput row t x = affineInput row t x'

affineInput depends on the Boolean assignment x only through its scalar baseline ∑ i, (row i).eval t * bitVal A (x i) at node t.

theorem Cslib.AffineTaylor.affineFactor_congr_baseline {A : Type u_1} [CommRing A] {ι : Type u_2} [Fintype ι] {σ : Type u_5} (Φ : MvPolynomial σ A) {rows : σ → ι → Polynomial A} {t : A} {x x' : ι → Bool} (h : ∀ (v : σ), ∑ i : ι, Polynomial.eval t (rows v i) * BitString.bitVal A (x i) = ∑ i : ι, Polynomial.eval t (rows v i) * BitString.bitVal A (x' i)) : affineFactor Φ rows t x = affineFactor Φ rows t x'

affineFactor depends on x only through the scalar baselines of its rows at node t.

Coefficient total-degree bounds

theorem Cslib.AffineTaylor.totalDegree_coeff_affineInput_le {A : Type u_1} [CommRing A] {ι : Type u_2} [Fintype ι] (row : ι → Polynomial A) (t : A) (x : ι → Bool) (j : ℕ) : ((affineInput row t x).coeff j).totalDegree ≤ j

Every outer Taylor coefficient j of affineInput has multivariate total degree at most j in the formal variables X.

theorem Cslib.AffineTaylor.totalDegree_coeff_affineFactor_le {A : Type u_1} [CommRing A] {ι : Type u_2} [Fintype ι] {σ : Type u_5} (Φ : MvPolynomial σ A) (rows : σ → ι → Polynomial A) (t : A) (x : ι → Bool) (j : ℕ) : ((affineFactor Φ rows t x).coeff j).totalDegree ≤ j

Every outer Taylor coefficient j of affineFactor has multivariate total degree at most j in the formal variables X.

theorem Cslib.AffineTaylor.totalDegree_coeff_factorProduct_le {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) (x : ι → Bool) (j : ℕ) : ((factorProduct s Φ P t x).coeff j).totalDegree ≤ j

Every outer Taylor coefficient j of the full factor product factorProduct has multivariate total degree at most j in the formal variables X (equation (3.9) of [OAI26c]).

Evaluation in formal variables and diagonal Taylor shift

theorem Cslib.AffineTaylor.map_eval_affineInput {A : Type u_1} [CommRing A] {ι : Type u_2} [Fintype ι] (row : ι → Polynomial A) (t : A) (x : ι → Bool) (y : ι → A) : Polynomial.map (MvPolynomial.eval y) (affineInput row t x) = Polynomial.C (∑ i : ι, Polynomial.eval t (row i) * BitString.bitVal A (x i)) + ∑ i : ι, Polynomial.C (y i) * ((Polynomial.taylor t) (row i) - Polynomial.C (Polynomial.eval t (row i)))

Evaluating the formal variables X of affineInput at any y : ι → A yields the scalar polynomial with baseline at x and Taylor corrections weighted by y.

theorem Cslib.AffineTaylor.map_eval_self_affineInput {A : Type u_1} [CommRing A] {ι : Type u_2} [Fintype ι] (row : ι → Polynomial A) (t : A) (x : ι → Bool) : Polynomial.map (MvPolynomial.eval fun (i : ι) => BitString.bitVal A (x i)) (affineInput row t x) = (Polynomial.taylor t) (∑ i : ι, row i * Polynomial.C (BitString.bitVal A (x i)))

Evaluating the formal variables X of affineInput diagonally at x cancels the baseline subtraction and produces the Taylor shift of ∑ i, row i * C (bitVal A (x i)) at t.

theorem Cslib.AffineTaylor.map_eval_affineFactor {A : Type u_1} [CommRing A] {ι : Type u_2} [Fintype ι] {σ : Type u_5} (Φ : MvPolynomial σ A) (rows : σ → ι → Polynomial A) (t : A) (x : ι → Bool) (y : ι → A) : Polynomial.map (MvPolynomial.eval y) (affineFactor Φ rows t x) = (MvPolynomial.aeval fun (v : σ) => Polynomial.map (MvPolynomial.eval y) (affineInput (rows v) t x)) Φ

Evaluating the formal variables X of affineFactor at y : ι → A pushes inside the factor evaluation.

theorem Cslib.AffineTaylor.map_eval_factorProduct {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) (x : ι → Bool) (y : ι → A) : Polynomial.map (MvPolynomial.eval y) (factorProduct s Φ P t x) = ∏ f ∈ s, Polynomial.map (MvPolynomial.eval y) (affineFactor (Φ f) (P f) t x)

Evaluating the formal variables X of factorProduct at y : ι → A factors over s.

theorem Cslib.AffineTaylor.eval_coeff_factorProduct {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) (x : ι → Bool) (y : ι → A) (j : ℕ) : (MvPolynomial.eval y) ((factorProduct s Φ P t x).coeff j) = (∏ f ∈ s, Polynomial.map (MvPolynomial.eval y) (affineFactor (Φ f) (P f) t x)).coeff j

Evaluating the j-th coefficient of factorProduct at y : ι → A agrees with taking the j-th coefficient after substituting X ↦ y into each factor.

theorem Cslib.AffineTaylor.map_eval_self_affineFactor {A : Type u_1} [CommRing A] {ι : Type u_2} [Fintype ι] {σ : Type u_5} (Φ : MvPolynomial σ A) (rows : σ → ι → Polynomial A) (t : A) (x : ι → Bool) : Polynomial.map (MvPolynomial.eval fun (i : ι) => BitString.bitVal A (x i)) (affineFactor Φ rows t x) = (Polynomial.taylor t) ((MvPolynomial.aeval fun (v : σ) => ∑ i : ι, rows v i * Polynomial.C (BitString.bitVal A (x i))) Φ)

Diagonal formal evaluation of affineFactor at x equals the Taylor shift of the scalar factor polynomial at t.

theorem Cslib.AffineTaylor.map_eval_self_factorProduct {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) (x : ι → Bool) : Polynomial.map (MvPolynomial.eval fun (i : ι) => BitString.bitVal A (x i)) (factorProduct s Φ P t x) = (Polynomial.taylor t) (∏ f ∈ s, (MvPolynomial.aeval fun (v : κ f) => ∑ i : ι, P f v i * Polynomial.C (BitString.bitVal A (x i))) (Φ f))

Diagonal formal evaluation of factorProduct at x equals the Taylor shift of the scalar product of factors at t (equation (3.8) of [OAI26c]).

theorem Cslib.AffineTaylor.taylor_replacedSum_eq_sum_map_eval {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) : (Polynomial.taylor t) (replacedSum s Φ P) = ∑ x : ι → Bool, Polynomial.map (MvPolynomial.eval fun (i : ι) => BitString.bitVal A (x i)) (factorProduct s Φ P t x)

Summing the diagonal formal evaluations of factorProduct over the Boolean cube yields the Taylor shift Polynomial.taylor t (replacedSum s Φ P) (∑_x G_x(x, z) = H(t + z), equation (3.8) of [OAI26c]).

theorem Cslib.AffineTaylor.eval_replacedSum {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) : Polynomial.eval t (replacedSum s Φ P) = ∑ x : ι → Bool, ∏ f ∈ s, (MvPolynomial.eval fun (v : κ f) => ∑ i : ι, Polynomial.eval t (P f v i) * BitString.bitVal A (x i)) (Φ f)

Scalar evaluation of replacedSum at any point t : A.

Restricted-subset Taylor jet identity

theorem Cslib.AffineTaylor.coeff_taylor_replacedSum_eq_sum_eval {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) (j : ℕ) : ((Polynomial.taylor t) (replacedSum s Φ P)).coeff j = ∑ x : ι → Bool, (MvPolynomial.eval fun (i : ι) => BitString.bitVal A (x i)) ((factorProduct s Φ P t x).coeff j)

The j-th Taylor coefficient of replacedSum at t is the Boolean-cube sum of the diagonal evaluations of (factorProduct s Φ P t x).coeff j.

theorem Cslib.AffineTaylor.coeff_taylor_replacedSum_eq_restricted_subsets {A : Type u_1} [CommRing A] {ι : Type u_2} {F : Type u_3} {κ : F → Type u_4} [Fintype ι] (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) {j q : ℕ} (hj : j ≤ q) : ((Polynomial.taylor t) (replacedSum s Φ P)).coeff j = ∑ E ∈ Finset.univ.powerset with E.card ≤ q, ∑ U ∈ E.powerset, (-1) ^ (E.card - U.card) * ∑ x : ι → Bool with ∀ i ∈ E, x i = true, (MvPolynomial.eval fun (i : ι) => BitString.bitVal A (decide (i ∈ U))) ((factorProduct s Φ P t x).coeff j)

Restricted-subset Taylor jet identity (equations (3.9)–(3.10), p. 24 of [OAI26c]). For every outer order j ≤ q and node t : A, the j-th Taylor coefficient of replacedSum at t equals the signed Möbius sum over pairs U ⊆ E with #E ≤ q of restricted cube sums in which (factorProduct s Φ P t x).coeff j remains indexed by the original assignment x while its formal variables are evaluated at the indicator of U.