Correctness of the uniform Pauli decision program

noncomputable def MIPRE.QLD.PauliBooleanProgram.encodedInput {k m : ℕ} (E : SAT.BinField k) (j : ℕ) (T U : Ty) (x y : PauliCL.Coord m → E.carrier) (a b : Answer E.carrier m 1) : Input

Equations

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

@[simp]

theorem MIPRE.QLD.PauliBooleanProgram.explicitDecode_ty {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (π : F ≃ F) (T : Ty) (x : PauliCL.Coord m → F) : (PauliCL.ExplicitSeed.decode π T x).ty = T

theorem MIPRE.QLD.PauliBooleanProgram.parser_for_type {k m : ℕ} (E : SAT.BinField k) (hk : 0 < k) (π : E.carrier ≃ E.carrier) (T : Ty) (x : PauliCL.Coord m → E.carrier) (a : Answer E.carrier m 1) (ha : (PauliCL.ExplicitSeed.decode π T x).fmtOk a = true) : PauliAnswerProgram.parser.toFun (T, Cost.unary m, Cost.unary k, Cost.unary 1, PauliAnswerProgram.answerBits E a) = (true, PauliAnswerProgram.answerRows E a)

@[simp]

theorem MIPRE.QLD.PauliBooleanProgram.route_encodedInput {k m : ℕ} (E : SAT.BinField k) (j : ℕ) (T U : Ty) (x y : PauliCL.Coord m → E.carrier) (a b : Answer E.carrier m 1) : route.toFun (encodedInput E j T U x y a b) = PauliBranchProgram.route T U

theorem MIPRE.QLD.PauliBooleanProgram.leftParser_encodedInput {k m : ℕ} (E : SAT.BinField k) (hk : 0 < k) (j : ℕ) (π : E.carrier ≃ E.carrier) (T U : Ty) (x y : PauliCL.Coord m → E.carrier) (a b : Answer E.carrier m 1) (ha : (PauliCL.ExplicitSeed.decode π T x).fmtOk a = true) (hb : (PauliCL.ExplicitSeed.decode π U y).fmtOk b = true) : (leftParser.toFun (encodedInput E j T U x y a b)).1 = true

theorem MIPRE.QLD.PauliBooleanProgram.rightParser_encodedInput {k m : ℕ} (E : SAT.BinField k) (hk : 0 < k) (j : ℕ) (π : E.carrier ≃ E.carrier) (T U : Ty) (x y : PauliCL.Coord m → E.carrier) (a b : Answer E.carrier m 1) (ha : (PauliCL.ExplicitSeed.decode π T x).fmtOk a = true) (hb : (PauliCL.ExplicitSeed.decode π U y).fmtOk b = true) : (rightParser.toFun (encodedInput E j T U x y a b)).1 = true

theorem MIPRE.QLD.PauliBooleanProgram.program_of_formatted {k m : ℕ} (E : SAT.BinField k) (hk : 0 < k) (j : ℕ) (π : E.carrier ≃ E.carrier) (T U : Ty) (x y : PauliCL.Coord m → E.carrier) (a b : Answer E.carrier m 1) (ha : (PauliCL.ExplicitSeed.decode π T x).fmtOk a = true) (hb : (PauliCL.ExplicitSeed.decode π U y).fmtOk b = true) : have input := encodedInput E j T U x y a b; program.toFun input = [consistency.toFun input, axisCheck.toFun input, diagonalCheck.toFun input, tableCheck.toFun input, pairCheck.toFun input, probeCheck.toFun input, magicCheck.toFun input, magicProbeCheck.toFun input].getD (PauliBranchProgram.route T U).1 true

theorem MIPRE.QLD.PauliBooleanProgram.explicitDecode_format_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} (π : F ≃ F) (T : Ty) (x y : PauliCL.Coord m → F) (a : Answer F m d) : (PauliCL.ExplicitSeed.decode π T x).fmtOk a = (PauliCL.ExplicitSeed.decode π T y).fmtOk a

theorem MIPRE.QLD.PauliBooleanProgram.program_same_type {k m : ℕ} (E : SAT.BinField k) (hk : 0 < k) (j : ℕ) (π : E.carrier ≃ E.carrier) (T : Ty) (x y : PauliCL.Coord m → E.carrier) (a b : Answer E.carrier m 1) (ha : (PauliCL.ExplicitSeed.decode π T x).fmtOk a = true) (hb : (PauliCL.ExplicitSeed.decode π T y).fmtOk b = true) : program.toFun (encodedInput E j T T x y a b) = decide (a = b)

theorem MIPRE.QLD.PauliBooleanProgram.seed_fieldEncoding {k m : ℕ} (E : SAT.BinField k) (x : PauliCL.Coord m → E.carrier) : Introspection.PauliStageProgram.seed.toFun (PauliCL.fieldEncoding E x) = E.toBits (x PauliCL.Coord.seed)

theorem MIPRE.QLD.PauliBooleanProgram.direction_fieldEncoding {k m : ℕ} (E : SAT.BinField k) (x : PauliCL.Coord m → E.carrier) : Introspection.PauliStageProgram.direction.toFun (PauliCL.fieldEncoding E x) = E.vecBits fun (i : Fin m) => x (PauliCL.Coord.direction i)

