Computing binary matrices of field maps and of Frobenius

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

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

Compute a field map on the polynomial basis, then transpose the column list.

Equations

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

theorem MIPRE.SAT.fieldMapMatrixProg_correct (k : ℕ) (hk : 1 ≤ k) (L : (shoupBinField k hk).carrier →ₗ[ZMod 2] (shoupBinField k hk).carrier) (f : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr) Cost.BitStr) (hf : ∀ (a : (shoupBinField k hk).carrier), f.toFun (Cost.unary k, (shoupBinField k hk).toBits a) = (shoupBinField k hk).toBits (L a)) : (fieldMapMatrixProg f).toFun (Cost.unary k) = LowDegree.BinaryLinear.matrixBits ((LinearMap.toMatrix (shoupPowerBasis k hk) (shoupPowerBasis k hk)) L)

A canonically encoded linear map gives its exact matrix in the effective basis.

noncomputable def MIPRE.SAT.shoupFrobeniusLinear (k : ℕ) (hk : 1 ≤ k) : (shoupBinField k hk).carrier →ₗ[ZMod 2] (shoupBinField k hk).carrier

Frobenius as a binary linear map on the concrete quotient field.

Equations

• MIPRE.SAT.shoupFrobeniusLinear k hk = (FiniteField.frobeniusAlgHom (ZMod 2) (MIPRE.SAT.shoupBinField k hk).carrier).toLinearMap

@[simp]

theorem MIPRE.SAT.shoupFrobeniusLinear_apply (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) : (shoupFrobeniusLinear k hk) a = a ^ 2

noncomputable def MIPRE.SAT.shoupFrobeniusMatrix (k : ℕ) (hk : 1 ≤ k) : Matrix (Fin k) (Fin k) (ZMod 2)

Frobenius in the actual polynomial-basis coordinates.

Equations

• MIPRE.SAT.shoupFrobeniusMatrix k hk = (LinearMap.toMatrix (MIPRE.SAT.shoupPowerBasis k hk) (MIPRE.SAT.shoupPowerBasis k hk)) (MIPRE.SAT.shoupFrobeniusLinear k hk)

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

One squaring, including uniform modulus construction.

Equations

• MIPRE.SAT.shoupSquareProg = MIPRE.SAT.shoupMulProg.comp (MIPRE.Cost.PolyTimeFun.fst.pair (MIPRE.Cost.PolyTimeFun.snd.pair MIPRE.Cost.PolyTimeFun.snd))

theorem MIPRE.SAT.shoupSquareProg_correct (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) : shoupSquareProg.toFun (Cost.unary k, (shoupBinField k hk).toBits a) = (shoupBinField k hk).toBits ((shoupFrobeniusLinear k hk) a)

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

One polynomial-time program constructs the full binary Frobenius matrix.

Equations

• MIPRE.SAT.shoupFrobeniusMatrixProg = MIPRE.SAT.fieldMapMatrixProg MIPRE.SAT.shoupSquareProg

theorem MIPRE.SAT.shoupFrobeniusMatrixProg_correct (k : ℕ) (hk : 1 ≤ k) : shoupFrobeniusMatrixProg.toFun (Cost.unary k) = LowDegree.BinaryLinear.matrixBits (shoupFrobeniusMatrix k hk)

theorem MIPRE.SAT.shoupFrobeniusMatrix_minpoly (k : ℕ) (hk : 1 ≤ k) : minpoly (ZMod 2) (shoupFrobeniusMatrix k hk) = Polynomial.X ^ k - 1

The full field degree is the degree of Frobenius's minimal polynomial.

theorem MIPRE.SAT.shoupFrobeniusMatrix_period (k : ℕ) (hk : 1 ≤ k) : shoupFrobeniusMatrix k hk ^ k = 1

The matrix computed by the program has period dividing the field degree.

theorem MIPRE.SAT.shoupFrobeniusMatrix_squarefree (k : ℕ) (hk : 1 ≤ k) (hodd : Odd k) : Squarefree (minpoly (ZMod 2) (shoupFrobeniusMatrix k hk))

Odd degree makes the Frobenius minimal polynomial squarefree.

theorem MIPRE.SAT.shoupFrobeniusMatrixProg_time_le : ∃ (R : Polynomial ℕ), ∀ (k : ℕ), ∃ t ≤ Polynomial.eval k R, shoupFrobeniusMatrixProg.code.Runs (Cost.encode (Cost.unary k)) (Cost.encode (shoupFrobeniusMatrixProg.toFun (Cost.unary k))) t

On unary degree input the complete matrix construction has polynomial runtime.