The honest measurements for all twenty-six Pauli question types

Every measurement uses the same field register tensor one qubit. The low-degree questions read functions of a Pauli outcome; the commuting and anticommuting branches use the actual verifier phase. All answer constructors and inactive branches are explicit.

@[reducible, inline]

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

Equations

• MIPRE.QLD.Honest.Space F m = (MIPRE.QLD.Honest.Register F m × Fin 2)

def MIPRE.QLD.Honest.liftOp {F : Type u_1} {m : ℕ} (M : Matrix (Register F m) (Register F m) ℂ) : Matrix (Space F m) (Space F m) ℂ

Equations

• MIPRE.QLD.Honest.liftOp M = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1

theorem MIPRE.QLD.Honest.liftOp_isPVM {F : Type u_1} [Fintype F] [DecidableEq F] {m : ℕ} {A : Type u_2} [Fintype A] [DecidableEq A] {P : A → Matrix (Register F m) (Register F m) ℂ} (hP : IsPVM P) : IsPVM fun (a : A) => liftOp (P a)

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

Equations

• MIPRE.QLD.Honest.pauliLift W h = MIPRE.QLD.Honest.liftOp (MIPRE.QLD.Honest.pauliOp W h)

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

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

Equations

• MIPRE.QLD.Honest.probeLift ω W b = MIPRE.QLD.Honest.liftOp (MIPRE.QLD.Honest.probeOp ω W b)

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

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

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

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

noncomputable def MIPRE.QLD.Honest.lineAnswer {F : Type u_1} [Field F] {m : ℕ} (n : ℕ) (u v : LIDT.Point F m) (h : Register F m) : LIDT.LinePoly F n

The polynomial coefficient answer to a line query.

Equations

• MIPRE.QLD.Honest.lineAnswer n u v h i = (MIPRE.LowDegree.lineRestrict u v (MIPRE.LowDegree.ldEnc h)).coeff ↑i

def MIPRE.QLD.Honest.pairLabel (p : ZMod 2 × ZMod 2) : Bas → ZMod 2

Equations

• MIPRE.QLD.Honest.pairLabel p MIPRE.QLD.Bas.X = p.1
• MIPRE.QLD.Honest.pairLabel p MIPRE.QLD.Bas.Z = p.2

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

Equations

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

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

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

Equations

• MIPRE.QLD.Honest.pairBBranch ω W = if MIPRE.QLD.gam ω = 0 then MIPRE.QLD.Honest.probeLift ω W else MIPRE.Introspection.readout fun (x : MIPRE.QLD.Honest.Space F m) => 0

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

noncomputable def MIPRE.QLD.Honest.constraintBranch {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (c : Fin LCS.MagicSquare.layout.r) : (Fin 3 → ZMod 2) → Matrix (Space F m) (Space F m) ℂ

Equations

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

theorem MIPRE.QLD.Honest.constraintBranch_isPVM {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (c : Fin LCS.MagicSquare.layout.r) : IsPVM (constraintBranch ω c)

noncomputable def MIPRE.QLD.Honest.variableBranch {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (j : Fin LCS.MagicSquare.layout.s) : ZMod 2 → Matrix (Space F m) (Space F m) ℂ

Equations

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

theorem MIPRE.QLD.Honest.variableBranch_isPVM {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (j : Fin LCS.MagicSquare.layout.s) : IsPVM (variableBranch ω j)

noncomputable def MIPRE.QLD.Honest.answerOp {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) : Question F m → Answer F m d → Matrix (Space F m) (Space F m) ℂ

All twenty-six measurements on the actual question and answer alphabets.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.QLD.Honest.answerOp hm (MIPRE.QLD.Question.pauli W) = MIPRE.fibSum (MIPRE.QLD.Honest.pauliLift W) MIPRE.QLD.Answer.pauliAns
• MIPRE.QLD.Honest.answerOp hm (MIPRE.QLD.Question.pairB W ω) = MIPRE.fibSum (MIPRE.QLD.Honest.pairBBranch ω W) MIPRE.QLD.Answer.bit
• MIPRE.QLD.Honest.answerOp hm (MIPRE.QLD.Question.pair ω) = MIPRE.fibSum (MIPRE.QLD.Honest.pairBranch ω) MIPRE.QLD.Answer.bitPair
• MIPRE.QLD.Honest.answerOp hm (MIPRE.QLD.Question.con c ω) = MIPRE.fibSum (MIPRE.QLD.Honest.constraintBranch ω c) MIPRE.QLD.Answer.bitTriple
• MIPRE.QLD.Honest.answerOp hm (MIPRE.QLD.Question.var j ω) = MIPRE.fibSum (MIPRE.QLD.Honest.variableBranch ω j) MIPRE.QLD.Answer.bit

theorem MIPRE.QLD.Honest.answerOp_isPVM {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (q : Question F m) : IsPVM (answerOp hm q)

theorem MIPRE.QLD.Honest.fibre_format_zero {F : Type u_1} [DecidableEq F] {m d : ℕ} {X : Type u_2} [Fintype X] (P : X → Matrix (Space F m) (Space F m) ℂ) (f : X → Answer F m d) (q : Question F m) (hf : ∀ (x : X), q.fmtOk (f x) = true) (a : Answer F m d) (ha : q.fmtOk a = false) : fibSum P f a = 0

theorem MIPRE.QLD.Honest.answerOp_format_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (q : Question F m) (a : Answer F m d) (ha : q.fmtOk a = false) : answerOp hm q a = 0

Every malformed answer has zero effect, for every question.

theorem MIPRE.QLD.Honest.answerOp_pauli {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (W : Bas) (h : Register F m) : answerOp hm (Question.pauli W) (Answer.pauliAns h) = pauliLift W h

theorem MIPRE.QLD.Honest.variableBranch_X {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (h : gam ω ≠ 0) (b : ZMod 2) : variableBranch ω (LCS.MagicSquare.v 0 variableBranch_X._proof_1) b = probeLift ω Bas.X b

theorem MIPRE.QLD.Honest.variableBranch_Z {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (h : gam ω ≠ 0) (b : ZMod 2) : variableBranch ω (LCS.MagicSquare.v 4 variableBranch_Z._proof_1) b = probeLift ω Bas.Z b