Exact arithmetic programs for the Pauli decision rules

These bridges identify the uniform field programs with the existing game predicates. In particular the line test retains geometric membership, the full-answer test evaluates at arbitrary field points, and the commutation bit uses the entire tuple of the endpoint prescribed by the rule.

theorem MIPRE.QLD.PauliArithmeticProgram.parameter_eq_lineParam {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (origin direction point : Fin m → F) : Introspection.FieldLineCheck.parameter origin direction point = LIDT.CL.lineParam origin direction point

theorem MIPRE.QLD.PauliArithmeticProgram.lineCheckProg_eq_lowDeg (k : ℕ) (hk : 1 ≤ k) {m n : ℕ} (origin direction point : Fin m → (SAT.shoupBinField k hk).carrier) (f : LIDT.LinePoly (SAT.shoupBinField k hk).carrier n) (a : (SAT.shoupBinField k hk).carrier) : Introspection.FieldLineCheck.lineCheckProg.toFun ((Cost.unary k, (SAT.shoupBinField k hk).vecBits origin, (SAT.shoupBinField k hk).vecBits direction, (SAT.shoupBinField k hk).vecBits point), (SAT.shoupBinField k hk).vecBits f, (SAT.shoupBinField k hk).toBits a) = lowDeg origin direction point f a

The executable coefficient/membership check is exactly the Pauli line rule.

noncomputable def MIPRE.QLD.PauliArithmeticProgram.answerRows {k m : ℕ} (E : SAT.BinField k) (h : (Fin m → Bool) → E.carrier) : List Cost.BitStr

Canonical full Pauli rows follow the repository's binary cube order.

Equations

• MIPRE.QLD.PauliArithmeticProgram.answerRows E h = E.vecBits fun (i : Fin (2 ^ m)) => h ((MIPRE.Introspection.FieldTableProgram.cubeEnumeration m).symm i)

noncomputable def MIPRE.QLD.PauliArithmeticProgram.fullAnswerCheckProg : Cost.PolyTimeFun ((Cost.Unary × List Cost.BitStr × List Cost.BitStr) × Cost.BitStr) Bool

Width, queried point, full answer rows, and claimed point value.

Equations

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

theorem MIPRE.QLD.PauliArithmeticProgram.fullAnswerCheckProg_correct (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (point : Fin m → (SAT.shoupBinField k hk).carrier) (h : (Fin m → Bool) → (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier) : fullAnswerCheckProg.toFun ((Cost.unary k, (SAT.shoupBinField k hk).vecBits point, answerRows (SAT.shoupBinField k hk) h), (SAT.shoupBinField k hk).toBits a) = decide ((MvPolynomial.eval point) (LowDegree.ldEnc h) = a)

theorem MIPRE.QLD.PauliArithmeticProgram.probeProg_eq_prb (k : ℕ) (hk : 1 ≤ k) (a r : (SAT.shoupBinField k hk).carrier) : Introspection.FieldGammaProgram.probeProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).toBits a, (SAT.shoupBinField k hk).toBits r) = LowDegree.BinaryLinear.bit (prb a r)

The trace probe used by rules five and seven.

theorem MIPRE.QLD.PauliArithmeticProgram.gammaProg_eq_gam (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (ω : Omega (SAT.shoupBinField k hk).carrier m) : Introspection.FieldGammaProgram.gammaProg.toFun (Cost.unary k, List.ofFn fun (i : Fin m) => ((SAT.shoupBinField k hk).toBits (ω.uX i), (SAT.shoupBinField k hk).toBits (ω.uZ i)), (SAT.shoupBinField k hk).toBits ω.rX, (SAT.shoupBinField k hk).toBits ω.rZ) = LowDegree.BinaryLinear.bit (gam ω)

The trace commutation bit used by rules four through seven.