Every edge of the full introspection graph has perfect honest play

noncomputable def MIPRE.Introspection.Complete.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 ℓ : ℕ} [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) (c : QLD.Content F m) : QuestionType QLD.Ty ℓ → Answer F A m d → Matrix (Space L D R) (Space L D R) ℂ

Equations

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

noncomputable def MIPRE.Introspection.Complete.sampleCheck {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (hm : m ∣ Fintype.card F) (c : QLD.Content F m) (t u : QuestionType QLD.Ty ℓ) (a b : ParsedAnswer ((Fin m → Bool) → F) A (QLD.Answer F m d)) : Bool

Equations

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

theorem MIPRE.Introspection.Complete.pauli_adj {ℓ : ℕ} (p q : QLD.Ty) (h : TypeGraph.Adj QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (Sum.inl p) (Sum.inl q)) : QLD.adj p q = true

theorem MIPRE.Introspection.Complete.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 ℓ : ℕ} [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) (c : QLD.Content F m) (p q : QLD.Ty) (h : QLD.adj p q = true) (a b : Answer F A m 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.Complete.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 ℓ : ℕ} [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) (hd : 1 ≤ d) (c : QLD.Content F m) (p q : QLD.Ty) (h : QLD.adj p q = true) (a b : Answer F A m 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.Complete.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 ℓ : ℕ} [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) (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 d) : Commute (sampleOp L D R hm hL c p a) (sampleOp L D R hm hL c q b)

theorem MIPRE.Introspection.Complete.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 ℓ : ℕ} [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) (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 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