Polynomial-time transport to any supplied binary field basis

theorem MIPRE.SAT.instFactPrimeOfNatNat_mIPRE_2 : Fact (Nat.Prime 2)

noncomputable def MIPRE.SAT.shoupBasisMatrix (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) : Matrix (Fin k) (Fin k) (ZMod 2)

Columns of a new basis in the original, effective polynomial basis.

Equations

• MIPRE.SAT.shoupBasisMatrix k hk b = (LinearMap.toMatrix b (MIPRE.SAT.shoupPowerBasis k hk)) LinearMap.id

theorem MIPRE.SAT.shoupBasisMatrix_encoding (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) : LowDegree.BinaryLinear.transposeBits k (List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i)) = LowDegree.BinaryLinear.matrixBits (shoupBasisMatrix k hk b)

The supplied basis vectors are exactly the columns of the change-of-basis matrix.

theorem MIPRE.SAT.shoupBasisMatrix_mulVec (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (a : (shoupBinField k hk).carrier) : (shoupBasisMatrix k hk b).mulVec (b.equivFun a) = (shoupCoordinateEquiv k hk) a

Matrix application sends the new coordinates to the original coordinates.

theorem MIPRE.SAT.shoupBasisMatrix_surjective (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) : Function.Surjective (shoupBasisMatrix k hk b).mulVec

noncomputable def MIPRE.SAT.shoupInBasisProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr × Cost.BitStr) Cost.BitStr

Read a field element in an arbitrary basis supplied as polynomial-basis vectors.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.SAT.shoupInBasisProg_correct (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (a : (shoupBinField k hk).carrier) : shoupInBasisProg.toFun (Cost.unary k, List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i), (shoupBinField k hk).toBits a) = LowDegree.BinaryLinear.vectorBits (b.equivFun a)

The computed coordinates are exactly the mathematical basis coordinates.

noncomputable def MIPRE.SAT.shoupMultiplicationTableProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr) (List (List Cost.BitStr))

All multiplication-table bits, with the two basis indices as the first two list indices.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.SAT.shoupMultiplicationTableProg_correct (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) : shoupMultiplicationTableProg.toFun (Cost.unary k, List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i)) = List.ofFn fun (i : Fin k) => List.ofFn fun (j : Fin k) => LowDegree.BinaryLinear.vectorBits (b.equivFun (b i * b j))

Table transport is correct for every supplied basis, including a self-dual normal basis.

theorem MIPRE.SAT.esize_shoupBasis (k : ℕ) (hk : 1 ≤ k) (v : Fin k → (shoupBinField k hk).carrier) : Cost.esize (List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (v i)) ≤ k * (4 * k + 2) + 1

A k-vector field basis has quadratic encoded size.

theorem MIPRE.SAT.shoupMultiplicationTableProg_time_le : ∃ (R : Polynomial ℕ), ∀ (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier), ∃ t ≤ Polynomial.eval k R, shoupMultiplicationTableProg.code.Runs (Cost.encode (Cost.unary k, List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i))) (Cost.encode (shoupMultiplicationTableProg.toFun (Cost.unary k, List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i)))) t

Printing all k³ table bits, including every solve, takes polynomial time in k.