Dense truncated bivariate jet arrays in polynomial time

Appendix B.2 of OpenAI, The Exponential Time Hypothesis is False represents elements of the truncated bivariate polynomial ring ℤ[V]/(V^ℓ)[z]/(z^J) as dense J × ℓ tables of integer coefficients, stored in their unique representative modulo (z^J, V^ℓ).

Building on the rectangular integer table primitives (Cslib.IsTableShape, Cslib.rowEntry, Cslib.tabulateTable) in Complexity/Computability/PolyTime/Int/Table.lean, this module provides executable truncated jet operations on List (List ℤ) (Cslib.JetRows), proves exact coefficient formulas and commutative-ring laws on (J, ℓ)-shaped arrays, establishes ℓ₁ coefficient-norm and binary bit-length bounds for truncated 2D convolution, and certifies that every operation is computable in polynomial time on multi-tape Turing machines (Turing.MultiTapeTM.ComputableInPolyTime) with dimensions (J, ℓ) in unary and coefficient tables in encList (encList encIntBin).

Main definitions

• Cslib.JetRows: alias List (List ℤ) for dense J × ℓ coefficient tables.
• Cslib.zeroJet, Cslib.constJet, Cslib.zJet, Cslib.vJet: zero, constant, and generator jet arrays.
• Cslib.addJet, Cslib.negJet, Cslib.subJet, Cslib.smulJet: linear operations on J × ℓ jet arrays.
• Cslib.shiftZJet, Cslib.shiftVJet: multiplication by z modulo z^J and by V modulo V^ℓ.
• Cslib.convEntry, Cslib.convJet: truncated 2D Cauchy product in O(J^2 ℓ^2) integer operations.
• Cslib.jetL1Norm: the ℓ₁ coefficient norm ∑ |c_{j, u}| of a list of rows.

Main results

• Cslib.rowEntry_zeroJet, Cslib.rowEntry_constJet, Cslib.rowEntry_addJet, Cslib.rowEntry_negJet, Cslib.rowEntry_subJet, Cslib.rowEntry_smulJet, Cslib.rowEntry_shiftZJet, Cslib.rowEntry_shiftVJet, Cslib.rowEntry_convJet: exact in-bounds coefficient formulas.
• Cslib.addJet_comm, Cslib.addJet_assoc, Cslib.convJet_comm, Cslib.convJet_assoc, Cslib.convJet_addJet, Cslib.addJet_convJet, Cslib.constJet_one_convJet, Cslib.convJet_constJet_one: commutative-ring identities on (J, ℓ)-shaped arrays.
• Cslib.jetL1Norm_addJet_le, Cslib.jetL1Norm_convJet_le: subadditivity and submultiplicativity of the ℓ₁ coefficient norm under truncated addition and 2D convolution.
• Cslib.size_natAbs_rowEntry_convJet_le, Cslib.length_encIntBin_mem_convJet_le: binary magnitude and encoded bit-length bounds on entries of convJet.
• Cslib.computableInPolyTime_zeroJet, Cslib.computableInPolyTime_constJet, Cslib.computableInPolyTime_addJet, Cslib.computableInPolyTime_negJet, Cslib.computableInPolyTime_subJet, Cslib.computableInPolyTime_smulJet, Cslib.computableInPolyTime_shiftZJet, Cslib.computableInPolyTime_shiftVJet, Cslib.computableInPolyTime_convJet: plain ComputableInPolyTime composition rules and direct certificates (zeroJet_polytime, …, convJet_polytime).

References

• OpenAI, The Exponential Time Hypothesis is False

@[reducible, inline]

abbrev Cslib.JetRows : Type

Dense list-of-rows representation of truncated bivariate jets in ℤ[V]/(V^ℓ)[z]/(z^J).

Executable jet operations

def Cslib.zeroJet (J ℓ : ℕ) : List (List ℤ)

The J × ℓ zero jet array.

def Cslib.constJet (J ℓ : ℕ) (c : ℤ) : List (List ℤ)

The constant jet c placed at (0, 0) and 0 elsewhere, truncated to J × ℓ.

def Cslib.zJet (J ℓ : ℕ) : List (List ℤ)

The generator z in ℤ[V]/(V^ℓ)[z]/(z^J) (1 at (1, 0) when in range).

def Cslib.vJet (J ℓ : ℕ) : List (List ℤ)

The generator V in ℤ[V]/(V^ℓ)[z]/(z^J) (1 at (0, 1) when in range).

