Stage-1 sparse monomial $z$-jet substitution and node-$t$ Taylor shift

Section 3.4, Sections 5.3–5.4, and Appendix B.2 of OpenAI, The Exponential Time Hypothesis is False evaluate each degree-$\le k$ sparse $\mathbb{F}_2$ equation at a node $t \in \mathbb{Z}$ in $\mathbb{Z}[z]/(z^J)$ by:

1. Horner Taylor-shifting univariate integer polynomials around $t$ modulo $z^J$ (Cslib.taylorShiftZJet, using step helper Cslib.SparseMonomialJet.hornerShiftStep);
2. assembling each factor variable's homogenized affine-Taylor input $z$-jet $d_{\mathrm{den}} \theta_{f,v}(z; x) = \langle d_{\mathrm{den}} \vec{P}_{f,v}(t), x \rangle + \langle d_{\mathrm{den}}(\vec{P}_{f,v}(t + z) - \vec{P}_{f,v}(t)), \mathbf{1}_U \rangle \bmod z^J$ (Cslib.combineAffineInputZJet, Cslib.evalBaselineAt, Cslib.evalTaylorCorrectionZJet, Cslib.evalAffineInputZJet, Cslib.evalAffineInputZJetTable), bridged to Cslib.AffineTaylor.affineInput;
3. multiplying variable $z$-jets across canonical monomials (via helper Cslib.SparseMonomialJet.prodMonomialJet) with scale $d_{\mathrm{den}}^{k - |M|}$ and summing across sparse equations (Cslib.evalClearedMonomialJet, Cslib.evalClearedEquationJet), bridged to Cslib.BitString.clearedMonomialPoly, Cslib.BitString.clearedMonomialSumPoly, and Cslib.Complexity.evalMonomialList; and
4. composing with Cslib.evalParityFactorJet at $\Delta = d_{\mathrm{den}}^k$ (Cslib.evalEquationParityFactorJet) for the homogenized $J \times \ell$ factor table matching Cslib.BitString.parityFactorCleared ($\Gamma = \Delta^{2 \ell - 1}$ when $d_{\mathrm{den}} \ne 0$), with @[fun_prop] ComputableInPolyTime certificates on all nine top-level routines.

References

• OpenAI, The Exponential Time Hypothesis is False

1. Univariate integer polynomial Taylor shift modulo $z^J$ (taylorShiftZJet)

def Cslib.SparseMonomialJet.hornerShiftStep (J : ℕ) (t : ℤ) (acc : List ℤ) (c : ℤ) : List ℤ

Single Horner Taylor-shift step mapping acc to (c + (t + z) * acc) mod z^J.

def Cslib.taylorShiftZJet (J : ℕ) (t : ℤ) (coeffs : List ℤ) : List ℤ

Executable univariate integer Taylor shift at node $t \in \mathbb{Z}$ truncated modulo $z^J$ ([OAI26c], §3.4 and Appendix B.2), computing the low-$J$ coefficients of Polynomial.taylor t (Polynomial.ofCoeffList coeffs).

@[simp]

theorem Cslib.length_taylorShiftZJet (J : ℕ) (t : ℤ) (coeffs : List ℤ) : (taylorShiftZJet J t coeffs).length = J

taylorShiftZJet J t coeffs has exact length J.

theorem Cslib.getD_taylorShiftZJet_of_lt {J j : ℕ} (hj : j < J) (t : ℤ) (coeffs : List ℤ) : (taylorShiftZJet J t coeffs).getD j 0 = ((Polynomial.taylor t) (Polynomial.ofCoeffList coeffs)).coeff j

Entry j < J of taylorShiftZJet J t coeffs equals (Polynomial.taylor t (Polynomial.ofCoeffList coeffs)).coeff j.

theorem Cslib.taylorShiftZJet_eq_coeffsBelow (J : ℕ) (t : ℤ) (coeffs : List ℤ) : taylorShiftZJet J t coeffs = ((Polynomial.taylor t) (Polynomial.ofCoeffList coeffs)).coeffsBelow J

taylorShiftZJet agrees with Polynomial.coeffsBelow J of Polynomial.taylor t.

theorem Cslib.natDegree_ofCoeffList_taylorShiftZJet_le (J : ℕ) (t : ℤ) (coeffs : List ℤ) : (Polynomial.ofCoeffList (taylorShiftZJet J t coeffs)).natDegree ≤ J - 1

The polynomial represented by taylorShiftZJet J t coeffs has degree at most J - 1.

theorem Cslib.X_pow_dvd_taylor_sub_ofCoeffList_taylorShiftZJet (J : ℕ) (t : ℤ) (coeffs : List ℤ) : Polynomial.X ^ J ∣ (Polynomial.taylor t) (Polynomial.ofCoeffList coeffs) - Polynomial.ofCoeffList (taylorShiftZJet J t coeffs)

Congruence of ofCoeffList (taylorShiftZJet J t coeffs) modulo $X^J$.

theorem Cslib.ofCoeffList_taylorShiftZJet_eq_taylor {J : ℕ} (t : ℤ) {coeffs : List ℤ} (hdeg : (Polynomial.ofCoeffList coeffs).natDegree < J) : Polynomial.ofCoeffList (taylorShiftZJet J t coeffs) = (Polynomial.taylor t) (Polynomial.ofCoeffList coeffs)

Exact recovery of Polynomial.taylor t when (ofCoeffList coeffs).natDegree < J.

