Beigel–Tarui parity-amplifier coefficients and staged factor jet evaluation

Lemma 5.1 and Appendix B.1–B.2 of OpenAI, The Exponential Time Hypothesis is False expand $p_\ell(Y) = (1 - Y)^\ell \sum_{j < \ell} \binom{\ell + j - 1}{j} Y^j$ in powers of $h(Y) = Y (Y - 1)$ with linear remainders $a_{\ell, s} + b_{\ell, s} Y$, and evaluate a single parity-amplifier factor on a fixed-denominator $z$-jet cleared by $\Gamma = \Delta^{2 \ell - 1}$.

• Cslib.polyAdd, Cslib.mulZJet, Cslib.polyMul, Cslib.divModByH: executable univariate polynomial and 1D $z$-jet arithmetic bridged to Polynomial.ofCoeffList, Polynomial.coeffNorm1, and monic division by Polynomial.hPoly.
• Cslib.parityLinearCoeffs, Cslib.evalParityAmplifier: $(a_{\ell, s}, b_{\ell, s})$ expansion bridged to Polynomial.parityAmplifier and Polynomial.parityBaseDigit, parity congruence mod $2^\ell$, $2^{7 \ell^2}$ magnitude bound, and ComputableInPolyTime.
• Cslib.evalParityFactorJet: $\Gamma$-cleared $J \times \ell$ factor table built with Cslib.tabulateTable and Cslib.rowEntry, bridged to Cslib.IsTableShape, Cslib.jetL1Norm, and Cslib.BitString.parityFactorCleared, with $\mathbb{Z}[X]$ / $\mathbb{Q}[X]$ ($\Delta \ne 0$) / $j = 0$ identities, Appendix B.2 norm/bit bounds, and ComputableInPolyTime.

Coefficient $\ell_1$-norms and list/polynomial helpers

def Cslib.polyNorm1 (p : List ℤ) : ℕ

The $\ell_1$-norm $\sum_i |c_i|$ of an integer coefficient list.

theorem Cslib.jetL1Norm_eq_sum_map_polyNorm1 (rows : List (List ℤ)) : jetL1Norm rows = (List.map polyNorm1 rows).sum

Cslib.jetL1Norm equals the sum of Cslib.polyNorm1 across rows.

theorem Cslib.polyNorm1_nil : polyNorm1 [] = 0

polyNorm1 of the empty coefficient list is 0.

theorem Cslib.polyNorm1_cons (c : ℤ) (p : List ℤ) : polyNorm1 (c :: p) = c.natAbs + polyNorm1 p

polyNorm1 of c :: p adds c.natAbs to polyNorm1 p.

theorem Cslib.polyNorm1_append (p q : List ℤ) : polyNorm1 (p ++ q) = polyNorm1 p + polyNorm1 q

polyNorm1 is additive across list concatenation.

theorem Cslib.polyNorm1_reverse (p : List ℤ) : polyNorm1 p.reverse = polyNorm1 p

Reversing a coefficient list preserves polyNorm1.

theorem Cslib.polyNorm1_take_le (p : List ℤ) (n : ℕ) : polyNorm1 (List.take n p) ≤ polyNorm1 p

Taking a prefix does not increase polyNorm1.

theorem Cslib.natAbs_mem_le_polyNorm1 {p : List ℤ} {z : ℤ} (hz : z ∈ p) : z.natAbs ≤ polyNorm1 p

Every coefficient z ∈ p has z.natAbs ≤ polyNorm1 p.

theorem Cslib.polyNorm1_le_length_mul {p : List ℤ} {B : ℕ} (h : ∀ z ∈ p, z.natAbs ≤ B) : polyNorm1 p ≤ p.length * B

Uniform entrywise magnitude bound B implies polyNorm1 p ≤ p.length * B.

theorem Cslib.length_encIntBin_le_of_natAbs_le {z : ℤ} {e : ℕ} (hz : z.natAbs ≤ 2 ^ e) : (Turing.MultiTapeTM.encIntBin z).length ≤ e + 2

Bounding z.natAbs ≤ 2 ^ e bounds (encIntBin z).length ≤ e + 2.

Univariate polynomial and 1D $z$-jet primitives

def Cslib.polyAdd (p q : List ℤ) : List ℤ

Addition of univariate integer polynomials represented by low-first coefficient lists.

def Cslib.cauchyCoeff (p q : List ℤ) (k : ℕ) : ℤ

The $k$-th Cauchy-product coefficient $\sum_{i \le k} p_i q_{k - i}$.

def Cslib.mulZJet (J : ℕ) (u v : List ℤ) : List ℤ

1D truncated $z$-jet Cauchy product $(u \cdot v) \bmod z^J$ of length $J$.

def Cslib.polyMul (p q : List ℤ) : List ℤ

Multiplication of univariate integer polynomials represented by low-first coefficient lists.

def Cslib.ParityFactorEval.divModByHStep (state : List ℤ × ℤ × ℤ) (c : ℤ) : List ℤ × ℤ × ℤ

Single Horner-division step for monic division by $Y^2 - Y$.

def Cslib.divModByH (p : List ℤ) : List ℤ × ℤ × ℤ

Monic division of p by $h(Y) = Y^2 - Y$ with linear remainder (a, b).

theorem Cslib.getD_polyAdd (p q : List ℤ) (i : ℕ) : (polyAdd p q).getD i 0 = p.getD i 0 + q.getD i 0

Entrywise getD specification of polyAdd.

theorem Cslib.ofCoeffList_polyAdd (p q : List ℤ) : Polynomial.ofCoeffList (polyAdd p q) = Polynomial.ofCoeffList p + Polynomial.ofCoeffList q

polyAdd represents polynomial addition under Polynomial.ofCoeffList.

theorem Cslib.polyNorm1_polyAdd_le (p q : List ℤ) : polyNorm1 (polyAdd p q) ≤ polyNorm1 p + polyNorm1 q

Triangle inequality for polyNorm1 of polyAdd.

@[simp]

theorem Cslib.length_mulZJet (J : ℕ) (u v : List ℤ) : (mulZJet J u v).length = J

mulZJet J u v has length J.

theorem Cslib.coeff_ofCoeffList_mulZJet {J j : ℕ} (hj : j < J) (u v : List ℤ) : (Polynomial.ofCoeffList (mulZJet J u v)).coeff j = (Polynomial.ofCoeffList u * Polynomial.ofCoeffList v).coeff j

Below J, ofCoeffList (mulZJet J u v) has the same coefficients as ofCoeffList u * ofCoeffList v.

theorem Cslib.getD_mulZJet_of_lt {J j : ℕ} (hj : j < J) (u v : List ℤ) : (mulZJet J u v).getD j 0 = (Polynomial.ofCoeffList (List.take J u) * Polynomial.ofCoeffList (List.take J v)).coeff j

Coefficient specification of mulZJet on degree-$< J$ prefixes.

theorem Cslib.ofCoeffList_polyMul (p q : List ℤ) : Polynomial.ofCoeffList (polyMul p q) = Polynomial.ofCoeffList p * Polynomial.ofCoeffList q

polyMul represents polynomial multiplication under Polynomial.ofCoeffList.

theorem Cslib.polyNorm1_mulZJet_le (J : ℕ) (u v : List ℤ) : polyNorm1 (mulZJet J u v) ≤ polyNorm1 (List.take J u) * polyNorm1 (List.take J v)

Submultiplicativity of polyNorm1 under truncated $z$-jet multiplication mulZJet.

theorem Cslib.polyNorm1_polyMul_le (p q : List ℤ) : polyNorm1 (polyMul p q) ≤ polyNorm1 p * polyNorm1 q

Submultiplicativity of polyNorm1 under polyMul.

theorem Cslib.ofCoeffList_divModByH (p : List ℤ) : Polynomial.ofCoeffList p = Polynomial.ofCoeffList (divModByH p).1 * (Polynomial.X ^ 2 - Polynomial.X) + (Polynomial.C (divModByH p).2.1 + Polynomial.C (divModByH p).2.2 * Polynomial.X)

Polynomial division identity for divModByH dividing by $X^2 - X$.

@[simp]

