Exact row and binary encodings for the executable Pauli queries

theorem MIPRE.QLD.PauliCL.packRows_fieldEncoding_getD {k m : ℕ} (E : SAT.BinField k) (x : Coord m → E.carrier) (c : Coord m) : (Introspection.PauliStageProgram.packRows.toFun (fieldEncoding E x)).getD ↑((coordNumbering m) c) [] = E.toBits (x c)

theorem MIPRE.QLD.PauliCL.packRows_fieldEncoding {k m : ℕ} (E : SAT.BinField k) (x : Coord m → E.carrier) : Introspection.PauliStageProgram.packRows.toFun (fieldEncoding E x) = numberedRows E x

theorem MIPRE.QLD.PauliCL.unpackRows_numberedRows {k m : ℕ} (E : SAT.BinField k) (x : Coord m → E.carrier) : Introspection.PauliStageProgram.unpackRows.toFun (Cost.unary m, numberedRows E x) = fieldEncoding E x

theorem MIPRE.QLD.PauliCL.rowInput_correct (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (T : Ty) (r : ℕ) (u x : Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) : Introspection.PauliStageProgram.rowInput.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), programTag T, r, numberedRows (SAT.shoupBinField k hk) u, numberedRows (SAT.shoupBinField k hk) x) = stageInput k hk j T u x

theorem MIPRE.QLD.PauliCL.linearRows_correct (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) (T : Ty) (r : ℕ) (hr1 : 1 ≤ r) (hr3 : r ≤ 3) (u x : Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) : Introspection.PauliStageProgram.linearRows.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), programTag T, r, numberedRows (SAT.shoupBinField k hk) u, numberedRows (SAT.shoupBinField k hk) x) = numberedRows (SAT.shoupBinField k hk) (((ExplicitSeed.presentation (Introspection.SeedProgram.selector (SAT.shoupBinField k hk) j hj) T).mapOfPrefix (r - 1) u) x)

theorem MIPRE.QLD.PauliCL.binaryInput_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (T : Ty) (r : ℕ) (u x : Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) : Introspection.PauliStageProgram.binaryInput.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), programTag T, r, CL.toBits ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) u), CL.toBits ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) x)) = ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), programTag T, r, numberedRows (SAT.shoupBinField k hk) u, numberedRows (SAT.shoupBinField k hk) x)

theorem MIPRE.QLD.PauliCL.binaryPresentation_mapOfPrefix {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m k : ℕ} [NeZero m] (χ : F → Fin m) (b : Module.Basis (Fin k) (ZMod 2) F) (T : Ty) (r : ℕ) (u x : Coord m → F) : ((ExplicitSeed.binaryPresentation χ b T).mapOfPrefix r ((binaryVectorEquiv b) u)) ((binaryVectorEquiv b) x) = (binaryVectorEquiv b) (((ExplicitSeed.presentation χ T).mapOfPrefix r u) x)

theorem MIPRE.QLD.PauliCL.linearBits_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (hj : j ≤ k) (T : Ty) (r : ℕ) (hr1 : 1 ≤ r) (hr3 : r ≤ 3) (u x : Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) : Introspection.PauliStageProgram.linearBits.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), programTag T, r, CL.toBits ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) u), CL.toBits ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) x)) = CL.toBits (((ExplicitSeed.binaryPresentation (Introspection.SeedProgram.selector (SAT.shoupBinField k hk) j hj) (SAT.shoupSelfDualNormalBasis k hk hodd) T).mapOfPrefix (r - 1) ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) u)) ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) x))

theorem MIPRE.QLD.PauliCL.marginalRows_correct (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) (T : Ty) (r : ℕ) (hr1 : 1 ≤ r) (hr3 : r ≤ 3) (u x : Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) : Introspection.PauliStageProgram.marginalRows.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), programTag T, r, numberedRows (SAT.shoupBinField k hk) u, numberedRows (SAT.shoupBinField k hk) x) = numberedRows (SAT.shoupBinField k hk) ((CL.CLFun.truncate r (ExplicitSeed.presentation (Introspection.SeedProgram.selector (SAT.shoupBinField k hk) j hj) T)).eval x)

theorem MIPRE.QLD.PauliCL.binaryPresentation_truncate {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m k : ℕ} [NeZero m] (χ : F → Fin m) (b : Module.Basis (Fin k) (ZMod 2) F) (T : Ty) (r : ℕ) (x : Coord m → F) : (CL.CLFun.truncate r (ExplicitSeed.binaryPresentation χ b T)).eval ((binaryVectorEquiv b) x) = (binaryVectorEquiv b) ((CL.CLFun.truncate r (ExplicitSeed.presentation χ T)).eval x)

theorem MIPRE.QLD.PauliCL.marginalBits_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (hj : j ≤ k) (T : Ty) (r : ℕ) (hr1 : 1 ≤ r) (hr3 : r ≤ 3) (u x : Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) : Introspection.PauliStageProgram.marginalBits.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), programTag T, r, CL.toBits ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) u), CL.toBits ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) x)) = CL.toBits ((CL.CLFun.truncate r (ExplicitSeed.binaryPresentation (Introspection.SeedProgram.selector (SAT.shoupBinField k hk) j hj) (SAT.shoupSelfDualNormalBasis k hk hodd) T)).eval ((binaryVectorEquiv (SAT.shoupSelfDualNormalBasis k hk hodd)) x))