theorem Cslib.polyNorm1_taylorShiftZJet_le (J : ℕ) (t : ℤ) (coeffs : List ℤ) : polyNorm1 (taylorShiftZJet J t coeffs) ≤ polyNorm1 coeffs * (t.natAbs + 1) ^ coeffs.length

Horner $\ell_1$-norm bound for taylorShiftZJet.

theorem Cslib.length_encIntBin_mem_taylorShiftZJet_le {J : ℕ} {t : ℤ} {coeffs : List ℤ} {z : ℤ} (hz : z ∈ taylorShiftZJet J t coeffs) : (Turing.MultiTapeTM.encIntBin z).length ≤ (polyNorm1 coeffs).size + coeffs.length * (t.natAbs + 1).size + 2

Entry bit-length bound for taylorShiftZJet under encIntBin.

2. Affine-Taylor variable $z$-jet evaluation (evalAffineInputZJet)

def Cslib.combineAffineInputZJet (J : ℕ) (base : ℤ) (corrJet : List ℤ) : List ℤ

Assembles a length-J 1D $z$-jet from base ($j = 0$) and corrJet ($1 \le j < J$).

def Cslib.evalBaselineAt (t : ℤ) (rowCoeffs : List (List ℤ)) (x : List Bool) : ℤ

Evaluates the scalar baseline $\langle d_{\mathrm{den}} \vec{P}_{f,v}(t), x \rangle$ at t ([OAI26c], §3.4 eq. (3.7) and Appendix B.2; missing x bits default to false).

def Cslib.evalTaylorCorrectionZJet (J : ℕ) (t : ℤ) (rowCoeffs : List (List ℤ)) (U : List Bool) : List ℤ

Evaluates the length-J zero-constant Taylor-correction $z$-jet $\langle d_{\mathrm{den}}(\vec{P}_{f,v}(t + z) - \vec{P}_{f,v}(t)), \mathbf{1}_U \rangle \bmod z^J$ ([OAI26c], §3.4 eq. (3.7) and Appendix B.2; missing U bits default to false).

def Cslib.evalAffineInputZJet (J : ℕ) (t : ℤ) (rowCoeffs : List (List ℤ)) (U x : List Bool) : List ℤ

Evaluates the length-J homogenized affine-Taylor input $z$-jet $d_{\mathrm{den}} \theta_{f,v}$ ([OAI26c], §3.4 eq. (3.7) and Appendix B.2).

def Cslib.evalAffineInputZJetTable (J : ℕ) (t : ℤ) (rowsCoeffs : List (List (List ℤ))) (U x : List Bool) : List (List ℤ)

Materialized rowsCoeffs.length × J table of homogenized affine-Taylor variable $z$-jets.

@[simp]

theorem Cslib.length_combineAffineInputZJet (J : ℕ) (base : ℤ) (corrJet : List ℤ) : (combineAffineInputZJet J base corrJet).length = J

combineAffineInputZJet J base corrJet has exact length J.

theorem Cslib.getD_combineAffineInputZJet_of_lt {J j : ℕ} (hj : j < J) (base : ℤ) (corrJet : List ℤ) : (combineAffineInputZJet J base corrJet).getD j 0 = if j = 0 then base else corrJet.getD j 0

Entry j < J of combineAffineInputZJet is base at 0 and corrJet.getD j 0 for j > 0.

theorem Cslib.evalBaselineAt_eq_sum (t : ℤ) (rowCoeffs : List (List ℤ)) (x : List Bool) : evalBaselineAt t rowCoeffs x = ∑ i : Fin rowCoeffs.length, Polynomial.eval t (Polynomial.ofCoeffList (rowCoeffs.getD ↑i [])) * BitString.bitVal ℤ (x.getD (↑i) false)

evalBaselineAt t rowCoeffs x equals the polynomial baseline sum at t.

theorem Cslib.evalBaselineAt_zero (rowCoeffs : List (List ℤ)) (x : List Bool) : evalBaselineAt 0 rowCoeffs x = ∑ i : Fin rowCoeffs.length, rowEntry rowCoeffs (↑i) 0 * BitString.bitVal ℤ (x.getD (↑i) false)

At t = 0, evalBaselineAt 0 rowCoeffs x sums the constant entries selected by x.

@[simp]

theorem Cslib.length_evalTaylorCorrectionZJet (J : ℕ) (t : ℤ) (rowCoeffs : List (List ℤ)) (U : List Bool) : (evalTaylorCorrectionZJet J t rowCoeffs U).length = J

evalTaylorCorrectionZJet has exact length J.

theorem Cslib.getD_evalTaylorCorrectionZJet_of_lt {J j : ℕ} (hj : j < J) (t : ℤ) (rowCoeffs : List (List ℤ)) (U : List Bool) : (evalTaylorCorrectionZJet J t rowCoeffs U).getD j 0 = if j = 0 then 0 else ∑ i : Fin rowCoeffs.length, BitString.bitVal ℤ (U.getD (↑i) false) * ((Polynomial.taylor t) (Polynomial.ofCoeffList (rowCoeffs.getD ↑i []))).coeff j

Entrywise specification of evalTaylorCorrectionZJet for j < J.

@[simp]

theorem Cslib.length_evalAffineInputZJet (J : ℕ) (t : ℤ) (rowCoeffs : List (List ℤ)) (U x : List Bool) : (evalAffineInputZJet J t rowCoeffs U x).length = J

evalAffineInputZJet returns a $z$-jet of exact length J.

@[simp]