theorem Cslib.length_divModByH_fst (p : List ℤ) : (divModByH p).1.length = p.length

Quotient length invariant of divModByH.

theorem Cslib.natAbs_divModByH_snd_le (p : List ℤ) : (divModByH p).2.1.natAbs ≤ polyNorm1 p ∧ (divModByH p).2.2.natAbs ≤ polyNorm1 p

Linear remainder magnitude bound for divModByH ([OAI26c], Lemma B.1).

theorem Cslib.polyNorm1_divModByH_fst_le (p : List ℤ) : polyNorm1 (divModByH p).1 ≤ p.length * polyNorm1 p

Quotient $\ell_1$-norm bound for divModByH ([OAI26c], Lemma B.1).

theorem Cslib.divByMonic_and_modByMonic_hPoly_ofCoeffList (p : List ℤ) : Polynomial.ofCoeffList p /ₘ Polynomial.hPoly = Polynomial.ofCoeffList (divModByH p).1 ∧ Polynomial.ofCoeffList p %ₘ Polynomial.hPoly = Polynomial.C (divModByH p).2.1 + Polynomial.C (divModByH p).2.2 * Polynomial.X

divModByH computes the exact monic quotient and remainder on division by Polynomial.hPoly = X ^ 2 - X.

Beigel–Tarui parity-amplifier coefficients (parityLinearCoeffs)

def Cslib.ParityFactorEval.prefixSumPoly (v : List ℤ) : List ℤ

Prefix-sum step mapping $v$ to $(\sum_{i \le j} v_i)_{j < |v|}$.

def Cslib.ParityFactorEval.taylorInvOneSubPow (ℓ : ℕ) : List ℤ

Degree-$< \ell$ Taylor inverse of $(1 - Y)^\ell$ modulo $Y^\ell$.

def Cslib.ParityFactorEval.oneSubPow (ℓ : ℕ) : List ℤ

Coefficient list of $(1 - Y)^\ell$.

def Cslib.parityPolyCoeffs (ℓ : ℕ) : List ℤ

Coefficient list of $p_\ell(Y) = (1 - Y)^\ell \sum_{j < \ell} \binom{\ell + j - 1}{j} Y^j$.

def Cslib.ParityFactorEval.parityDivStep (state : List ℤ × List (ℤ × ℤ)) : List ℤ × List (ℤ × ℤ)

Single outer division step appending the linear remainder of divModByH.

def Cslib.parityLinearCoeffs (ℓ : ℕ) : List (ℤ × ℤ)

Executable Beigel–Tarui linear remainder table [(a_0, b_0), ..., (a_{ℓ-1}, b_{ℓ-1})] expanding $p_\ell(Y) = \sum_{s < \ell} (a_s + b_s Y) (Y (Y - 1))^s$.

def Cslib.evalParityAmplifier (ℓ : ℕ) (y : ℤ) : ℤ

Integer evaluation of the Beigel–Tarui $(a_s, b_s)$ expansion in powers of $y (y - 1)$.

theorem Cslib.ofCoeffList_parityPolyCoeffs_eq_parityAmplifier (ℓ : ℕ) : Polynomial.ofCoeffList (parityPolyCoeffs ℓ) = Polynomial.parityAmplifier ℓ

parityPolyCoeffs ℓ represents Polynomial.parityAmplifier ℓ under Polynomial.ofCoeffList.

theorem Cslib.ofCoeffList_parityPolyCoeffs {ℓ : ℕ} (hℓ : 1 ≤ ℓ) : Polynomial.ofCoeffList (parityPolyCoeffs ℓ) = (1 - Polynomial.X) ^ ℓ * ∑ j ∈ Finset.range ℓ, Polynomial.C ↑((ℓ + j - 1).choose j) * Polynomial.X ^ j

Polynomial specification of parityPolyCoeffs for $1 \le \ell$.

@[simp]

theorem Cslib.length_parityLinearCoeffs (ℓ : ℕ) : (parityLinearCoeffs ℓ).length = ℓ

parityLinearCoeffs ℓ has length ℓ.

