The concrete Pauli probes of the honest QLD strategy

Low-degree evaluation followed by the verifier's field trace is exactly the binary spectral measurement of a Weyl observable. The verifier's gam is proved to equal the commutation phase of the two observables.

@[reducible, inline]

abbrev MIPRE.QLD.Honest.Register (F : Type u_2) (m : ℕ) : Type u_2

Equations

• MIPRE.QLD.Honest.Register F m = ((Fin m → Bool) → F)

noncomputable def MIPRE.QLD.Honest.basis {F : Type u_1} [Field F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (W : Bas) : Register F m → Matrix (Register F m) (Register F m) ℂ

Equations

• MIPRE.QLD.Honest.basis MIPRE.QLD.Bas.X = MIPRE.Weyl.wX
• MIPRE.QLD.Honest.basis MIPRE.QLD.Bas.Z = MIPRE.Weyl.wZ

theorem MIPRE.QLD.Honest.basis_isWeyl {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (W : Bas) : Weyl.IsWeylFamily (basis W)

noncomputable def MIPRE.QLD.Honest.pauliOp {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (W : Bas) : Register F m → Matrix (Register F m) (Register F m) ℂ

Equations

• MIPRE.QLD.Honest.pauliOp W = MIPRE.Weyl.proj (MIPRE.QLD.Honest.basis W)

theorem MIPRE.QLD.Honest.pauliOp_isPVM {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (W : Bas) : IsPVM (pauliOp W)

noncomputable def MIPRE.QLD.Honest.probeVector {F : Type u_1} [Field F] {m : ℕ} (ω : Omega F m) (W : Bas) : Register F m

Equations

• MIPRE.QLD.Honest.probeVector ω W = ω.r W • MIPRE.LowDegree.indVec (ω.pt W)

noncomputable def MIPRE.QLD.Honest.probeLabel {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (W : Bas) (h : Register F m) : ZMod 2

Equations

• MIPRE.QLD.Honest.probeLabel ω W h = MIPRE.QLD.prb ((MvPolynomial.eval (ω.pt W)) (MIPRE.LowDegree.ldEnc h)) (ω.r W)

theorem MIPRE.QLD.Honest.eval_ldEnc_dot {F : Type u_1} [Field F] {m : ℕ} (h : Register F m) (u : LIDT.Point F m) : (MvPolynomial.eval u) (LowDegree.ldEnc h) = ∑ y : Fin m → Bool, h y * LowDegree.indVec u y

theorem MIPRE.QLD.Honest.probeVector_trace {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (W : Bas) (h : Register F m) : Weyl.trDot (probeVector ω W) h = probeLabel ω W h

noncomputable def MIPRE.QLD.Honest.probeOp {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (W : Bas) : ZMod 2 → Matrix (Register F m) (Register F m) ℂ

Equations

• MIPRE.QLD.Honest.probeOp ω W = MIPRE.fibSum (MIPRE.QLD.Honest.pauliOp W) (MIPRE.QLD.Honest.probeLabel ω W)

theorem MIPRE.QLD.Honest.probeOp_isPVM {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (W : Bas) : IsPVM (probeOp ω W)

theorem MIPRE.QLD.Honest.signed_fibre {X : Type u_2} {I : Type u_3} [Fintype X] [Fintype I] [DecidableEq I] (P : X → Matrix I I ℂ) (f : X → ZMod 2) : ∑ b : ZMod 2, sgn b • fibSum P f b = ∑ x : X, sgn (f x) • P x

theorem MIPRE.QLD.Honest.probe_observable {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (W : Bas) : LCS.observableOfMeasurementSystem (probeOp ω W) = basis W (probeVector ω W)

The actual verifier probe is the binary spectral measurement of this Weyl operator.

theorem MIPRE.QLD.Honest.probeOp_isMeasurementSystem {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (W : Bas) : LCS.IsMeasurementSystem (probeOp ω W)

theorem MIPRE.QLD.Honest.probe_basis_isObservable {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (W : Bas) : LCS.IsObservable (basis W (probeVector ω W))

theorem MIPRE.QLD.Honest.probe_phase {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) : Weyl.trDot (probeVector ω Bas.X) (probeVector ω Bas.Z) = gam ω

The phase tested by the verifier is precisely the Pauli commutation phase.

theorem MIPRE.QLD.Honest.probe_basis_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (h : gam ω = 0) : Commute (basis Bas.X (probeVector ω Bas.X)) (basis Bas.Z (probeVector ω Bas.Z))

theorem MIPRE.QLD.Honest.probe_basis_anticommute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (h : gam ω ≠ 0) : basis Bas.X (probeVector ω Bas.X) * basis Bas.Z (probeVector ω Bas.Z) = -(basis Bas.Z (probeVector ω Bas.Z) * basis Bas.X (probeVector ω Bas.X))