theorem Cslib.length_evalAffineInputZJetTable (J : ℕ) (t : ℤ) (rowsCoeffs : List (List (List ℤ))) (U x : List Bool) : (evalAffineInputZJetTable J t rowsCoeffs U x).length = rowsCoeffs.length

evalAffineInputZJetTable has length rowsCoeffs.length.

theorem Cslib.isTableShape_evalAffineInputZJetTable (J : ℕ) (t : ℤ) (rowsCoeffs : List (List (List ℤ))) (U x : List Bool) : IsTableShape rowsCoeffs.length J (evalAffineInputZJetTable J t rowsCoeffs U x)

evalAffineInputZJetTable has rectangular shape rowsCoeffs.length × J.

theorem Cslib.truncZJet_getD_evalAffineInputZJetTable (J : ℕ) (t : ℤ) (rowsCoeffs : List (List (List ℤ))) (U x : List Bool) (v : ℕ) : truncZJet J ((evalAffineInputZJetTable J t rowsCoeffs U x).getD v []) = evalAffineInputZJet J t (rowsCoeffs.getD v []) U x

Truncating row v of evalAffineInputZJetTable to length J agrees with evalAffineInputZJet J t (rowsCoeffs.getD v []) U x at every v : ℕ.

theorem Cslib.rowEntry_evalAffineInputZJetTable_of_lt {J j : ℕ} (hj : j < J) (t : ℤ) (rowsCoeffs : List (List (List ℤ))) (U x : List Bool) (v : ℕ) : rowEntry (evalAffineInputZJetTable J t rowsCoeffs U x) v j = (evalAffineInputZJet J t (rowsCoeffs.getD v []) U x).getD j 0

Entry (v, j) (j < J) of evalAffineInputZJetTable agrees with evalAffineInputZJet.

theorem Cslib.evalAffineInputZJetTable_eq_tabulateTable (J : ℕ) (t : ℤ) (rowsCoeffs : List (List (List ℤ))) (U x : List Bool) : evalAffineInputZJetTable J t rowsCoeffs U x = tabulateTable rowsCoeffs.length J fun (v j : ℕ) => (evalAffineInputZJet J t (rowsCoeffs.getD v []) U x).getD j 0

evalAffineInputZJetTable agrees with Cslib.tabulateTable on rowsCoeffs.length × J.

theorem Cslib.getD_evalAffineInputZJet_eq_coeff_affineInput_fin {J n j : ℕ} (hj : j < J) (t : ℤ) {rowCoeffs : List (List ℤ)} (hlen : rowCoeffs.length ≤ n) (U x : List Bool) : (evalAffineInputZJet J t rowCoeffs U x).getD j 0 = (Polynomial.map (MvPolynomial.eval fun (i : Fin n) => BitString.bitVal ℤ (U.getD (↑i) false)) (AffineTaylor.affineInput (fun (i : Fin n) => Polynomial.ofCoeffList (rowCoeffs.getD ↑i [])) t fun (i : Fin n) => x.getD (↑i) false)).coeff j

Refinement of evalAffineInputZJet to Cslib.AffineTaylor.affineInput over Fin n ([OAI26c], §3.4 eq. (3.7) and Appendix B.2) for rowCoeffs.length ≤ n and j < J.

theorem Cslib.getD_evalAffineInputZJet_eq_coeff_affineInput {J j : ℕ} (hj : j < J) (t : ℤ) (rowCoeffs : List (List ℤ)) (U x : List Bool) : (evalAffineInputZJet J t rowCoeffs U x).getD j 0 = (Polynomial.map (MvPolynomial.eval fun (i : Fin rowCoeffs.length) => BitString.bitVal ℤ (U.getD (↑i) false)) (AffineTaylor.affineInput (fun (i : Fin rowCoeffs.length) => Polynomial.ofCoeffList (rowCoeffs.getD ↑i [])) t fun (i : Fin rowCoeffs.length) => x.getD (↑i) false)).coeff j

Entrywise specification of evalAffineInputZJet against Cslib.AffineTaylor.affineInput over Fin rowCoeffs.length for j < J.

theorem Cslib.rowEntry_evalAffineInputZJetTable_eq_coeff_affineInput {J n j : ℕ} (hj : j < J) (t : ℤ) {rowsCoeffs : List (List (List ℤ))} (hrows : ∀ r ∈ rowsCoeffs, r.length ≤ n) (U x : List Bool) (v : ℕ) : rowEntry (evalAffineInputZJetTable J t rowsCoeffs U x) v j = (Polynomial.map (MvPolynomial.eval fun (i : Fin n) => BitString.bitVal ℤ (U.getD (↑i) false)) (AffineTaylor.affineInput (fun (i : Fin n) => Polynomial.ofCoeffList ((rowsCoeffs.getD v []).getD ↑i [])) t fun (i : Fin n) => x.getD (↑i) false)).coeff j

Table entry specification of evalAffineInputZJetTable against Cslib.AffineTaylor.affineInput over Fin n (∀ r ∈ rowsCoeffs, r.length ≤ n) for j < J.

theorem Cslib.getD_zero_evalAffineInputZJet {J : ℕ} (hJ : 1 ≤ J) (t : ℤ) (rowCoeffs : List (List ℤ)) (U x : List Bool) : (evalAffineInputZJet J t rowCoeffs U x).getD 0 0 = evalBaselineAt t rowCoeffs x

At j = 0 (1 ≤ J), evalAffineInputZJet evaluates to evalBaselineAt t rowCoeffs x.

