Documentation

MIPRE.Background.Introspection.BinaryAnchors

The actual QLD Pauli answers pass the introspection anchor tests #

noncomputable def MIPRE.Introspection.BinaryComplete.seedAnswer {F : Type u_1} {A : Type u_2} [Field F] [Algebra (ZMod 2) F] {m d t : ℕ} (β : Module.Basis (Fin t) (ZMod 2) F) :

Answer F A m t d → ParsedAnswer (Seed m t) A (Seed m t)

Equations

Instances For

theorem MIPRE.Introspection.BinaryComplete.auxOp_seedAnswer {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (β : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (q : Honest.AuxQuestion ℓ) (a : Answer F A m t d) :

Honest.auxOp L D R hL q a = Honest.auxOp L D R hL q (seedAnswer β a)

theorem MIPRE.Introspection.BinaryComplete.pauliOp_zero_or_seed {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (β : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (W : QLD.Bas) (a : Answer F A m t d) :

pauliOp β L D R hm (QLD.Question.pauli W) a = 0 ∨ ∃ (x : (Fin m → Bool) → F), a = ParsedAnswer.pauli (QLD.Answer.pauliAns x)

theorem MIPRE.Introspection.BinaryComplete.anchor_check {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (β : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → A → A → Bool) (p : QLD.Ty) (q : Honest.AuxQuestion ℓ) (DP : QLD.Ty → QLD.Ty → QLD.Answer F m d → QLD.Answer F m d → Bool) (x : QLD.Honest.Register F m) (b : Answer F A m t d) :

TypedPredicate.check L (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (project β) D DP (Sum.inl p) (Sum.inr q) (ParsedAnswer.pauli (QLD.Answer.pauliAns x)) b = TypedPredicate.check L (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) id D (fun (x x_1 : QLD.Ty) (x_2 x_3 : Coord m t → ZMod 2) => true) (Sum.inl p) (Sum.inr q) (ParsedAnswer.pauli ((Weyl.binEquiv β) x)) (seedAnswer β b)

theorem MIPRE.Introspection.BinaryComplete.anchor_check_swap {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (β : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → A → A → Bool) (p : QLD.Ty) (q : Honest.AuxQuestion ℓ) (DP : QLD.Ty → QLD.Ty → QLD.Answer F m d → QLD.Answer F m d → Bool) (a b : Answer F A m t d) :

TypedPredicate.check L (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (project β) D DP (Sum.inl p) (Sum.inr q) a b = TypedPredicate.check L (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (project β) D DP (Sum.inr q) (Sum.inl p) b a

theorem MIPRE.Introspection.BinaryComplete.anchor_X_commute {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (β : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hβ : LowDegree.IsSelfDualBasis β) (hm : m ∣ Fintype.card F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (w : Bool) (k : Fin ℓ) (hk : ↑k = 0) (a b : Answer F A m t d) :

Commute (pauliOp β L D R hm (QLD.Question.pauli QLD.Bas.X) a) (auxOp L D R hL (AuxType.hide k, w) b)

theorem MIPRE.Introspection.BinaryComplete.anchor_Z_commute {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (β : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hβ : LowDegree.IsSelfDualBasis β) (hm : m ∣ Fintype.card F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (w : Bool) (a b : Answer F A m t d) :

Commute (pauliOp β L D R hm (QLD.Question.pauli QLD.Bas.Z) a) (auxOp L D R hL (AuxType.sample , w) b)

theorem MIPRE.Introspection.BinaryComplete.anchor_X_reject {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (β : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hβ : LowDegree.IsSelfDualBasis β) (hm : m ∣ Fintype.card F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (w : Bool) (k : Fin ℓ) (hk : ↑k = 0) (DP : QLD.Ty → QLD.Ty → QLD.Answer F m d → QLD.Answer F m d → Bool) (a b : Answer F A m t d) (hr : TypedPredicate.check L (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (project β) D DP (Sum.inl (QLD.Ty.pauli QLD.Bas.X)) (Sum.inr (AuxType.hide k, w)) a b = false) :

pauliOp β L D R hm (QLD.Question.pauli QLD.Bas.X) a * auxOp L D R hL (AuxType.hide k, w) b = 0

theorem MIPRE.Introspection.BinaryComplete.anchor_Z_reject {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (β : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hβ : LowDegree.IsSelfDualBasis β) (hm : m ∣ Fintype.card F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (w : Bool) (DP : QLD.Ty → QLD.Ty → QLD.Answer F m d → QLD.Answer F m d → Bool) (a b : Answer F A m t d) (hr : TypedPredicate.check L (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (project β) D DP (Sum.inl (QLD.Ty.pauli QLD.Bas.Z)) (Sum.inr (AuxType.sample , w)) a b = false) :

pauliOp β L D R hm (QLD.Question.pauli QLD.Bas.Z) a * auxOp L D R hL (AuxType.sample , w) b = 0