def Cslib.addJet (J ℓ : ℕ) (A B : List (List ℤ)) : List (List ℤ)

Entrywise addition of two jet arrays, normalized to shape J × ℓ.

def Cslib.negJet (J ℓ : ℕ) (A : List (List ℤ)) : List (List ℤ)

Entrywise negation of a jet array, normalized to shape J × ℓ.

def Cslib.subJet (J ℓ : ℕ) (A B : List (List ℤ)) : List (List ℤ)

Entrywise subtraction of two jet arrays, normalized to shape J × ℓ.

def Cslib.smulJet (J ℓ : ℕ) (c : ℤ) (A : List (List ℤ)) : List (List ℤ)

Entrywise integer scalar multiplication of a jet array, normalized to shape J × ℓ.

def Cslib.shiftZJet (J ℓ : ℕ) (A : List (List ℤ)) : List (List ℤ)

Multiplication by z modulo z^J, shifting row index up by 1 and dropping row J - 1.

def Cslib.shiftVJet (J ℓ : ℕ) (A : List (List ℤ)) : List (List ℤ)

Multiplication by V modulo V^ℓ, shifting column index up by 1 and dropping ℓ - 1.

def Cslib.convEntry (A B : List (List ℤ)) (j u : ℕ) : ℤ

Coefficient (j, u) of the 2D Cauchy product of A and B, computed over List.range.

def Cslib.convJet (J ℓ : ℕ) (A B : List (List ℤ)) : List (List ℤ)

Truncated 2D convolution in ℤ[V]/(V^ℓ)[z]/(z^J) using O(J^2 ℓ^2) integer operations.

Output shape and exact coefficient semantics

theorem Cslib.isTableShape_zeroJet (J ℓ : ℕ) : IsTableShape J ℓ (zeroJet J ℓ)

theorem Cslib.isTableShape_constJet (J ℓ : ℕ) (c : ℤ) : IsTableShape J ℓ (constJet J ℓ c)

theorem Cslib.isTableShape_zJet (J ℓ : ℕ) : IsTableShape J ℓ (zJet J ℓ)

theorem Cslib.isTableShape_vJet (J ℓ : ℕ) : IsTableShape J ℓ (vJet J ℓ)

theorem Cslib.isTableShape_addJet (J ℓ : ℕ) (A B : List (List ℤ)) : IsTableShape J ℓ (addJet J ℓ A B)

theorem Cslib.isTableShape_negJet (J ℓ : ℕ) (A : List (List ℤ)) : IsTableShape J ℓ (negJet J ℓ A)

theorem Cslib.isTableShape_subJet (J ℓ : ℕ) (A B : List (List ℤ)) : IsTableShape J ℓ (subJet J ℓ A B)

theorem Cslib.isTableShape_smulJet (J ℓ : ℕ) (c : ℤ) (A : List (List ℤ)) : IsTableShape J ℓ (smulJet J ℓ c A)

theorem Cslib.isTableShape_shiftZJet (J ℓ : ℕ) (A : List (List ℤ)) : IsTableShape J ℓ (shiftZJet J ℓ A)

theorem Cslib.isTableShape_shiftVJet (J ℓ : ℕ) (A : List (List ℤ)) : IsTableShape J ℓ (shiftVJet J ℓ A)

theorem Cslib.isTableShape_convJet (J ℓ : ℕ) (A B : List (List ℤ)) : IsTableShape J ℓ (convJet J ℓ A B)

theorem Cslib.convEntry_eq_sum (A B : List (List ℤ)) (j u : ℕ) : convEntry A B j u = ∑ j₁ ∈ Finset.range (j + 1), ∑ u₁ ∈ Finset.range (u + 1), rowEntry A j₁ u₁ * rowEntry B (j - j₁) (u - u₁)

@[simp]

theorem Cslib.rowEntry_zeroJet (J ℓ j u : ℕ) : rowEntry (zeroJet J ℓ) j u = 0