theorem Cslib.getD_parityLinearCoeffs_eq_parityBaseDigit (ℓ s : ℕ) : (parityLinearCoeffs ℓ).getD s (0, 0) = ((Polynomial.parityBaseDigit ℓ s).coeff 0, (Polynomial.parityBaseDigit ℓ s).coeff 1)

Entry s of parityLinearCoeffs ℓ equals the (coeff 0, coeff 1) pair of Polynomial.parityBaseDigit ℓ s.

theorem Cslib.ofCoeffList_parityPolyCoeffs_eq_sum (ℓ : ℕ) : Polynomial.ofCoeffList (parityPolyCoeffs ℓ) = ∑ s ∈ Finset.range ℓ, (Polynomial.C ((parityLinearCoeffs ℓ).getD s (0, 0)).1 + Polynomial.C ((parityLinearCoeffs ℓ).getD s (0, 0)).2 * Polynomial.X) * (Polynomial.X ^ 2 - Polynomial.X) ^ s

Exact $\mathbb{Z}[X]$ identity expanding $p_\ell(X)$ in powers of $X^2 - X$.

theorem Cslib.evalParityAmplifier_eq_eval_parityAmplifier (ℓ : ℕ) (y : ℤ) : evalParityAmplifier ℓ y = Polynomial.eval y (Polynomial.parityAmplifier ℓ)

evalParityAmplifier ℓ y agrees with (Polynomial.parityAmplifier ℓ).eval y.

