The sampler's actual numbered binary field blocks

The fixed block programs convert exactly between the numbered binary vector used by binaryPresentation and canonical Shoup field rows in the fixed order uX, uZ, seed, direction, rX, rZ. The field basis is the effective self-dual normal basis, not the computational polynomial basis.

def MIPRE.QLD.PauliCL.numberedRows {k m : ℕ} (E : SAT.BinField k) (x : Coord m → E.carrier) : List Cost.BitStr

Canonical field rows in the explicit ambient coordinate order.

Equations

• MIPRE.QLD.PauliCL.numberedRows E x = List.ofFn fun (i : Fin (3 * m + 3)) => E.toBits (x ((MIPRE.QLD.PauliCL.coordNumbering m).symm i))

theorem MIPRE.QLD.PauliCL.numberedRows_length {k m : ℕ} (E : SAT.BinField k) (x : Coord m → E.carrier) : (numberedRows E x).length = 3 * m + 3

theorem MIPRE.QLD.PauliCL.numberedRows_getD {k m : ℕ} (E : SAT.BinField k) (x : Coord m → E.carrier) (c : Coord m) : (numberedRows E x).getD ↑((coordNumbering m) c) [] = E.toBits (x c)

theorem MIPRE.QLD.PauliCL.numberedRows_eq_vecBits {k m : ℕ} (E : SAT.BinField k) (x : Coord m → E.carrier) : numberedRows E x = E.vecBits fun (i : Fin (3 * m + 3)) => x ((coordNumbering m).symm i)

theorem MIPRE.QLD.PauliCL.binaryVectorEquiv_bits {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m k : ℕ} [NeZero m] (b : Module.Basis (Fin k) (ZMod 2) F) (x : Coord m → F) : CL.toBits ((binaryVectorEquiv b) x) = (List.ofFn fun (i : Fin (3 * m + 3)) => LowDegree.BinaryLinear.vectorBits (b.equivFun (x ((coordNumbering m).symm i)))).flatten

Exact list order for an arbitrary binary basis: coordinate-major, followed by the basis bits of that coordinate.

theorem MIPRE.QLD.PauliCL.encodeBlocksProg_numberedRows (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) {m : ℕ} [NeZero m] (x : Coord m → (SAT.shoupBinField k hk).carrier) : Introspection.BinaryBlock.encodeBlocksProg.toFun (Cost.unary k, numberedRows (SAT.shoupBinField k hk) x) = CL.toBits ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) x)

The executable encoder produces the exact numbered CL bit vector.

theorem MIPRE.QLD.PauliCL.decodeBlocksProg_binaryVector (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) {m : ℕ} [NeZero m] (x : Coord m → (SAT.shoupBinField k hk).carrier) : Introspection.BinaryBlock.decodeBlocksProg.toFun (Cost.unary (3 * m + 3), Cost.unary k, CL.toBits ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) x)) = numberedRows (SAT.shoupBinField k hk) x

The executable decoder returns the exact canonical field row at each numbered coordinate of the self-dual downsized vector.

theorem MIPRE.QLD.PauliCL.decodeBlocksProg_ofBits (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) {m : ℕ} [NeZero m] (z : Cost.BitStr) (hz : List.length z = (3 * m + 3) * k) : Introspection.BinaryBlock.decodeBlocksProg.toFun (Cost.unary (3 * m + 3), Cost.unary k, z) = numberedRows (SAT.shoupBinField k hk) ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)).symm (CL.ofBits ((3 * m + 3) * k) z))

A full-length raw CL bit string is interpreted by the actual inverse binary coordinate map; no assumption that its bits are polynomial coordinates is made.