A common carrier for all honest introspection measurements

The concrete Pauli measurements and the full auxiliary family share the same field register, original strategy register, and one extra qubit. The permutation below moves that qubit past the original strategy register; it does not change any measurement or require a completeness premise for the Pauli test.

@[reducible, inline]

abbrev MIPRE.Introspection.Complete.Seed (F : Type u_3) (m : ℕ) : Type u_3

Equations

• MIPRE.Introspection.Complete.Seed F m = MIPRE.QLD.Honest.Register F m

@[reducible, inline]

abbrev MIPRE.Introspection.Complete.Answer (F : Type u_3) (A : Type u_4) (m d : ℕ) : Type (max u_3 u_4)

Equations

• MIPRE.Introspection.Complete.Answer F A m d = MIPRE.Introspection.ParsedAnswer (MIPRE.Introspection.Complete.Seed F m) A (MIPRE.QLD.Answer F m d)

def MIPRE.Introspection.Complete.project {F : Type u_1} [Field F] {m d : ℕ} : QLD.Answer F m d → Seed F m

The actual full Pauli answer carries the seed; other formats have a fixed projection and zero effect at the distinguished Pauli questions.

Equations

• MIPRE.Introspection.Complete.project (MIPRE.QLD.Answer.pauliAns x_1) = x_1
• MIPRE.Introspection.Complete.project x✝ = 0

@[reducible, inline]

abbrev MIPRE.Introspection.Complete.Space {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [Fintype A] [DecidableEq A] {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) : Type u_1

Equations

• MIPRE.Introspection.Complete.Space L D R = ((MIPRE.Introspection.Complete.Seed F m × Fin R.d) × Fin 2)

def MIPRE.Introspection.Complete.shuffle {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [Fintype A] [DecidableEq A] {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) : Space L D R ≃ QLD.Honest.Space F m × Fin R.d

Equations

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

def MIPRE.Introspection.Complete.pauliLift {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [Fintype A] [DecidableEq A] {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) (M : Matrix (QLD.Honest.Space F m) (QLD.Honest.Space F m) ℂ) : Matrix (Space L D R) (Space L D R) ℂ

Equations

• MIPRE.Introspection.Complete.pauliLift L D R M = MIPRE.Introspection.registerOp (MIPRE.Introspection.Complete.shuffle L D R) (MIPRE.aOp M)

@[simp]

theorem MIPRE.Introspection.Complete.pauliLift_zero {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m ℓ : ℕ} [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) : pauliLift L D R 0 = 0

theorem MIPRE.Introspection.Complete.pauliLift_mul {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m ℓ : ℕ} [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) (M N : Matrix (QLD.Honest.Space F m) (QLD.Honest.Space F m) ℂ) : pauliLift L D R (M * N) = pauliLift L D R M * pauliLift L D R N

theorem MIPRE.Introspection.Complete.pauliLift_isPVM {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m ℓ : ℕ} [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) {B : Type u_3} [Fintype B] [DecidableEq B] {M : B → Matrix (QLD.Honest.Space F m) (QLD.Honest.Space F m) ℂ} (hM : IsPVM M) : IsPVM fun (a : B) => pauliLift L D R (M a)

theorem MIPRE.Introspection.Complete.pauliLift_register {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m ℓ : ℕ} [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) (M : Matrix (Seed F m) (Seed F m) ℂ) : pauliLift L D R (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1) = aOp (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1)

noncomputable def MIPRE.Introspection.Complete.pauliOp {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) (q : QLD.Question F m) : Answer F A m d → Matrix (Space L D R) (Space L D R) ℂ

Equations

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

theorem MIPRE.Introspection.Complete.pauliOp_isPVM {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) (q : QLD.Question F m) : IsPVM (pauliOp L D R hm q)

noncomputable def MIPRE.Introspection.Complete.auxOp {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ : ℕ} (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) : Matrix (Space L D R) (Space L D R) ℂ

Equations

• MIPRE.Introspection.Complete.auxOp L D R hL q a = MIPRE.aOp (MIPRE.Introspection.Honest.auxOp L D R hL q a)

theorem MIPRE.Introspection.Complete.auxOp_isPVM {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 ℓ) : IsPVM (auxOp L D R hL q)

theorem MIPRE.Introspection.Complete.pauliOp_pauliAns {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) (x : Seed F m) : pauliOp L D R hm (QLD.Question.pauli W) (ParsedAnswer.pauli (QLD.Answer.pauliAns x)) = aOp (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (QLD.Honest.pauliOp W x) 1)

theorem MIPRE.Introspection.Complete.pauliOp_wrong {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 : QLD.Answer F m d) (ha : (QLD.Question.pauli W).fmtOk a = false) : pauliOp L D R hm (QLD.Question.pauli W) (ParsedAnswer.pauli a) = 0

theorem MIPRE.Introspection.Complete.pauliOp_X {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) (x : Seed F m) : pauliOp L D R hm (QLD.Question.pauli QLD.Bas.X) (ParsedAnswer.pauli (QLD.Answer.pauliAns x)) = aOp (Honest.pauliXOp L D R x)

theorem MIPRE.Introspection.Complete.pauliOp_Z {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) (x : Seed F m) : pauliOp L D R hm (QLD.Question.pauli QLD.Bas.Z) (ParsedAnswer.pauli (QLD.Answer.pauliAns x)) = aOp (Honest.pauliZOp L D R x)