theorem Cslib.getD_zero_evalAffineInputZJet_zero {J : ℕ} (hJ : 1 ≤ J) (rowCoeffs : List (List ℤ)) (U x : List Bool) : (evalAffineInputZJet J 0 rowCoeffs U x).getD 0 0 = ∑ i : Fin rowCoeffs.length, rowEntry rowCoeffs (↑i) 0 * BitString.bitVal ℤ (x.getD (↑i) false)

At t = 0 and j = 0 (1 ≤ J), evalAffineInputZJet J 0 rowCoeffs U x sums the constant entries selected by x.

theorem Cslib.getD_zero_evalAffineInputZJet_of_unit_row {J w : ℕ} (hJ : 1 ≤ J) (dDen : ℤ) {rowCoeffs : List (List ℤ)} (hw : w < rowCoeffs.length) (hunit : ∀ u < rowCoeffs.length, rowEntry rowCoeffs u 0 = if u = w then dDen else 0) (U x : List Bool) : (evalAffineInputZJet J 0 rowCoeffs U x).getD 0 0 = dDen * BitString.bitVal ℤ (x.getD w false)

At t = 0, j = 0 (1 ≤ J), a unit row restoring coordinate w at scale dDen evaluates to dDen * bitVal ℤ (x.getD w false) regardless of U.

theorem Cslib.polyNorm1_evalAffineInputZJet_le_sum_taylorShiftZJet (J : ℕ) (t : ℤ) (rowCoeffs : List (List ℤ)) (U x : List Bool) : polyNorm1 (evalAffineInputZJet J t rowCoeffs U x) ≤ (List.map (fun (c : List ℤ) => polyNorm1 (taylorShiftZJet J t c)) rowCoeffs).sum

Coordinatewise shifted-norm bound for evalAffineInputZJet.

theorem Cslib.polyNorm1_evalAffineInputZJet_le (J : ℕ) (t : ℤ) (rowCoeffs : List (List ℤ)) (U x : List Bool) : polyNorm1 (evalAffineInputZJet J t rowCoeffs U x) ≤ (List.map (fun (c : List ℤ) => polyNorm1 c * (t.natAbs + 1) ^ c.length) rowCoeffs).sum

Appendix B.2 $B_0$-style $\ell_1$-norm bound for evalAffineInputZJet ([OAI26c], Appendix B.2, p. 48) via polyNorm1_taylorShiftZJet_le.

theorem Cslib.polyNorm1_evalTaylorCorrectionZJet_le (J : ℕ) (t : ℤ) (rowCoeffs : List (List ℤ)) (U : List Bool) : polyNorm1 (evalTaylorCorrectionZJet J t rowCoeffs U) ≤ (List.map (fun (c : List ℤ) => polyNorm1 c * (t.natAbs + 1) ^ c.length) rowCoeffs).sum

Appendix B.2 $\ell_1$-norm bound for evalTaylorCorrectionZJet.

theorem Cslib.polyNorm1_truncZJet_mem_evalAffineInputZJetTable_le {J B₀ : ℕ} {t : ℤ} {rowsCoeffs : List (List (List ℤ))} (hrows : ∀ rowCoeffs ∈ rowsCoeffs, (List.map (fun (c : List ℤ) => polyNorm1 c * (t.natAbs + 1) ^ c.length) rowCoeffs).sum ≤ B₀) (U x : List Bool) {q : List ℤ} (hq : q ∈ evalAffineInputZJetTable J t rowsCoeffs U x) : polyNorm1 (truncZJet J q) ≤ B₀ ∧ polyNorm1 q ≤ B₀

Every row q ∈ evalAffineInputZJetTable J t rowsCoeffs U x satisfies polyNorm1 (truncZJet J q) ≤ B₀ and polyNorm1 q ≤ B₀ under rowwise Horner bound B₀.

3. Stage-1 homogenized monomial & equation $z$-jet evaluation

def Cslib.SparseMonomialJet.prodMonomialJet (J : ℕ) (varJets : List (List ℤ)) (mon : List ℕ) : List ℤ

Product of truncated variable $z$-jets across mon modulo $z^J$.

def Cslib.evalClearedMonomialJet (J k : ℕ) (dDen : ℤ) (varJets : List (List ℤ)) (mon : List ℕ) : List ℤ

Stage-1 degree-$k$ homogenized monomial $z$-jet evaluation ([OAI26c], §5.3–5.4 and Appendix B.2), computing $d_{\mathrm{den}}^{k - |\text{mon}|} \prod_{v \in \text{mon}} \theta_v(z) \bmod z^J$ (missing varJets rows default to []; k < mon.length uses k - mon.length = 0).

def Cslib.evalClearedEquationJet (J k : ℕ) (dDen : ℤ) (varJets : List (List ℤ)) (eq : List (List ℕ)) : List ℤ

Stage-1 degree-$k$ homogenized sparse equation $z$-jet evaluation ([OAI26c], §5.3–5.4 and Appendix B.2), summing evalClearedMonomialJet across mon ∈ eq modulo $z^J$.

@[simp]

theorem Cslib.length_evalClearedMonomialJet (J k : ℕ) (dDen : ℤ) (varJets : List (List ℤ)) (mon : List ℕ) : (evalClearedMonomialJet J k dDen varJets mon).length = J

evalClearedMonomialJet has exact length J.

@[simp]

theorem Cslib.length_evalClearedEquationJet (J k : ℕ) (dDen : ℤ) (varJets : List (List ℤ)) (eq : List (List ℕ)) : (evalClearedEquationJet J k dDen varJets eq).length = J