theorem MIPRE.QLD.PauliBooleanProgram.program_axis (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (W : Bas) (x y : PauliCL.Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier) (f : LIDT.LinePoly (SAT.shoupBinField k hk).carrier 1) : program.toFun (encodedInput (SAT.shoupBinField k hk) j (Ty.point W) (Ty.aline W) x y (Answer.val a) (Answer.apoly f)) = lowDeg (fun (i : Fin (2 ^ j)) => y (PauliCL.Coord.point W i)) (Pi.single (LIDT.CL.chi hm ((PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) (y PauliCL.Coord.seed))) 1) (fun (i : Fin (2 ^ j)) => x (PauliCL.Coord.point W i)) f a

theorem MIPRE.QLD.PauliBooleanProgram.program_diagonal (k : ℕ) (hk : 1 ≤ k) (j m : ℕ) (W : Bas) (x y : PauliCL.Coord m → (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier) (f : LIDT.LinePoly (SAT.shoupBinField k hk).carrier (m * 1)) : program.toFun (encodedInput (SAT.shoupBinField k hk) j (Ty.point W) (Ty.dline W) x y (Answer.val a) (Answer.dpoly f)) = lowDeg (fun (i : Fin m) => y (PauliCL.Coord.point W i)) (fun (i : Fin m) => y (PauliCL.Coord.direction i)) (fun (i : Fin m) => x (PauliCL.Coord.point W i)) f a

theorem MIPRE.QLD.PauliBooleanProgram.program_table (k : ℕ) (hk : 1 ≤ k) (j m : ℕ) (W : Bas) (x y : PauliCL.Coord m → (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier) (h : (Fin m → Bool) → (SAT.shoupBinField k hk).carrier) : program.toFun (encodedInput (SAT.shoupBinField k hk) j (Ty.point W) (Ty.pauli W) x y (Answer.val a) (Answer.pauliAns h)) = decide ((MvPolynomial.eval fun (i : Fin m) => x (PauliCL.Coord.point W i)) (LowDegree.ldEnc h) = a)

theorem MIPRE.QLD.PauliBooleanProgram.bit_ne_zero (b : ZMod 2) : LowDegree.BinaryLinear.bit b = decide (b ≠ 0)

theorem MIPRE.QLD.PauliBooleanProgram.boolEq_bits (a b : ZMod 2) : boolEq.toFun (LowDegree.BinaryLinear.bit a, LowDegree.BinaryLinear.bit b) = decide (a = b)

theorem MIPRE.QLD.PauliBooleanProgram.program_pair (k : ℕ) (hk : 1 ≤ k) (j m : ℕ) (W : Bas) (x y : PauliCL.Coord m → (SAT.shoupBinField k hk).carrier) (a : ZMod 2) (b : Bas → ZMod 2) : program.toFun (encodedInput (SAT.shoupBinField k hk) j (Ty.pairB W) Ty.pair x y (Answer.bit a) (Answer.bitPair b)) = (decide (gam (PauliCL.vectorContent y).omega ≠ 0) || decide (a = b W))

theorem MIPRE.QLD.PauliBooleanProgram.program_probe (k : ℕ) (hk : 1 ≤ k) (j m : ℕ) (W : Bas) (x y : PauliCL.Coord m → (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier) (b : ZMod 2) : program.toFun (encodedInput (SAT.shoupBinField k hk) j (Ty.point W) (Ty.pairB W) x y (Answer.val a) (Answer.bit b)) = (decide (gam (PauliCL.vectorContent y).omega ≠ 0) || decide (prb a (y (PauliCL.Coord.scalar W)) = b))

theorem MIPRE.QLD.PauliBooleanProgram.boolNot_bit (a : ZMod 2) : boolNot.toFun (LowDegree.BinaryLinear.bit a) = decide (a = 0)

theorem MIPRE.QLD.PauliBooleanProgram.bitAt_ofFn {n : ℕ} (a : Fin n → ZMod 2) (i : Fin n) : bitAt.toFun (↑i, List.ofFn fun (j : Fin n) => [LowDegree.BinaryLinear.bit (a j)]) = LowDegree.BinaryLinear.bit (a i)

theorem MIPRE.QLD.PauliBooleanProgram.parity_bits (a : Fin 3 → ZMod 2) : parityProg.toFun (LowDegree.BinaryLinear.bit (a 0), LowDegree.BinaryLinear.bit (a 1), LowDegree.BinaryLinear.bit (a 2)) = LowDegree.BinaryLinear.bit (∑ i : Fin 3, a i)

theorem MIPRE.QLD.PauliBooleanProgram.program_magic (k : ℕ) (hk : 1 ≤ k) (j m : ℕ) (i : Fin LCS.MagicSquare.layout.r) (v : Fin LCS.MagicSquare.layout.s) (x y : PauliCL.Coord m → (SAT.shoupBinField k hk).carrier) (a : Fin 3 → ZMod 2) (b : ZMod 2) : program.toFun (encodedInput (SAT.shoupBinField k hk) j (Ty.con i) (Ty.var v) x y (Answer.bitTriple a) (Answer.bit b)) = (decide (gam (PauliCL.vectorContent y).omega = 0) || decide (v ∈ LCS.MagicSquare.layout.V i) && decide (∑ z : Fin 3, a z = LCS.MagicSquare.game.b i) && decide (a (LCS.MagicSquare.cellIdx i v) = b))

theorem MIPRE.QLD.PauliBooleanProgram.program_magicProbe (k : ℕ) (hk : 1 ≤ k) (j m : ℕ) (W : Bas) (v : Fin LCS.MagicSquare.layout.s) (x y : PauliCL.Coord m → (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier) (b : ZMod 2) : program.toFun (encodedInput (SAT.shoupBinField k hk) j (Ty.point W) (Ty.var v) x y (Answer.val a) (Answer.bit b)) = (decide (gam (PauliCL.vectorContent y).omega = 0) || probeEligible (Ty.point W, Ty.var v) && decide (prb a (y (PauliCL.Coord.scalar W)) = b))