Effective trace Gram matrices

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

theorem MIPRE.SAT.shoupBinField_oneBits (k : ℕ) (hk : 1 ≤ k) (v : Cost.BitStr) (hv : List.length v = k) : LowDegree.BinaryPolynomial.oneBits v = (shoupBinField k hk).toBits 1

The actual coefficient-vector representation of the unit.

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

Output the trace as one base-field bit, rather than an extension-field vector.

Equations

• MIPRE.SAT.shoupTraceBitProg = MIPRE.SAT.ArrayProg.eqBits.comp (MIPRE.SAT.shoupTraceProg.pair (MIPRE.LowDegree.BinaryPolynomial.oneBitsProg.comp MIPRE.Cost.PolyTimeFun.snd))

theorem MIPRE.SAT.shoupTraceBitProg_correct (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) : shoupTraceBitProg.toFun (Cost.unary k, (shoupBinField k hk).toBits a) = LowDegree.BinaryLinear.bit ((Algebra.trace (ZMod 2) (shoupBinField k hk).carrier) a)

noncomputable def MIPRE.SAT.shoupTraceGram (k : ℕ) (hk : 1 ≤ k) {n : ℕ} (v : Fin n → (shoupBinField k hk).carrier) : Matrix (Fin n) (Fin n) (ZMod 2)

The binary trace Gram matrix of any finite field-vector family.

Equations

• MIPRE.SAT.shoupTraceGram k hk v i j = (Algebra.trace (ZMod 2) (MIPRE.SAT.shoupBinField k hk).carrier) (v i * v j)

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

Construct the full trace Gram matrix of a supplied family.

Equations

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

theorem MIPRE.SAT.shoupTraceGramProg_correct (k : ℕ) (hk : 1 ≤ k) {n : ℕ} (v : Fin n → (shoupBinField k hk).carrier) : shoupTraceGramProg.toFun (Cost.unary k, List.ofFn fun (i : Fin n) => (shoupBinField k hk).toBits (v i)) = LowDegree.BinaryLinear.matrixBits (shoupTraceGram k hk v)

Every printed entry is the algebraic trace of the corresponding product.

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

A basis has a nonsingular trace Gram matrix.

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

Compute the inverse trace Gram matrix of a basis.

Equations

• MIPRE.SAT.shoupInverseGramProg = MIPRE.LowDegree.BinaryLinear.inverseMatrixProg.comp (MIPRE.Cost.PolyTimeFun.fst.pair MIPRE.SAT.shoupTraceGramProg)

theorem MIPRE.SAT.shoupInverseGramProg_correct (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) : LowDegree.BinaryLinear.mulBits k (LowDegree.BinaryLinear.matrixBits (shoupTraceGram k hk ⇑b)) (shoupInverseGramProg.toFun (Cost.unary k, List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i))) = LowDegree.BinaryLinear.identityBits k ∧ LowDegree.BinaryLinear.mulBits k (shoupInverseGramProg.toFun (Cost.unary k, List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i))) (LowDegree.BinaryLinear.matrixBits (shoupTraceGram k hk ⇑b)) = LowDegree.BinaryLinear.identityBits k