Documentation

MIPRE.Foundations.Introspection.HonestPauliEdges

Honest Pauli anchor edges on every parsed answer #

The X and Z effects below are the genuine full-register basis measurements. They leave the original strategy's auxiliary register unchanged. This file connects them to the same parsed Sample and Hide effects used in the complete auxiliary construction, including all malformed answer constructors.

def MIPRE.Introspection.Honest.parsedPauliOp {I : Type u_1} {V : Type u_2} {A : Type u_3} {PA : Type u_4} (M : PA → Matrix I I ℂ) :

ParsedAnswer V A PA → Matrix I I ℂ

Equations

MIPRE.Introspection.Honest.parsedPauliOp M (MIPRE.Introspection.ParsedAnswer.pauli a) = M a
MIPRE.Introspection.Honest.parsedPauliOp M x✝ = 0

Instances For

theorem MIPRE.Introspection.Honest.parsedPauliOp_isPVM {I : Type u_1} {V : Type u_2} {A : Type u_3} {PA : Type u_4} [Fintype I] [DecidableEq I] [Fintype V] [Fintype A] [Fintype PA] (M : PA → Matrix I I ℂ) (hM : IsPVM M) :

IsPVM (parsedPauliOp M)

noncomputable def MIPRE.Introspection.Honest.pauliXOp {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) (x : ι → F) :

Matrix ((ι → F) × Fin R.d) ((ι → F) × Fin R.d) ℂ

Equations

MIPRE.Introspection.Honest.pauliXOp L D R x = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (MIPRE.Weyl.proj MIPRE.Weyl.wX x) 1

Instances For

theorem MIPRE.Introspection.Honest.pauliXOp_isPVM {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) :

IsPVM (pauliXOp L D R)

theorem MIPRE.Introspection.Honest.pauliZOp_isPVM {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) :

IsPVM (pauliZOp L D R)

noncomputable def MIPRE.Introspection.Honest.parsedPauliXOp {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) :

ParsedAnswer (ι → F) A (ι → F) → Matrix ((ι → F) × Fin R.d) ((ι → F) × Fin R.d) ℂ

Equations

MIPRE.Introspection.Honest.parsedPauliXOp L D R = MIPRE.Introspection.Honest.parsedPauliOp (MIPRE.Introspection.Honest.pauliXOp L D R)

Instances For

def MIPRE.Introspection.Honest.parsedPauliZOp {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) :

ParsedAnswer (ι → F) A (ι → F) → Matrix ((ι → F) × Fin R.d) ((ι → F) × Fin R.d) ℂ

Equations

MIPRE.Introspection.Honest.parsedPauliZOp L D R = MIPRE.Introspection.Honest.parsedPauliOp (MIPRE.Introspection.Honest.pauliZOp L D R)

Instances For

theorem MIPRE.Introspection.Honest.parsedPauliXOp_isPVM {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) :

IsPVM (parsedPauliXOp L D R)

theorem MIPRE.Introspection.Honest.parsedPauliZOp_isPVM {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) :

IsPVM (parsedPauliZOp L D R)

theorem MIPRE.Introspection.Honest.parsedPauliX_hide_commute {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) (w : Bool) (h : (L w).SupportedOn Finset.univ) (a b : ParsedAnswer (ι → F) A (ι → F)) :

Commute (parsedPauliXOp L D R a) (parsedHideOp L D R w 0 h b)

theorem MIPRE.Introspection.Honest.parsedPauliZ_sample_commute {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) (w : Bool) (a b : ParsedAnswer (ι → F) A (ι → F)) :

Commute (parsedPauliZOp L D R a) (parsedCoreOp L D R (true , w) b)

theorem MIPRE.Introspection.Honest.check_pauli_aux_swap {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) {P : Type u_4} (X Z : P) (DP : P → P → (ι → F) → (ι → F) → Bool) (p : P) (t : AuxType ℓ × Bool) (a b : ParsedAnswer (ι → F) A (ι → F)) :

TypedPredicate.check L X Z id D DP (Sum.inl p) (Sum.inr t) a b = TypedPredicate.check L X Z id D DP (Sum.inr t) (Sum.inl p) b a

theorem MIPRE.Introspection.Honest.parsedPauliX_hide_reject_zero {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) {P : Type u_4} (X Z : P) (DP : P → P → (ι → F) → (ι → F) → Bool) (w : Bool) (k : Fin ℓ) (hk : ↑k = 0) (h : (L w).SupportedOn Finset.univ) (a b : ParsedAnswer (ι → F) A (ι → F)) (hr : TypedPredicate.check L X Z id D DP (Sum.inl X) (Sum.inr (AuxType.hide k, w)) a b = false) :

parsedPauliXOp L D R a * parsedHideOp L D R w 0 h b = 0

theorem MIPRE.Introspection.Honest.parsedPauliZ_sample_reject_zero {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) {P : Type u_4} (X Z : P) (DP : P → P → (ι → F) → (ι → F) → Bool) (w : Bool) (a b : ParsedAnswer (ι → F) A (ι → F)) (hr : TypedPredicate.check L X Z id D DP (Sum.inl Z) (Sum.inr (AuxType.sample , w)) a b = false) :

parsedPauliZOp L D R a * parsedCoreOp L D R (true , w) b = 0

theorem MIPRE.Introspection.Honest.parsedHide_pauliX_reject_zero {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) {P : Type u_4} (X Z : P) (DP : P → P → (ι → F) → (ι → F) → Bool) (w : Bool) (k : Fin ℓ) (hk : ↑k = 0) (h : (L w).SupportedOn Finset.univ) (a b : ParsedAnswer (ι → F) A (ι → F)) (hr : TypedPredicate.check L X Z id D DP (Sum.inr (AuxType.hide k, w)) (Sum.inl X) a b = false) :

parsedHideOp L D R w 0 h a * parsedPauliXOp L D R b = 0

theorem MIPRE.Introspection.Honest.parsedSample_pauliZ_reject_zero {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) {P : Type u_4} (X Z : P) (DP : P → P → (ι → F) → (ι → F) → Bool) (w : Bool) (a b : ParsedAnswer (ι → F) A (ι → F)) (hr : TypedPredicate.check L X Z id D DP (Sum.inr (AuxType.sample , w)) (Sum.inl Z) a b = false) :

parsedCoreOp L D R (true , w) a * parsedPauliZOp L D R b = 0