Documentation

MIPRE.Background.Introspection.HonestPauliEdges

The commuting and Magic Square edges of the honest Pauli strategy #

source
theorem MIPRE.QLD.Honest.pvm_commute {I : Type u_2} {X : Type u_3} [Fintype I] [DecidableEq I] [Fintype X] {P : X → Matrix I I ℂ} (hP : IsPVM P) (x y : X) :
Commute (P x) (P y)
source
theorem MIPRE.QLD.Honest.answerOp_point_pairB_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (ω : Omega F m) (W : Bas) (a b : Answer F m d) :
Commute (answerOp hm (Question.point W (ω.pt W)) a) (answerOp hm (Question.pairB W ω) b)
source
theorem MIPRE.QLD.Honest.answerOp_point_pairB_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (ω : Omega F m) (W : Bas) (a b : Answer F m d) (hr : accepts hm (Question.point W (ω.pt W)) (Question.pairB W ω) a b = false) :
answerOp hm (Question.point W (ω.pt W)) a * answerOp hm (Question.pairB W ω) b = 0
source
def MIPRE.QLD.Honest.distinguished :
Bas → Fin LCS.MagicSquare.layout.s

The cells used to anchor the two Pauli probes.

Equations
Instances For
    source
    theorem MIPRE.QLD.Honest.variableBranch_distinguished {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (h : gam ω ≠ 0) (W : Bas) :
    variableBranch ω (distinguished W) = probeLift ω W
    source
    theorem MIPRE.QLD.Honest.answerOp_point_var_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (ω : Omega F m) (W : Bas) (a b : Answer F m d) :
    Commute (answerOp hm (Question.point W (ω.pt W)) a) (answerOp hm (Question.var (distinguished W) ω) b)
    source
    theorem MIPRE.QLD.Honest.answerOp_point_var_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (ω : Omega F m) (W : Bas) (a b : Answer F m d) (hr : accepts hm (Question.point W (ω.pt W)) (Question.var (distinguished W) ω) a b = false) :
    answerOp hm (Question.point W (ω.pt W)) a * answerOp hm (Question.var (distinguished W) ω) b = 0
    source
    theorem MIPRE.QLD.Honest.answerOp_con_var_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (ω : Omega F m) (c : Fin LCS.MagicSquare.layout.r) (j : Fin LCS.MagicSquare.layout.s) (hj : j ∈ LCS.MagicSquare.layout.V c) (a b : Answer F m d) :
    Commute (answerOp hm (Question.con c ω) a) (answerOp hm (Question.var j ω) b)
    source
    theorem MIPRE.QLD.Honest.answerOp_con_var_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (ω : Omega F m) (c : Fin LCS.MagicSquare.layout.r) (j : Fin LCS.MagicSquare.layout.s) (hj : j ∈ LCS.MagicSquare.layout.V c) (a b : Answer F m d) (hr : accepts hm (Question.con c ω) (Question.var j ω) a b = false) :
    answerOp hm (Question.con c ω) a * answerOp hm (Question.var j ω) b = 0
    source
    theorem MIPRE.QLD.Honest.probe_joint_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (h : gam ω = 0) (W : Bas) (b : ZMod 2) (p : ZMod 2 × ZMod 2) :
    Commute (probeLift ω W b) (probeLift ω Bas.X p.1 * probeLift ω Bas.Z p.2)
    source
    theorem MIPRE.QLD.Honest.probe_joint_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (h : gam ω = 0) (W : Bas) (b : ZMod 2) (p : ZMod 2 × ZMod 2) (hb : b ≠ pairLabel p W) :
    probeLift ω W b * (probeLift ω Bas.X p.1 * probeLift ω Bas.Z p.2) = 0
    source
    theorem MIPRE.QLD.Honest.answerOp_pairB_pair_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (ω : Omega F m) (W : Bas) (a b : Answer F m d) :
    Commute (answerOp hm (Question.pairB W ω) a) (answerOp hm (Question.pair ω) b)
    source
    theorem MIPRE.QLD.Honest.answerOp_pairB_pair_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (ω : Omega F m) (W : Bas) (a b : Answer F m d) (hr : accepts hm (Question.pairB W ω) (Question.pair ω) a b = false) :
    answerOp hm (Question.pairB W ω) a * answerOp hm (Question.pair ω) b = 0