theorem Cslib.evalParityAmplifier_eq {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (y : ℤ) : evalParityAmplifier ℓ y = (1 - y) ^ ℓ * ∑ j ∈ Finset.range ℓ, ↑((ℓ + j - 1).choose j) * y ^ j

For $1 \le \ell$ and every integer $y$, the $(a_{\ell, s}, b_{\ell, s})$ expansion evaluates to $p_\ell(y) = (1 - y)^\ell \sum_{j < \ell} \binom{\ell + j - 1}{j} y^j$.

theorem Cslib.evalParityAmplifier_modEq {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (y : ℤ) : evalParityAmplifier ℓ y ≡ if 2 ∣ y then 1 else 0 [ZMOD 2 ^ ℓ]

Beigel–Tarui parity amplification ([OAI26c], Lemma 5.1): for $1 \le \ell$ and every $y \in \mathbb{Z}$, $p_\ell(y) \equiv [2 \mid y] \pmod{2^\ell}$.

Magnitude and bit-length bounds for parityLinearCoeffs (Lemma B.1)

theorem Cslib.natAbs_mem_parityLinearCoeffs_le {ℓ : ℕ} {ab : ℤ × ℤ} (hab : ab ∈ parityLinearCoeffs ℓ) : ab.1.natAbs ≤ 2 ^ (7 * ℓ ^ 2) ∧ ab.2.natAbs ≤ 2 ^ (7 * ℓ ^ 2)

Coefficient magnitude bound ([OAI26c], Lemma B.1): every pair $(a_s, b_s)$ in parityLinearCoeffs ℓ has $|a_s|, |b_s| \le 2^{7 \ell^2}$.

theorem Cslib.length_encIntBin_mem_parityLinearCoeffs_le {ℓ : ℕ} {ab : ℤ × ℤ} (hab : ab ∈ parityLinearCoeffs ℓ) : (Turing.MultiTapeTM.encIntBin ab.1).length ≤ 7 * ℓ ^ 2 + 2 ∧ (Turing.MultiTapeTM.encIntBin ab.2).length ≤ 7 * ℓ ^ 2 + 2

Coefficient bit-length bound ([OAI26c], Lemma B.1): every coefficient in parityLinearCoeffs ℓ uses at most $7 \ell^2 + 2$ bits under encIntBin.

Staged fixed-denominator factor jet evaluation (evalParityFactorJet)

def Cslib.truncZJet (J : ℕ) (u : List ℤ) : List ℤ

Truncate or zero-pad a 1D integer $z$-jet to length $J$.

def Cslib.powZJet (J : ℕ) (u : List ℤ) (s : ℕ) : List ℤ

1D truncated $z$-jet power $u^s \bmod z^J$ of length $J$.

def Cslib.ParityFactorEval.colJet (J ℓ : ℕ) (Δ : ℤ) (yJet : List ℤ) (coeffs : List (ℤ × ℤ)) (hJet : List ℤ) (s : ℕ) : List ℤ

Column-$s$ cleared $z$-jet $\Delta^{2 (\ell - 1 - s)} (\Delta a_s + b_s Y) (Y (Y - \Delta))^s$ of length $J$.

def Cslib.ParityFactorEval.cols (J ℓ : ℕ) (Δ : ℤ) (yJet : List ℤ) : List (List ℤ)

Column list (colJet ... s)_{s < ℓ} for evalParityFactorJet.

def Cslib.evalParityFactorJet (J ℓ : ℕ) (Δ : ℤ) (yJet : List ℤ) : List (List ℤ)

Staged fixed-denominator parity-factor jet evaluation ([OAI26c], Appendix B.2): returns a $J \times \ell$ integer table (J rows of length ℓ) whose entry (j, s) (j < J, s < ℓ) is unconditionally (including when $\Delta = 0$) the $z^j$ coefficient of the homogenized integer polynomial $\Delta^{2 (\ell - 1 - s)} (\Delta a_s + b_s \widetilde{Y}(z)) (\widetilde{Y}(z) (\widetilde{Y}(z) - \Delta))^s \bmod z^J$ for $\widetilde{Y}(z) = \sum_{r < J} \text{yJet}[r] z^r$. When $\Delta \ne 0$, this equals the $z^j$ coefficient of $\Gamma \cdot (a_s + b_s Y(z)) (Y(z) (Y(z) - 1))^s \bmod z^J$ for $Y(z) = \Delta^{-1} \widetilde{Y}(z)$ and $\Gamma = \Delta^{2 \ell - 1}$ (see evalParityFactorJet_entry_cast_rat; for $\Delta = 0$, e.g. evalParityFactorJet 1 1 0 [1] = [[-1]], whereas the rational expression has $\Gamma = 0$).

@[simp]

theorem Cslib.length_truncZJet (J : ℕ) (u : List ℤ) : (truncZJet J u).length = J

truncZJet J u has length J.

@[simp]

theorem Cslib.length_powZJet (J : ℕ) (u : List ℤ) (s : ℕ) : (powZJet J u s).length = J

powZJet J u s has length J.

theorem Cslib.isTableShape_evalParityFactorJet (J ℓ : ℕ) (Δ : ℤ) (yJet : List ℤ) : IsTableShape J ℓ (evalParityFactorJet J ℓ Δ yJet)

evalParityFactorJet J ℓ Δ yJet has rectangular shape J × ℓ.

theorem Cslib.ofCoeffList_truncZJet (J : ℕ) (u : List ℤ) : Polynomial.ofCoeffList (truncZJet J u) = Polynomial.ofCoeffList (List.take J u)

truncZJet J u represents u.take J under Polynomial.ofCoeffList.

theorem Cslib.coeff_eq_below_mul {P₁ P₂ Q₁ Q₂ : Polynomial ℤ} {J : ℕ} (h1 : ∀ i < J, P₁.coeff i = Q₁.coeff i) (h2 : ∀ i < J, P₂.coeff i = Q₂.coeff i) (j : ℕ) : j < J → (P₁ * P₂).coeff j = (Q₁ * Q₂).coeff j

Polynomial multiplication preserves coefficient equality below degree J.

theorem Cslib.getD_powZJet_of_lt {J j : ℕ} (hj : j < J) (u : List ℤ) (s : ℕ) : (powZJet J u s).getD j 0 = (Polynomial.ofCoeffList (List.take J u) ^ s).coeff j

Coefficient specification of powZJet on degree-$< J$ prefixes.

theorem Cslib.evalParityFactorJet_entry_eq_coeff {J ℓ j s : ℕ} (hj : j < J) (hs : s < ℓ) (Δ : ℤ) (yJet : List ℤ) : rowEntry (evalParityFactorJet J ℓ Δ yJet) j s = have ab := (parityLinearCoeffs ℓ).getD s (0, 0); have Y := Polynomial.ofCoeffList (List.take J yJet); (Polynomial.C (Δ ^ (2 * (ℓ - 1 - s))) * ((Polynomial.C (Δ * ab.1) + Polynomial.C ab.2 * Y) * (Y * (Y - Polynomial.C Δ)) ^ s)).coeff j

Polynomial-in-$z$ specification of evalParityFactorJet modulo $z^J$.

theorem Cslib.evalParityFactorJet_entry_eq_parityFactorCleared {J j : ℕ} (hj : j < J) (ℓ s : ℕ) (Δ : ℤ) (yJet : List ℤ) : rowEntry (evalParityFactorJet J ℓ Δ yJet) j s = ((BitString.parityFactorCleared ℓ (Polynomial.C Δ) (Polynomial.ofCoeffList (List.take J yJet))).coeff s).coeff j

Stage-2 to Stage-3 bridge ([OAI26c], §5.4 and Appendix B.2): for every $j < J$ and all $\ell, s \in \mathbb{N}$, entry $(j, s)$ of evalParityFactorJet J ℓ Δ yJet equals the $z^j$ coefficient of the $V^s$ coefficient of Cslib.BitString.parityFactorCleared.

theorem Cslib.evalParityFactorJet_entry_cast_rat {J ℓ j s : ℕ} (hℓ : 1 ≤ ℓ) (hj : j < J) (hs : s < ℓ) {Δ : ℤ} (hΔ : Δ ≠ 0) (yJet : List ℤ) : have ab := (parityLinearCoeffs ℓ).getD s (0, 0); have YQ := Polynomial.C (↑Δ)⁻¹ * Polynomial.map (Int.castRingHom ℚ) (Polynomial.ofCoeffList (List.take J yJet)); ↑(rowEntry (evalParityFactorJet J ℓ Δ yJet) j s) = (Polynomial.C (↑Δ ^ (2 * ℓ - 1)) * ((Polynomial.C ↑ab.1 + Polynomial.C ↑ab.2 * YQ) * (YQ * (YQ - 1)) ^ s)).coeff j

Rational $z$-jet homogenization identity ([OAI26c], Appendix B.2) for $\Delta \ne 0$ and $Y_{\mathbb{Q}}(z) = \Delta^{-1} \widetilde{Y}(z) \in \mathbb{Q}[X]$.

theorem Cslib.evalParityFactorJet_row_sum_cast_rat {J ℓ j : ℕ} (hℓ : 1 ≤ ℓ) (hj : j < J) {Δ : ℤ} (hΔ : Δ ≠ 0) (yJet : List ℤ) : have YQ := Polynomial.C (↑Δ)⁻¹ * Polynomial.map (Int.castRingHom ℚ) (Polynomial.ofCoeffList (List.take J yJet)); ↑((evalParityFactorJet J ℓ Δ yJet).getD j []).sum = (Polynomial.C (↑Δ ^ (2 * ℓ - 1)) * (Polynomial.map (Int.castRingHom ℚ) (Polynomial.ofCoeffList (parityPolyCoeffs ℓ))).comp YQ).coeff j

Summing row $j < J$ of evalParityFactorJet ($V = 1$) gives the $z^j$ coefficient of $\Delta^{2 \ell - 1} p_\ell(Y_{\mathbb{Q}}(z))$ over $\mathbb{Q}[X]$.

theorem Cslib.evalParityFactorJet_row_zero_entry {J ℓ s : ℕ} (hJ : 1 ≤ J) (hs : s < ℓ) (Δ y : ℤ) {yJet : List ℤ} (hy0 : yJet.getD 0 0 = Δ * y) : have ab := (parityLinearCoeffs ℓ).getD s (0, 0); rowEntry (evalParityFactorJet J ℓ Δ yJet) 0 s = Δ ^ (2 * ℓ - 1) * ((ab.1 + ab.2 * y) * (y * (y - 1)) ^ s)

Constant-in-$z$ ($j = 0$) integer specialization when $\text{yJet}[0] = \Delta y$.

theorem Cslib.evalParityFactorJet_row_zero_sum {J ℓ : ℕ} (hJ : 1 ≤ J) (Δ y : ℤ) {yJet : List ℤ} (hy0 : yJet.getD 0 0 = Δ * y) : ((evalParityFactorJet J ℓ Δ yJet).getD 0 []).sum = Δ ^ (2 * ℓ - 1) * evalParityAmplifier ℓ y

Summing row $0$ when $\text{yJet}[0] = \Delta y$ gives $\Delta^{2 \ell - 1} p_\ell(y)$.

Prefix $\ell_1$-norm and bit-length bounds for evalParityFactorJet (Appendix B.2)

theorem Cslib.polyNorm1_truncZJet (J : ℕ) (u : List ℤ) : polyNorm1 (truncZJet J u) = polyNorm1 (List.take J u)

truncZJet preserves the prefix $\ell_1$-norm.

theorem Cslib.polyNorm1_powZJet_le (J : ℕ) (u : List ℤ) (s : ℕ) : polyNorm1 (powZJet J u s) ≤ polyNorm1 (List.take J u) ^ s

Powering bound for powZJet under polyNorm1.

theorem Cslib.jetL1Norm_evalParityFactorJet_le (J ℓ : ℕ) (Δ : ℤ) (yJet : List ℤ) : jetL1Norm (evalParityFactorJet J ℓ Δ yJet) ≤ ℓ * 2 ^ (7 * ℓ ^ 2) * (polyNorm1 (List.take J yJet) + Δ.natAbs + 2) ^ (2 * ℓ - 1)

Total factor-table $\ell_1$-norm bound ([OAI26c], Appendix B.2, bound $B_1$).

theorem Cslib.natAbs_row_take_sum_evalParityFactorJet_le {J ℓ : ℕ} {Δ : ℤ} {yJet r : List ℤ} (hr : r ∈ evalParityFactorJet J ℓ Δ yJet) (m : ℕ) : (List.take m r).sum.natAbs ≤ ℓ * 2 ^ (7 * ℓ ^ 2) * (polyNorm1 (List.take J yJet) + Δ.natAbs + 2) ^ (2 * ℓ - 1)

Prefix-sum magnitude bound for every row of evalParityFactorJet ([OAI26c], Appendix B.2).

theorem Cslib.length_encIntBin_evalParityFactorJet_le {J ℓ : ℕ} {Δ : ℤ} {yJet r : List ℤ} (hr : r ∈ evalParityFactorJet J ℓ Δ yJet) (m : ℕ) : (Turing.MultiTapeTM.encIntBin (List.take m r).sum).length ≤ 8 * ℓ ^ 2 + 2 * ℓ * (polyNorm1 (List.take J yJet) + Δ.natAbs + 2).size + 2 ∧ ∀ z ∈ r, (Turing.MultiTapeTM.encIntBin z).length ≤ 8 * ℓ ^ 2 + 2 * ℓ * (polyNorm1 (List.take J yJet) + Δ.natAbs + 2).size + 2

Entry and row-prefix bit-length bound ([OAI26c], Appendix B.2): every entry and row prefix sum uses $O(\ell^2 + \ell \log(\|\widetilde{y}\|_1 + |\Delta| + 2))$ bits under encIntBin.

Plain polynomial-time certificates (ComputableInPolyTime)

theorem Cslib.intBin_pow_polytime {α : Type} {encIn : α ↪ List Bool} {base : α → ℤ} {exp : α → ℕ} (hb : Turing.MultiTapeTM.ComputableInPolyTime base encIn Turing.MultiTapeTM.encIntBin) (he : Turing.MultiTapeTM.ComputableInPolyTime exp encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => base x ^ exp x) encIn Turing.MultiTapeTM.encIntBin

theorem Cslib.polyNorm1_le_two_pow_encList (l : List ℤ) : polyNorm1 l ≤ 2 ^ (2 * ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) l).length)