evalClearedEquationJet has exact length J.

theorem Cslib.getD_evalClearedMonomialJet_of_lt {J k j : ℕ} (hj : j < J) (dDen : ℤ) {varJets : List (List ℤ)} {θ : ℕ → Polynomial ℤ} {mon : List ℕ} (hmon : Complexity.IsCanonicalMonomial mon) (_hdeg : mon.length ≤ k) (hθ : ∀ v ∈ mon, ∀ i < J, rowEntry varJets v i = (θ v).coeff i) : (evalClearedMonomialJet J k dDen varJets mon).getD j 0 = (BitString.clearedMonomialPoly dDen k θ mon.toFinset).coeff j

Coefficient specification of evalClearedMonomialJet against Cslib.BitString.clearedMonomialPoly for j < J.

theorem Cslib.getD_evalClearedEquationJet_of_lt {J k j : ℕ} (hj : j < J) (dDen : ℤ) {varJets : List (List ℤ)} {θ : ℕ → Polynomial ℤ} {eq : List (List ℕ)} (heq : Complexity.IsCanonicalEquation eq) (hdeg : ∀ mon ∈ eq, mon.length ≤ k) (hθ : ∀ mon ∈ eq, ∀ v ∈ mon, ∀ i < J, rowEntry varJets v i = (θ v).coeff i) : (evalClearedEquationJet J k dDen varJets eq).getD j 0 = (BitString.clearedMonomialSumPoly dDen k θ (List.map List.toFinset eq).toFinset).coeff j

Coefficient specification of evalClearedEquationJet against Cslib.BitString.clearedMonomialSumPoly for j < J.

theorem Cslib.taylor_clearedMonomialPoly (t dDen : ℤ) (k : ℕ) (θ₀ : ℕ → Polynomial ℤ) (M : Finset ℕ) : (Polynomial.taylor t) (BitString.clearedMonomialPoly dDen k θ₀ M) = BitString.clearedMonomialPoly dDen k (fun (v : ℕ) => (Polynomial.taylor t) (θ₀ v)) M

Polynomial.taylor t commutes with clearedMonomialPoly.

theorem Cslib.taylor_clearedMonomialSumPoly (t dDen : ℤ) (k : ℕ) (θ₀ : ℕ → Polynomial ℤ) (𝓜 : Finset (Finset ℕ)) : (Polynomial.taylor t) (BitString.clearedMonomialSumPoly dDen k θ₀ 𝓜) = BitString.clearedMonomialSumPoly dDen k (fun (v : ℕ) => (Polynomial.taylor t) (θ₀ v)) 𝓜

Polynomial.taylor t commutes with clearedMonomialSumPoly.

theorem Cslib.getD_evalClearedEquationJet_eq_taylor_coeff {J k j : ℕ} (hj : j < J) (t dDen : ℤ) {varJets : List (List ℤ)} {θ₀ : ℕ → Polynomial ℤ} {eq : List (List ℕ)} (heq : Complexity.IsCanonicalEquation eq) (hdeg : ∀ mon ∈ eq, mon.length ≤ k) (hθ : ∀ mon ∈ eq, ∀ v ∈ mon, ∀ i < J, rowEntry varJets v i = ((Polynomial.taylor t) (θ₀ v)).coeff i) : (evalClearedEquationJet J k dDen varJets eq).getD j 0 = ((Polynomial.taylor t) (BitString.clearedMonomialSumPoly dDen k θ₀ (List.map List.toFinset eq).toFinset)).coeff j

Node-$t$ Taylor-shift specialization of evalClearedEquationJet for j < J.

theorem Cslib.getD_zero_evalClearedMonomialJet {J k : ℕ} (hJ : 1 ≤ J) (dDen : ℤ) {varJets : List (List ℤ)} {mon : List ℕ} (hmon : Complexity.IsCanonicalMonomial mon) (hdeg : mon.length ≤ k) (x : ℕ → Bool) (hx : ∀ v ∈ mon, rowEntry varJets v 0 = dDen * BitString.bitVal ℤ (x v)) : (evalClearedMonomialJet J k dDen varJets mon).getD 0 0 = dDen ^ k * BitString.monomial ℤ mon.toFinset x

At j = 0 (1 ≤ J), evalClearedMonomialJet evaluates to dDen ^ k * monomial ℤ ... x.

theorem Cslib.getD_zero_evalClearedEquationJet {J k : ℕ} (hJ : 1 ≤ J) (dDen : ℤ) {varJets : List (List ℤ)} {eq : List (List ℕ)} (heq : Complexity.IsCanonicalEquation eq) (hdeg : ∀ mon ∈ eq, mon.length ≤ k) (x : ℕ → Bool) (hx : ∀ mon ∈ eq, ∀ v ∈ mon, rowEntry varJets v 0 = dDen * BitString.bitVal ℤ (x v)) : (evalClearedEquationJet J k dDen varJets eq).getD 0 0 = dDen ^ k * BitString.monomialSum ℤ (List.map List.toFinset eq).toFinset x

At j = 0 (1 ≤ J), evalClearedEquationJet gives dDen ^ k * monomialSum ℤ ... x.

theorem Cslib.even_monomialSum_toFinset_iff_evalMonomialList_eq_false {eq : List (List ℕ)} (heq : Complexity.IsCanonicalEquation eq) (x : ℕ → Bool) : Even (BitString.monomialSum ℤ (List.map List.toFinset eq).toFinset x) ↔ Complexity.evalMonomialList eq x = false

