The actual QLD Pauli answers pass the introspection anchor tests #
def
MIPRE.Introspection.Complete.seedAnswer
{F : Type u_1}
{A : Type u_2}
[Field F]
{m d : ℕ}
:
Answer F A m d → ParsedAnswer (Seed F m) A (Seed F m)
Equations
- MIPRE.Introspection.Complete.seedAnswer (MIPRE.Introspection.ParsedAnswer.pauli a) = MIPRE.Introspection.ParsedAnswer.pauli (MIPRE.Introspection.Complete.project a)
- MIPRE.Introspection.Complete.seedAnswer (MIPRE.Introspection.ParsedAnswer.pair y a) = MIPRE.Introspection.ParsedAnswer.pair y a
- MIPRE.Introspection.Complete.seedAnswer (MIPRE.Introspection.ParsedAnswer.read y yp a) = MIPRE.Introspection.ParsedAnswer.read y yp a
- MIPRE.Introspection.Complete.seedAnswer (MIPRE.Introspection.ParsedAnswer.hide y yp x_1) = MIPRE.Introspection.ParsedAnswer.hide y yp x_1
Instances For
theorem
MIPRE.Introspection.Complete.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 ℓ : ℕ}
[NeZero m]
(L : Bool → CL.CLFun F (Fin m → Bool) ℓ)
(D : Seed F m → Seed F m → 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 d)
:
theorem
MIPRE.Introspection.Complete.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 ℓ : ℕ}
[NeZero m]
(L : Bool → CL.CLFun F (Fin m → Bool) ℓ)
(D : Seed F m → Seed F m → A → A → Bool)
(R : SyncStrategy (Honest.sourceGame L D).doubled)
(hm : m ∣ Fintype.card F)
(W : QLD.Bas)
(a : Answer F A m 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.Complete.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 ℓ : ℕ}
[NeZero m]
(L : Bool → CL.CLFun F (Fin m → Bool) ℓ)
(D : Seed F m → Seed F m → 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 : Seed F m)
(b : Answer F A m 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 : (Fin m → Bool) → F) => true) (Sum.inl p) (Sum.inr q) (ParsedAnswer.pauli x)
(seedAnswer b)
theorem
MIPRE.Introspection.Complete.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 ℓ : ℕ}
[NeZero m]
(L : Bool → CL.CLFun F (Fin m → Bool) ℓ)
(D : Seed F m → Seed F m → 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 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.Complete.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 ℓ : ℕ}
[NeZero m]
(L : Bool → CL.CLFun F (Fin m → Bool) ℓ)
(D : Seed F m → Seed F m → A → A → Bool)
(R : SyncStrategy (Honest.sourceGame L D).doubled)
(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 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.Complete.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 ℓ : ℕ}
[NeZero m]
(L : Bool → CL.CLFun F (Fin m → Bool) ℓ)
(D : Seed F m → Seed F m → A → A → Bool)
(R : SyncStrategy (Honest.sourceGame L D).doubled)
(hm : m ∣ Fintype.card F)
(hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ)
(w : Bool)
(a b : Answer F A m 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.Complete.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 ℓ : ℕ}
[NeZero m]
(L : Bool → CL.CLFun F (Fin m → Bool) ℓ)
(D : Seed F m → Seed F m → A → A → Bool)
(R : SyncStrategy (Honest.sourceGame L D).doubled)
(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 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)
:
theorem
MIPRE.Introspection.Complete.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 ℓ : ℕ}
[NeZero m]
(L : Bool → CL.CLFun F (Fin m → Bool) ℓ)
(D : Seed F m → Seed F m → A → A → Bool)
(R : SyncStrategy (Honest.sourceGame L D).doubled)
(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 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)
: