Canonical binary linear coordinates for the effective field

theorem MIPRE.LowDegree.BinaryLinear.vectorBits_vectorValue (n : ℕ) (v : Cost.BitStr) (hv : List.length v = n) : vectorBits (vectorValue n v) = v

Decoding and re-encoding a vector of the prescribed width is exact.

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

theorem MIPRE.SAT.shoupBinField_ofBits (k : ℕ) (hk : 1 ≤ k) (v : Cost.BitStr) (hv : List.length v = k) : (shoupBinField k hk).ofBits v = LowDegree.BinaryPolynomial.evalBits (shoupRoot k hk) v

Correct-width decoding in the Shoup model is evaluation at its root.

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

The canonical bit representation is also a binary linear equivalence.

Equations

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

@[simp]

theorem MIPRE.SAT.shoupCoordinateEquiv_apply (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) : (shoupCoordinateEquiv k hk) a = LowDegree.BinaryLinear.vectorValue k ((shoupBinField k hk).toBits a)

theorem MIPRE.SAT.shoupCoordinateEquiv_encoding (k : ℕ) (hk : 1 ≤ k) (a : (shoupBinField k hk).carrier) : LowDegree.BinaryLinear.vectorBits ((shoupCoordinateEquiv k hk) a) = (shoupBinField k hk).toBits a

Canonical field encodings and canonical linear coordinates coincide exactly.

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

The basis associated to the actual polynomial-time field representation.

Equations

• MIPRE.SAT.shoupPowerBasis k hk = Module.Basis.ofEquivFun (MIPRE.SAT.shoupCoordinateEquiv k hk)

theorem MIPRE.SAT.shoupPowerBasis_encoding (k : ℕ) (hk : 1 ≤ k) (j : Fin k) : (shoupBinField k hk).toBits ((shoupPowerBasis k hk) j) = LowDegree.BinaryLinear.unitBits k ↑j

Standard unit vectors encode the corresponding polynomial-basis elements.

theorem MIPRE.SAT.shoupMulProg_encoding (k : ℕ) (hk : 1 ≤ k) (a b : (shoupBinField k hk).carrier) : shoupMulProg.toFun (Cost.unary k, (shoupBinField k hk).toBits a, (shoupBinField k hk).toBits b) = (shoupBinField k hk).toBits (a * b)

Multiplication prints the canonical linear coordinates of the product.