Boolean parity bridge between monomialSum ℤ and Cslib.Complexity.evalMonomialList.

theorem Cslib.polyNorm1_evalClearedMonomialJet_le {J k B₀ : ℕ} {dDen : ℤ} (hd : dDen.natAbs ≤ B₀) {varJets : List (List ℤ)} {mon : List ℕ} (hdeg : mon.length ≤ k) (hjets : ∀ v ∈ mon, polyNorm1 (truncZJet J (varJets.getD v [])) ≤ B₀) : polyNorm1 (evalClearedMonomialJet J k dDen varJets mon) ≤ B₀ ^ k

Stage-1 monomial $\ell_1$-norm bound ([OAI26c], Appendix B.2).

theorem Cslib.polyNorm1_evalClearedEquationJet_le {J k B₀ : ℕ} {dDen : ℤ} (hd : dDen.natAbs ≤ B₀) {varJets : List (List ℤ)} (hjets : ∀ q ∈ varJets, polyNorm1 (truncZJet J q) ≤ B₀) {eq : List (List ℕ)} (hdeg : ∀ mon ∈ eq, mon.length ≤ k) : polyNorm1 (evalClearedEquationJet J k dDen varJets eq) ≤ eq.length * B₀ ^ k

Stage-1 equation $\ell_1$-norm bound ([OAI26c], Appendix B.2, $B = w \cdot B_0^k$).

theorem Cslib.length_encIntBin_mem_evalClearedEquationJet_le {J k B₀ : ℕ} {dDen : ℤ} (hd : dDen.natAbs ≤ B₀) {varJets : List (List ℤ)} (hjets : ∀ q ∈ varJets, polyNorm1 (truncZJet J q) ≤ B₀) {eq : List (List ℕ)} (hdeg : ∀ mon ∈ eq, mon.length ≤ k) {z : ℤ} (hz : z ∈ evalClearedEquationJet J k dDen varJets eq) : (Turing.MultiTapeTM.encIntBin z).length ≤ eq.length.size + k * B₀.size + 2

Stage-1 entry bit-length bound ([OAI26c], Appendix B.2) under encIntBin.

4. Composite Stage-1 $\to$ Stage-2 parity-factor $z$-jet (evalEquationParityFactorJet)

def Cslib.evalEquationParityFactorJet (J ℓ k : ℕ) (dDen : ℤ) (varJets : List (List ℤ)) (eq : List (List ℕ)) : List (List ℤ)

Composite Stage-1 $\to$ Stage-2 single-equation parity-factor $z$-jet evaluator ([OAI26c], §5.4 and Appendix B.2) with common equation scale $\Delta = d_{\mathrm{den}}^k$ (unconditionally matching parityFactorCleared, and clearing rational denominators by $\Gamma = \Delta^{2 \ell - 1}$ when $d_{\mathrm{den}} \ne 0$).

theorem Cslib.isTableShape_evalEquationParityFactorJet (J ℓ k : ℕ) (dDen : ℤ) (varJets : List (List ℤ)) (eq : List (List ℕ)) : IsTableShape J ℓ (evalEquationParityFactorJet J ℓ k dDen varJets eq)

evalEquationParityFactorJet has rectangular shape J × ℓ (IsTableShape J ℓ).

theorem Cslib.taylor_coeff_parityFactorCleared (t Δ : ℤ) (ℓ s : ℕ) (A : Polynomial ℤ) : (Polynomial.taylor t) ((BitString.parityFactorCleared ℓ (Polynomial.C Δ) A).coeff s) = (BitString.parityFactorCleared ℓ (Polynomial.C Δ) ((Polynomial.taylor t) A)).coeff s

Polynomial.taylor t commutes with taking the $V^s$ coefficient of parityFactorCleared.

theorem Cslib.evalEquationParityFactorJet_entry_eq_parityFactorCleared {J k j : ℕ} (hj : j < J) (ℓ s : ℕ) (dDen : ℤ) {varJets : List (List ℤ)} {θ : ℕ → Polynomial ℤ} {eq : List (List ℕ)} (heq : Complexity.IsCanonicalEquation eq) (hdeg : ∀ mon ∈ eq, mon.length ≤ k) (hθ : ∀ mon ∈ eq, ∀ v ∈ mon, ∀ i < J, rowEntry varJets v i = (θ v).coeff i) : rowEntry (evalEquationParityFactorJet J ℓ k dDen varJets eq) j s = ((BitString.parityFactorCleared ℓ (Polynomial.C (dDen ^ k)) (BitString.clearedMonomialSumPoly dDen k θ (List.map List.toFinset eq).toFinset)).coeff s).coeff j

Composite Stage-1 $\to$ Stage-2 specification ([OAI26c], §5.4 and Appendix B.2) against Cslib.BitString.parityFactorCleared for j < J.

theorem Cslib.evalEquationParityFactorJet_entry_eq_taylor_parityFactorCleared {J k j : ℕ} (hj : j < J) (ℓ s : ℕ) (t dDen : ℤ) {varJets : List (List ℤ)} {θ₀ : ℕ → Polynomial ℤ} {eq : List (List ℕ)} (heq : Complexity.IsCanonicalEquation eq) (hdeg : ∀ mon ∈ eq, mon.length ≤ k) (hθ : ∀ mon ∈ eq, ∀ v ∈ mon, ∀ i < J, rowEntry varJets v i = ((Polynomial.taylor t) (θ₀ v)).coeff i) : rowEntry (evalEquationParityFactorJet J ℓ k dDen varJets eq) j s = ((Polynomial.taylor t) ((BitString.parityFactorCleared ℓ (Polynomial.C (dDen ^ k)) (BitString.clearedMonomialSumPoly dDen k θ₀ (List.map List.toFinset eq).toFinset)).coeff s)).coeff j

