Every edge of the full introspection graph has perfect honest play

noncomputable def MIPRE.Introspection.BinaryComplete.sampleOp {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) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (c : QLD.Content F m) : QuestionType QLD.Ty ℓ → Answer F A m t d → Matrix (Space L D R) (Space L D R) ℂ

Equations

• MIPRE.Introspection.BinaryComplete.sampleOp β L D R hm hL c (Sum.inl p) = MIPRE.Introspection.BinaryComplete.pauliOp β L D R hm (MIPRE.QLD.Content.question hm c p)
• MIPRE.Introspection.BinaryComplete.sampleOp β L D R hm hL c (Sum.inr q) = MIPRE.Introspection.BinaryComplete.auxOp L D R hL q

noncomputable def MIPRE.Introspection.BinaryComplete.sampleCheck {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {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) (hm : m ∣ Fintype.card F) (c : QLD.Content F m) : QuestionType QLD.Ty ℓ → (u : QuestionType QLD.Ty ℓ) → (a b : ParsedAnswer (Coord m t → ZMod 2) A (QLD.Answer F m d)) → Bool

Equations

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

theorem MIPRE.Introspection.BinaryComplete.pauli_pair_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) (hm : m ∣ Fintype.card F) (c : QLD.Content F m) (p q : QLD.Ty) (h : QLD.adj p q = true) (a b : Answer F A m t d) : Commute (pauliOp β L D R hm (QLD.Content.question hm c p) a) (pauliOp β L D R hm (QLD.Content.question hm c q) b)

theorem MIPRE.Introspection.BinaryComplete.pauli_pair_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) (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) (c : QLD.Content F m) (p q : QLD.Ty) (h : QLD.adj p q = true) (a b : Answer F A m t d) (hr : sampleCheck β L D hm c (Sum.inl p) (Sum.inl q) a b = false) : pauliOp β L D R hm (QLD.Content.question hm c p) a * pauliOp β L D R hm (QLD.Content.question hm c q) b = 0

theorem MIPRE.Introspection.BinaryComplete.sampleOp_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) (hR : R.IsPCC) (c : QLD.Content F m) (p q : QuestionType QLD.Ty ℓ) (h : TypeGraph.Adj QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) p q) (a b : Answer F A m t d) : Commute (sampleOp β L D R hm hL c p a) (sampleOp β L D R hm hL c q b)

theorem MIPRE.Introspection.BinaryComplete.sampleOp_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) (hd : 1 ≤ d) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hval : R.value = 1) (c : QLD.Content F m) (p q : QuestionType QLD.Ty ℓ) (h : TypeGraph.Adj QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) p q) (a b : Answer F A m t d) (hr : sampleCheck β L D hm c p q a b = false) : sampleOp β L D R hm hL c p a * sampleOp β L D R hm hL c q b = 0