polyNorm1 l is bounded exponentially in (encList encIntBin l).length.

theorem Cslib.computableInPolyTime_polyAdd {α : Type} {encIn : α ↪ List Bool} {p q : α → List ℤ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hq : Turing.MultiTapeTM.ComputableInPolyTime q encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => polyAdd (p x) (q x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Polynomial-time certificate for polyAdd.

theorem Cslib.computableInPolyTime_cauchyCoeff {α : Type} {encIn : α ↪ List Bool} {p q : α → List ℤ} {k : α → ℕ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hq : Turing.MultiTapeTM.ComputableInPolyTime q encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hk : Turing.MultiTapeTM.ComputableInPolyTime k encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => cauchyCoeff (p x) (q x) (k x)) encIn Turing.MultiTapeTM.encIntBin

Polynomial-time certificate for cauchyCoeff.

theorem Cslib.computableInPolyTime_mulZJet {α : Type} {encIn : α ↪ List Bool} {J : α → ℕ} {u v : α → List ℤ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => mulZJet (J x) (u x) (v x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Compositional plain polynomial-time certificate for mulZJet.

theorem Cslib.computableInPolyTime_polyMul {α : Type} {encIn : α ↪ List Bool} {p q : α → List ℤ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hq : Turing.MultiTapeTM.ComputableInPolyTime q encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => polyMul (p x) (q x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Polynomial-time certificate for polyMul.

theorem Cslib.computableInPolyTime_divModByH {α : Type} {encIn : α ↪ List Bool} {p : α → List ℤ} (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => divModByH (p x)) encIn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin Turing.MultiTapeTM.encIntBin))

Polynomial-time certificate for monic division by $Y^2 - Y$ (divModByH).

theorem Cslib.computableInPolyTime_parityPolyCoeffs {α : Type} {encIn : α ↪ List Bool} {ℓ : α → ℕ} (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => parityPolyCoeffs (ℓ x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Polynomial-time certificate for parityPolyCoeffs.

theorem Cslib.computableInPolyTime_parityLinearCoeffs {α : Type} {encIn : α ↪ List Bool} {ℓ : α → ℕ} (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => parityLinearCoeffs (ℓ x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin Turing.MultiTapeTM.encIntBin))

Compositional plain polynomial-time certificate for parityLinearCoeffs.

theorem Cslib.parityLinearCoeffs_polytime : Turing.MultiTapeTM.ComputableInPolyTime parityLinearCoeffs Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin Turing.MultiTapeTM.encIntBin))

Standalone plain polynomial-time certificate for parityLinearCoeffs on unary $\ell$.

theorem Cslib.computableInPolyTime_truncZJet {α : Type} {encIn : α ↪ List Bool} {J : α → ℕ} {u : α → List ℤ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => truncZJet (J x) (u x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Compositional polynomial-time certificate for truncZJet.

theorem Cslib.computableInPolyTime_powZJet {α : Type} {encIn : α ↪ List Bool} {J s : α → ℕ} {u : α → List ℤ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hs : Turing.MultiTapeTM.ComputableInPolyTime s encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => powZJet (J x) (u x) (s x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Compositional plain polynomial-time certificate for powZJet.

theorem Cslib.singleton_intBin_polytime {α : Type} {encIn : α ↪ List Bool} {z : α → ℤ} (hz : Turing.MultiTapeTM.ComputableInPolyTime z encIn Turing.MultiTapeTM.encIntBin) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => [z x]) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Wrapping a binary integer into a singleton list is polynomial-time.

theorem Cslib.computableInPolyTime_evalParityFactorJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {Δ : α → ℤ} {yJet : α → List ℤ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hΔ : Turing.MultiTapeTM.ComputableInPolyTime Δ encIn Turing.MultiTapeTM.encIntBin) (hyJet : Turing.MultiTapeTM.ComputableInPolyTime yJet encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => evalParityFactorJet (J x) (ℓ x) (Δ x) (yJet x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Compositional plain polynomial-time certificate for evalParityFactorJet ([OAI26c], Appendix B.2) on unary $(J, \ell)$ and binary $(\Delta, \text{yJet})$.

theorem Cslib.evalParityFactorJet_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × ℤ × List ℤ) => evalParityFactorJet p.1.1 p.1.2 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Standalone plain polynomial-time certificate for evalParityFactorJet on unary $(J, \ell)$ and binary $(\Delta, \text{yJet})$.