Node-$t$ Taylor-shift specialization of evalEquationParityFactorJet for j < J.

theorem Cslib.evalEquationParityFactorJet_row_zero_sum {J ℓ k : ℕ} (hJ : 1 ≤ J) (dDen : ℤ) {varJets : List (List ℤ)} {eq : List (List ℕ)} (heq : Complexity.IsCanonicalEquation eq) (hdeg : ∀ mon ∈ eq, mon.length ≤ k) (x : ℕ → Bool) (hx : ∀ mon ∈ eq, ∀ v ∈ mon, rowEntry varJets v 0 = dDen * BitString.bitVal ℤ (x v)) : ((evalEquationParityFactorJet J ℓ k dDen varJets eq).getD 0 []).sum = (dDen ^ k) ^ (2 * ℓ - 1) * evalParityAmplifier ℓ (BitString.monomialSum ℤ (List.map List.toFinset eq).toFinset x)

Constant-in-$z$ ($j = 0$) row-sum evaluation of evalEquationParityFactorJet (1 ≤ J).

theorem Cslib.jetL1Norm_evalEquationParityFactorJet_le {J ℓ k B₀ : ℕ} {dDen : ℤ} (hd : dDen.natAbs ≤ B₀) {varJets : List (List ℤ)} (hjets : ∀ q ∈ varJets, polyNorm1 (truncZJet J q) ≤ B₀) {eq : List (List ℕ)} (hdeg : ∀ mon ∈ eq, mon.length ≤ k) : jetL1Norm (evalEquationParityFactorJet J ℓ k dDen varJets eq) ≤ ℓ * 2 ^ (7 * ℓ ^ 2) * (eq.length * B₀ ^ k + dDen.natAbs ^ k + 2) ^ (2 * ℓ - 1)

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

theorem Cslib.length_encIntBin_evalEquationParityFactorJet_le {J ℓ k B₀ : ℕ} {dDen : ℤ} (hd : dDen.natAbs ≤ B₀) {varJets : List (List ℤ)} (hjets : ∀ q ∈ varJets, polyNorm1 (truncZJet J q) ≤ B₀) {eq : List (List ℕ)} (hdeg : ∀ mon ∈ eq, mon.length ≤ k) {r : List ℤ} (hr : r ∈ evalEquationParityFactorJet J ℓ k dDen varJets eq) (m : ℕ) : (Turing.MultiTapeTM.encIntBin (List.take m r).sum).length ≤ 8 * ℓ ^ 2 + 2 * ℓ * (eq.length * B₀ ^ k + dDen.natAbs ^ k + 2).size + 2 ∧ ∀ z ∈ r, (Turing.MultiTapeTM.encIntBin z).length ≤ 8 * ℓ ^ 2 + 2 * ℓ * (eq.length * B₀ ^ k + dDen.natAbs ^ k + 2).size + 2

Composite factor-table entry and row-prefix bit-length bound under encIntBin.

5. Plain polynomial-time certificates (ComputableInPolyTime)

theorem Cslib.computableInPolyTime_taylorShiftZJet {α : Type} {encIn : α ↪ List Bool} {J : α → ℕ} {t : α → ℤ} {coeffs : α → List ℤ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encIntBin) (hcoeffs : Turing.MultiTapeTM.ComputableInPolyTime coeffs encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => taylorShiftZJet (J x) (t x) (coeffs x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Compositional plain polynomial-time certificate for taylorShiftZJet on unary J.

theorem Cslib.computableInPolyTime_combineAffineInputZJet {α : Type} {encIn : α ↪ List Bool} {J : α → ℕ} {base : α → ℤ} {corrJet : α → List ℤ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hbase : Turing.MultiTapeTM.ComputableInPolyTime base encIn Turing.MultiTapeTM.encIntBin) (hcorr : Turing.MultiTapeTM.ComputableInPolyTime corrJet encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => combineAffineInputZJet (J a) (base a) (corrJet a)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Compositional plain polynomial-time certificate for combineAffineInputZJet.

theorem Cslib.computableInPolyTime_evalBaselineAt {α : Type} {encIn : α ↪ List Bool} {encX : List Bool ↪ List Bool} {t : α → ℤ} {rowCoeffs : α → List (List ℤ)} {x : α → List Bool} (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encIntBin) (hrow : Turing.MultiTapeTM.ComputableInPolyTime rowCoeffs encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn encX) [Turing.MultiTapeTM.ListEncoding Turing.MultiTapeTM.encBool encX] [Turing.MultiTapeTM.SizedListEncoding Turing.MultiTapeTM.encBool encX] : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => evalBaselineAt (t a) (rowCoeffs a) (x a)) encIn Turing.MultiTapeTM.encIntBin

Compositional plain polynomial-time certificate for evalBaselineAt supporting any sized Boolean list encoding encX (both encBits and encList encBool).

theorem Cslib.computableInPolyTime_evalTaylorCorrectionZJet {α : Type} {encIn : α ↪ List Bool} {encU : List Bool ↪ List Bool} {J : α → ℕ} {t : α → ℤ} {rowCoeffs : α → List (List ℤ)} {U : α → List Bool} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encIntBin) (hrow : Turing.MultiTapeTM.ComputableInPolyTime rowCoeffs encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hU : Turing.MultiTapeTM.ComputableInPolyTime U encIn encU) [Turing.MultiTapeTM.ListEncoding Turing.MultiTapeTM.encBool encU] [Turing.MultiTapeTM.SizedListEncoding Turing.MultiTapeTM.encBool encU] : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => evalTaylorCorrectionZJet (J a) (t a) (rowCoeffs a) (U a)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Compositional plain polynomial-time certificate for evalTaylorCorrectionZJet supporting any sized Boolean list encoding encU (both encBits and encList encBool).

theorem Cslib.computableInPolyTime_evalAffineInputZJet {α : Type} {encIn : α ↪ List Bool} {encU encX : List Bool ↪ List Bool} {J : α → ℕ} {t : α → ℤ} {rowCoeffs : α → List (List ℤ)} {U x : α → List Bool} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encIntBin) (hrow : Turing.MultiTapeTM.ComputableInPolyTime rowCoeffs encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hU : Turing.MultiTapeTM.ComputableInPolyTime U encIn encU) (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn encX) [Turing.MultiTapeTM.ListEncoding Turing.MultiTapeTM.encBool encU] [Turing.MultiTapeTM.SizedListEncoding Turing.MultiTapeTM.encBool encU] [Turing.MultiTapeTM.ListEncoding Turing.MultiTapeTM.encBool encX] [Turing.MultiTapeTM.SizedListEncoding Turing.MultiTapeTM.encBool encX] : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => evalAffineInputZJet (J a) (t a) (rowCoeffs a) (U a) (x a)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Compositional plain polynomial-time certificate for evalAffineInputZJet supporting both encBits and encList encBool for (U, x).

