The complete honest auxiliary measurement family

All auxiliary vertices use one common register/source space. The graph and predicate are the actual restrictions of the typed introspection construction, including every Hide level, Read, Sample, Introspect, and consistency loops.

@[reducible, inline]

abbrev MIPRE.Introspection.Honest.AuxQuestion (ℓ : ℕ) : Type

Equations

• MIPRE.Introspection.Honest.AuxQuestion ℓ = (MIPRE.Introspection.AuxType ℓ × Bool)

noncomputable def MIPRE.Introspection.Honest.auxOp {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (t : AuxQuestion ℓ) : ParsedAnswer (ι → F) A PA → Matrix ((ι → F) × Fin R.d) ((ι → F) × Fin R.d) ℂ

Equations

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

theorem MIPRE.Introspection.Honest.auxOp_isPVM {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (t : AuxQuestion ℓ) : IsPVM (auxOp L D R hL t)

theorem MIPRE.Introspection.Honest.parsedCore_core_commute {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hR : R.IsPCC) (t u : CoreType) (a b : ParsedAnswer (ι → F) A PA) : Commute (parsedCoreOp L D R t a) (parsedCoreOp L D R u b)

theorem MIPRE.Introspection.Honest.parsedCore_core_reject_zero {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hR : R.IsPCC) (hval : R.value = 1) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (t u : CoreType) (a b : ParsedAnswer (ι → F) A PA) (hr : TypedPredicate.check L X Z projectPauli D DP (coreType t) (coreType u) a b = false) : parsedCoreOp L D R t a * parsedCoreOp L D R u b = 0

theorem MIPRE.Introspection.Honest.auxCheck_swap {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (t u : AuxQuestion ℓ) (a b : ParsedAnswer (ι → F) A PA) : TypedPredicate.check L X Z projectPauli D DP (Sum.inr t) (Sum.inr u) a b = TypedPredicate.check L X Z projectPauli D DP (Sum.inr u) (Sum.inr t) b a

theorem MIPRE.Introspection.Honest.auxOp_nonzero_fits {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (t : AuxQuestion ℓ) (a : ParsedAnswer (ι → F) A PA) (ha : auxOp L D R hL t a ≠ 0) : TypedPredicate.fits (Sum.inr t) a = true

theorem MIPRE.Introspection.Honest.auxCheck_self {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (t : AuxQuestion ℓ) (a : ParsedAnswer (ι → F) A PA) (ha : TypedPredicate.fits (Sum.inr t) a = true) : TypedPredicate.check L X Z projectPauli D DP (Sum.inr t) (Sum.inr t) a a = true

theorem MIPRE.Introspection.Honest.auxOp_self_reject_zero {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (t : AuxQuestion ℓ) (a b : ParsedAnswer (ι → F) A PA) (hr : TypedPredicate.check L X Z projectPauli D DP (Sum.inr t) (Sum.inr t) a b = false) : auxOp L D R hL t a * auxOp L D R hL t b = 0

theorem MIPRE.Introspection.Honest.auxOp_oriented_commute {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (E : P → P → Bool) (X Z : P) (t u : AuxQuestion ℓ) (he : TypeGraph.oriented E X Z (Sum.inr t) (Sum.inr u) = true) (a b : ParsedAnswer (ι → F) A PA) : Commute (auxOp L D R hL t a) (auxOp L D R hL u b)

theorem MIPRE.Introspection.Honest.auxOp_oriented_reject_zero {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hval : R.value = 1) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (t u : AuxQuestion ℓ) (he : TypeGraph.oriented E X Z (Sum.inr t) (Sum.inr u) = true) (a b : ParsedAnswer (ι → F) A PA) (hr : TypedPredicate.check L X Z projectPauli D DP (Sum.inr t) (Sum.inr u) a b = false) : auxOp L D R hL t a * auxOp L D R hL u b = 0

theorem MIPRE.Introspection.Honest.auxOp_commute {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (E : P → P → Bool) (X Z : P) (t u : AuxQuestion ℓ) (he : TypeGraph.Adj E X Z (Sum.inr t) (Sum.inr u)) (a b : ParsedAnswer (ι → F) A PA) : Commute (auxOp L D R hL t a) (auxOp L D R hL u b)

theorem MIPRE.Introspection.Honest.auxOp_reject_zero {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hval : R.value = 1) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (t u : AuxQuestion ℓ) (he : TypeGraph.Adj E X Z (Sum.inr t) (Sum.inr u)) (a b : ParsedAnswer (ι → F) A PA) (hr : TypedPredicate.check L X Z projectPauli D DP (Sum.inr t) (Sum.inr u) a b = false) : auxOp L D R hL t a * auxOp L D R hL u b = 0