theorem Cslib.rowEntry_constJet {J ℓ : ℕ} (c : ℤ) {j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (constJet J ℓ c) j u = if j = 0 ∧ u = 0 then c else 0

theorem Cslib.rowEntry_zJet {J ℓ j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (zJet J ℓ) j u = if j = 1 ∧ u = 0 then 1 else 0

theorem Cslib.rowEntry_vJet {J ℓ j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (vJet J ℓ) j u = if j = 0 ∧ u = 1 then 1 else 0

theorem Cslib.rowEntry_addJet {J ℓ : ℕ} (A B : List (List ℤ)) {j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (addJet J ℓ A B) j u = rowEntry A j u + rowEntry B j u

theorem Cslib.rowEntry_negJet {J ℓ : ℕ} (A : List (List ℤ)) {j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (negJet J ℓ A) j u = -rowEntry A j u

theorem Cslib.rowEntry_subJet {J ℓ : ℕ} (A B : List (List ℤ)) {j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (subJet J ℓ A B) j u = rowEntry A j u - rowEntry B j u

theorem Cslib.rowEntry_smulJet {J ℓ : ℕ} (c : ℤ) (A : List (List ℤ)) {j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (smulJet J ℓ c A) j u = c * rowEntry A j u

theorem Cslib.rowEntry_shiftZJet {J ℓ : ℕ} (A : List (List ℤ)) {j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (shiftZJet J ℓ A) j u = if j = 0 then 0 else rowEntry A (j - 1) u

theorem Cslib.rowEntry_shiftVJet {J ℓ : ℕ} (A : List (List ℤ)) {j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (shiftVJet J ℓ A) j u = if u = 0 then 0 else rowEntry A j (u - 1)

theorem Cslib.rowEntry_convJet {J ℓ : ℕ} (A B : List (List ℤ)) {j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (convJet J ℓ A B) j u = ∑ j₁ ∈ Finset.range (j + 1), ∑ u₁ ∈ Finset.range (u + 1), rowEntry A j₁ u₁ * rowEntry B (j - j₁) (u - u₁)

Algebraic identities on (J, ℓ)-shaped jet arrays

theorem Cslib.addJet_comm (J ℓ : ℕ) (A B : List (List ℤ)) : addJet J ℓ A B = addJet J ℓ B A

theorem Cslib.addJet_assoc (J ℓ : ℕ) (A B C : List (List ℤ)) : addJet J ℓ (addJet J ℓ A B) C = addJet J ℓ A (addJet J ℓ B C)

theorem Cslib.zeroJet_addJet {J ℓ : ℕ} {A : List (List ℤ)} (hA : IsTableShape J ℓ A) : addJet J ℓ (zeroJet J ℓ) A = A

theorem Cslib.addJet_zeroJet {J ℓ : ℕ} {A : List (List ℤ)} (hA : IsTableShape J ℓ A) : addJet J ℓ A (zeroJet J ℓ) = A

theorem Cslib.negJet_addJet (J ℓ : ℕ) (A : List (List ℤ)) : addJet J ℓ (negJet J ℓ A) A = zeroJet J ℓ

theorem Cslib.addJet_negJet (J ℓ : ℕ) (A : List (List ℤ)) : addJet J ℓ A (negJet J ℓ A) = zeroJet J ℓ

theorem Cslib.subJet_eq_addJet_negJet (J ℓ : ℕ) (A B : List (List ℤ)) : subJet J ℓ A B = addJet J ℓ A (negJet J ℓ B)

theorem Cslib.smulJet_addJet (J ℓ : ℕ) (c : ℤ) (A B : List (List ℤ)) : smulJet J ℓ c (addJet J ℓ A B) = addJet J ℓ (smulJet J ℓ c A) (smulJet J ℓ c B)

theorem Cslib.one_smulJet {J ℓ : ℕ} {A : List (List ℤ)} (hA : IsTableShape J ℓ A) : smulJet J ℓ 1 A = A

theorem Cslib.convJet_comm (J ℓ : ℕ) (A B : List (List ℤ)) : convJet J ℓ A B = convJet J ℓ B A

Commutativity of truncated 2D convolution.

theorem Cslib.convJet_assoc (J ℓ : ℕ) (A B C : List (List ℤ)) : convJet J ℓ (convJet J ℓ A B) C = convJet J ℓ A (convJet J ℓ B C)

Associativity of truncated 2D convolution.

theorem Cslib.convJet_addJet (J ℓ : ℕ) (A B C : List (List ℤ)) : convJet J ℓ A (addJet J ℓ B C) = addJet J ℓ (convJet J ℓ A B) (convJet J ℓ A C)

Left distributivity of truncated 2D convolution over addition.

theorem Cslib.addJet_convJet (J ℓ : ℕ) (A B C : List (List ℤ)) : convJet J ℓ (addJet J ℓ A B) C = addJet J ℓ (convJet J ℓ A C) (convJet J ℓ B C)

Right distributivity of truncated 2D convolution over addition.

theorem Cslib.zeroJet_convJet (J ℓ : ℕ) (A : List (List ℤ)) : convJet J ℓ (zeroJet J ℓ) A = zeroJet J ℓ

theorem Cslib.convJet_zeroJet (J ℓ : ℕ) (A : List (List ℤ)) : convJet J ℓ A (zeroJet J ℓ) = zeroJet J ℓ

theorem Cslib.constJet_convJet (J ℓ : ℕ) (c : ℤ) (A : List (List ℤ)) : convJet J ℓ (constJet J ℓ c) A = smulJet J ℓ c A

theorem Cslib.convJet_constJet (J ℓ : ℕ) (A : List (List ℤ)) (c : ℤ) : convJet J ℓ A (constJet J ℓ c) = smulJet J ℓ c A

theorem Cslib.constJet_one_convJet {J ℓ : ℕ} {A : List (List ℤ)} (hA : IsTableShape J ℓ A) : convJet J ℓ (constJet J ℓ 1) A = A

theorem Cslib.convJet_constJet_one {J ℓ : ℕ} {A : List (List ℤ)} (hA : IsTableShape J ℓ A) : convJet J ℓ A (constJet J ℓ 1) = A

theorem Cslib.smulJet_convJet (J ℓ : ℕ) (c : ℤ) (A B : List (List ℤ)) : convJet J ℓ (smulJet J ℓ c A) B = smulJet J ℓ c (convJet J ℓ A B)

theorem Cslib.convJet_smulJet (J ℓ : ℕ) (c : ℤ) (A B : List (List ℤ)) : convJet J ℓ A (smulJet J ℓ c B) = smulJet J ℓ c (convJet J ℓ A B)

theorem Cslib.shiftZJet_eq_convJet (J ℓ : ℕ) (A : List (List ℤ)) : shiftZJet J ℓ A = convJet J ℓ (zJet J ℓ) A

shiftZJet agrees with multiplying by the generator zJet under convJet.

theorem Cslib.shiftVJet_eq_convJet (J ℓ : ℕ) (A : List (List ℤ)) : shiftVJet J ℓ A = convJet J ℓ (vJet J ℓ) A

shiftVJet agrees with multiplying by the generator vJet under convJet.

ℓ₁ coefficient norm and binary bit-length bounds

def Cslib.jetL1Norm (A : List (List ℤ)) : ℕ

The ℓ₁ coefficient norm ∑ |c| of a list of integer rows.

theorem Cslib.jetL1Norm_tabulateTable (J ℓ : ℕ) (g : ℕ → ℕ → ℤ) : jetL1Norm (tabulateTable J ℓ g) = ∑ j ∈ Finset.range J, ∑ u ∈ Finset.range ℓ, (g j u).natAbs

theorem Cslib.sum_rowEntry_natAbs_le_jetL1Norm (J ℓ : ℕ) (A : List (List ℤ)) : ∑ j ∈ Finset.range J, ∑ u ∈ Finset.range ℓ, (rowEntry A j u).natAbs ≤ jetL1Norm A

Truncating any list of rows to (J, ℓ) cannot increase its ℓ₁ coefficient norm.

theorem Cslib.jetL1Norm_eq_sum_rowEntry {J ℓ : ℕ} {A : List (List ℤ)} (hA : IsTableShape J ℓ A) : jetL1Norm A = ∑ j ∈ Finset.range J, ∑ u ∈ Finset.range ℓ, (rowEntry A j u).natAbs

On a (J, ℓ)-shaped jet array, jetL1Norm equals the sum of in-bounds |rowEntry A j u|.

@[simp]

theorem Cslib.jetL1Norm_zeroJet (J ℓ : ℕ) : jetL1Norm (zeroJet J ℓ) = 0

theorem Cslib.jetL1Norm_constJet_le (J ℓ : ℕ) (c : ℤ) : jetL1Norm (constJet J ℓ c) ≤ c.natAbs

theorem Cslib.jetL1Norm_negJet_le (J ℓ : ℕ) (A : List (List ℤ)) : jetL1Norm (negJet J ℓ A) ≤ jetL1Norm A

theorem Cslib.jetL1Norm_addJet_le (J ℓ : ℕ) (A B : List (List ℤ)) : jetL1Norm (addJet J ℓ A B) ≤ jetL1Norm A + jetL1Norm B

Triangle inequality for the ℓ₁ coefficient norm under addJet.

theorem Cslib.jetL1Norm_subJet_le (J ℓ : ℕ) (A B : List (List ℤ)) : jetL1Norm (subJet J ℓ A B) ≤ jetL1Norm A + jetL1Norm B

theorem Cslib.jetL1Norm_smulJet_le (J ℓ : ℕ) (c : ℤ) (A : List (List ℤ)) : jetL1Norm (smulJet J ℓ c A) ≤ c.natAbs * jetL1Norm A

theorem Cslib.jetL1Norm_shiftZJet_le (J ℓ : ℕ) (A : List (List ℤ)) : jetL1Norm (shiftZJet J ℓ A) ≤ jetL1Norm A

theorem Cslib.jetL1Norm_shiftVJet_le (J ℓ : ℕ) (A : List (List ℤ)) : jetL1Norm (shiftVJet J ℓ A) ≤ jetL1Norm A

theorem Cslib.jetL1Norm_convJet_le (J ℓ : ℕ) (A B : List (List ℤ)) : jetL1Norm (convJet J ℓ A B) ≤ jetL1Norm A * jetL1Norm B

Submultiplicativity of the ℓ₁ coefficient norm under truncated 2D convolution (OpenAI, The Exponential Time Hypothesis is False, Appendix B.2): ‖A * B mod (z^J, V^ℓ)‖₁ ≤ ‖A‖₁ · ‖B‖₁.

theorem Cslib.natAbs_le_jetL1Norm_of_mem {A : List (List ℤ)} {row : List ℤ} (hrow : row ∈ A) {z : ℤ} (hz : z ∈ row) : z.natAbs ≤ jetL1Norm A

Every stored entry of A has magnitude bounded by jetL1Norm A.

theorem Cslib.natAbs_rowEntry_le_jetL1Norm (A : List (List ℤ)) (j u : ℕ) : (rowEntry A j u).natAbs ≤ jetL1Norm A

Every coefficient rowEntry A j u has magnitude bounded by jetL1Norm A.

theorem Cslib.natAbs_rowEntry_convJet_le_norm (J ℓ : ℕ) (A B : List (List ℤ)) (j u : ℕ) : (rowEntry (convJet J ℓ A B) j u).natAbs ≤ jetL1Norm A * jetL1Norm B

Magnitude bound on every entry of convJet in terms of input ℓ₁ norms.

theorem Cslib.length_encIntBin_mem_convJet_le_norm {J ℓ : ℕ} {A B : List (List ℤ)} {row : List ℤ} (hrow : row ∈ convJet J ℓ A B) {z : ℤ} (hz : z ∈ row) : (Turing.MultiTapeTM.encIntBin z).length ≤ (jetL1Norm A * jetL1Norm B).size + 1

Encoded bit-length bound on every stored entry of convJet via input ℓ₁ norms.

theorem Cslib.natAbs_rowEntry_convJet_le {J ℓ MA MB : ℕ} {A B : List (List ℤ)} (hA : ∀ row ∈ A, ∀ z ∈ row, z.natAbs ≤ MA) (hB : ∀ row ∈ B, ∀ z ∈ row, z.natAbs ≤ MB) (j u : ℕ) : (rowEntry (convJet J ℓ A B) j u).natAbs ≤ J * ℓ * (MA * MB)

Entrywise max-magnitude bound for convJet: if entries of A and B have magnitudes at most MA and MB, then every coefficient of convJet J ℓ A B has magnitude at most J * ℓ * (MA * MB).

theorem Cslib.size_natAbs_rowEntry_convJet_le {J ℓ bA bB : ℕ} {A B : List (List ℤ)} (hA : ∀ row ∈ A, ∀ z ∈ row, z.natAbs.size ≤ bA) (hB : ∀ row ∈ B, ∀ z ∈ row, z.natAbs.size ≤ bB) (j u : ℕ) : (rowEntry (convJet J ℓ A B) j u).natAbs.size ≤ bA + bB + (J * ℓ).size

Binary magnitude-size bound for convJet: if stored entries of A and B have binary magnitude size at most bA and bB, then every coefficient of convJet J ℓ A B has binary magnitude size at most bA + bB + (J * ℓ).size.

theorem Cslib.length_encIntBin_mem_convJet_le {J ℓ bA bB : ℕ} {A B : List (List ℤ)} (hA : ∀ row ∈ A, ∀ z ∈ row, (Turing.MultiTapeTM.encIntBin z).length ≤ bA + 1) (hB : ∀ row ∈ B, ∀ z ∈ row, (Turing.MultiTapeTM.encIntBin z).length ≤ bB + 1) {row : List ℤ} (hrow : row ∈ convJet J ℓ A B) {z : ℤ} (hz : z ∈ row) : (Turing.MultiTapeTM.encIntBin z).length ≤ bA + bB + (J * ℓ).size + 1

Encoded bit-length bound for every stored entry of convJet: if stored entries of A and B have encIntBin length at most bA + 1 and bB + 1, then every stored entry of convJet J ℓ A B has encIntBin length at most bA + bB + (J * ℓ).size + 1.

Plain polynomial-time certificates

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

zeroJet is computable in polynomial time for unary (J, ℓ).

theorem Cslib.computableInPolyTime_constJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {c : α → ℤ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hc : Turing.MultiTapeTM.ComputableInPolyTime c encIn Turing.MultiTapeTM.encIntBin) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => constJet (J x) (ℓ x) (c x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

constJet is computable in polynomial time for unary (J, ℓ) and binary c.

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

zJet is computable in polynomial time for unary (J, ℓ).

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

vJet is computable in polynomial time for unary (J, ℓ).

theorem Cslib.computableInPolyTime_addJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {A B : α → List (List ℤ)} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hB : Turing.MultiTapeTM.ComputableInPolyTime B encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => addJet (J x) (ℓ x) (A x) (B x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

addJet is computable in polynomial time.

theorem Cslib.computableInPolyTime_negJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {A : α → List (List ℤ)} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => negJet (J x) (ℓ x) (A x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

negJet is computable in polynomial time.

theorem Cslib.computableInPolyTime_subJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {A B : α → List (List ℤ)} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hB : Turing.MultiTapeTM.ComputableInPolyTime B encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => subJet (J x) (ℓ x) (A x) (B x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

subJet is computable in polynomial time.

theorem Cslib.computableInPolyTime_smulJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {c : α → ℤ} {A : α → List (List ℤ)} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hc : Turing.MultiTapeTM.ComputableInPolyTime c encIn Turing.MultiTapeTM.encIntBin) (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => smulJet (J x) (ℓ x) (c x) (A x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

smulJet is computable in polynomial time.

theorem Cslib.computableInPolyTime_shiftZJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {A : α → List (List ℤ)} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => shiftZJet (J x) (ℓ x) (A x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

shiftZJet is computable in polynomial time.

theorem Cslib.computableInPolyTime_shiftVJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {A : α → List (List ℤ)} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => shiftVJet (J x) (ℓ x) (A x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

shiftVJet is computable in polynomial time.

theorem Cslib.computableInPolyTime_convEntry {α : Type} {encIn : α ↪ List Bool} {A B : α → List (List ℤ)} {j u : α → ℕ} (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hB : Turing.MultiTapeTM.ComputableInPolyTime B encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => convEntry (A x) (B x) (j x) (u x)) encIn Turing.MultiTapeTM.encIntBin

Computing a single truncated 2D convolution coefficient convEntry is polynomial-time.

theorem Cslib.computableInPolyTime_convJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {A B : α → List (List ℤ)} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hB : Turing.MultiTapeTM.ComputableInPolyTime B encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => convJet (J x) (ℓ x) (A x) (B x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Truncated 2D convolution convJet is computable in polynomial time for unary (J, ℓ) and dense List (List ℤ) arrays over encIntBin.

theorem Cslib.zeroJet_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => zeroJet p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Direct polynomial-time certificate for zeroJet.

theorem Cslib.constJet_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × ℤ) => constJet p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encIntBin) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Direct polynomial-time certificate for constJet.

theorem Cslib.addJet_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ)) => addJet p.1.1.1 p.1.1.2 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Direct polynomial-time certificate for addJet.

theorem Cslib.negJet_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × List (List ℤ)) => negJet p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Direct polynomial-time certificate for negJet.

theorem Cslib.subJet_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ)) => subJet p.1.1.1 p.1.1.2 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Direct polynomial-time certificate for subJet.

theorem Cslib.smulJet_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ((ℕ × ℕ) × ℤ) × List (List ℤ)) => smulJet p.1.1.1 p.1.1.2 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encIntBin) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Direct polynomial-time certificate for smulJet.

theorem Cslib.shiftZJet_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × List (List ℤ)) => shiftZJet p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Direct polynomial-time certificate for shiftZJet.

theorem Cslib.shiftVJet_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × List (List ℤ)) => shiftVJet p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Direct polynomial-time certificate for shiftVJet.

theorem Cslib.convJet_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ)) => convJet p.1.1.1 p.1.1.2 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Direct polynomial-time certificate for convJet.