theorem Cslib.computableInPolyTime_evalAffineInputZJetTable {α : Type} {encIn : α ↪ List Bool} {encU encX : List Bool ↪ List Bool} {J : α → ℕ} {t : α → ℤ} {rowsCoeffs : α → List (List (List ℤ))} {U x : α → List Bool} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encIntBin) (hrows : Turing.MultiTapeTM.ComputableInPolyTime rowsCoeffs encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) (hU : Turing.MultiTapeTM.ComputableInPolyTime U encIn encU) (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn encX) [Turing.MultiTapeTM.ListEncoding Turing.MultiTapeTM.encBool encU] [Turing.MultiTapeTM.SizedListEncoding Turing.MultiTapeTM.encBool encU] [Turing.MultiTapeTM.ListEncoding Turing.MultiTapeTM.encBool encX] [Turing.MultiTapeTM.SizedListEncoding Turing.MultiTapeTM.encBool encX] : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => evalAffineInputZJetTable (J a) (t a) (rowsCoeffs a) (U a) (x a)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Compositional plain polynomial-time certificate for evalAffineInputZJetTable supporting both encBits and encList encBool for (U, x).

theorem Cslib.computableInPolyTime_evalClearedMonomialJet {α : Type} {encIn : α ↪ List Bool} {J k : α → ℕ} {dDen : α → ℤ} {varJets : α → List (List ℤ)} {mon : α → List ℕ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k encIn Turing.MultiTapeTM.encUnary) (hdDen : Turing.MultiTapeTM.ComputableInPolyTime dDen encIn Turing.MultiTapeTM.encIntBin) (hvarJets : Turing.MultiTapeTM.ComputableInPolyTime varJets encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hmon : Turing.MultiTapeTM.ComputableInPolyTime mon encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => evalClearedMonomialJet (J x) (k x) (dDen x) (varJets x) (mon x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Compositional plain polynomial-time certificate for evalClearedMonomialJet on unary (J, k).

theorem Cslib.computableInPolyTime_evalClearedEquationJet {α : Type} {encIn : α ↪ List Bool} {J k : α → ℕ} {dDen : α → ℤ} {varJets : α → List (List ℤ)} {eq : α → List (List ℕ)} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k encIn Turing.MultiTapeTM.encUnary) (hdDen : Turing.MultiTapeTM.ComputableInPolyTime dDen encIn Turing.MultiTapeTM.encIntBin) (hvarJets : Turing.MultiTapeTM.ComputableInPolyTime varJets encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (heq : Turing.MultiTapeTM.ComputableInPolyTime eq encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => evalClearedEquationJet (J x) (k x) (dDen x) (varJets x) (eq x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Compositional plain polynomial-time certificate for evalClearedEquationJet on unary (J, k).

theorem Cslib.computableInPolyTime_evalEquationParityFactorJet {α : Type} {encIn : α ↪ List Bool} {J ℓ k : α → ℕ} {dDen : α → ℤ} {varJets : α → List (List ℤ)} {eq : α → List (List ℕ)} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k encIn Turing.MultiTapeTM.encUnary) (hdDen : Turing.MultiTapeTM.ComputableInPolyTime dDen encIn Turing.MultiTapeTM.encIntBin) (hvarJets : Turing.MultiTapeTM.ComputableInPolyTime varJets encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (heq : Turing.MultiTapeTM.ComputableInPolyTime eq encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => evalEquationParityFactorJet (J x) (ℓ x) (k x) (dDen x) (varJets x) (eq x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Compositional plain polynomial-time certificate for evalEquationParityFactorJet ([OAI26c], Appendix B.2) on unary (J, ℓ, k).