The honest Pauli measurements on the binary source register

A self-dual field basis transports the actual quantum projectors to qubit coordinates. The original CL functions remain binary; they are not assumed to arise by downsizing field-linear CL functions.

@[reducible, inline]

abbrev MIPRE.Introspection.BinaryComplete.Coord (m t : ℕ) : Type

Equations

• MIPRE.Introspection.BinaryComplete.Coord m t = ((Fin m → Bool) × Fin t)

@[reducible, inline]

abbrev MIPRE.Introspection.BinaryComplete.Seed (m t : ℕ) : Type

Equations

• MIPRE.Introspection.BinaryComplete.Seed m t = (MIPRE.Introspection.BinaryComplete.Coord m t → ZMod 2)

@[reducible, inline]

abbrev MIPRE.Introspection.BinaryComplete.Answer (F : Type u_1) (A : Type u_2) (m t d : ℕ) : Type (max u_2 u_1)

Equations

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

noncomputable def MIPRE.Introspection.BinaryComplete.project {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m d t : ℕ} (b : Module.Basis (Fin t) (ZMod 2) F) : QLD.Answer F m d → Seed m t

Equations

• MIPRE.Introspection.BinaryComplete.project b (MIPRE.QLD.Answer.pauliAns x_1) = (MIPRE.Weyl.binEquiv b) x_1
• MIPRE.Introspection.BinaryComplete.project b x✝ = 0

@[reducible, inline]

abbrev MIPRE.Introspection.BinaryComplete.Space {A : Type u_2} [Fintype A] [DecidableEq A] {m ℓ t : ℕ} (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) : Type

Equations

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

noncomputable def MIPRE.Introspection.BinaryComplete.shuffle {F : Type u_1} {A : Type u_2} [Field F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m ℓ t : ℕ} (b : 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) : 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.

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

Equations

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

@[simp]

theorem MIPRE.Introspection.BinaryComplete.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 ℓ t : ℕ} [NeZero m] (b : 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) : pauliLift b L D R 0 = 0

theorem MIPRE.Introspection.BinaryComplete.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 ℓ t : ℕ} [NeZero m] (b : 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) (M N : Matrix (QLD.Honest.Space F m) (QLD.Honest.Space F m) ℂ) : pauliLift b L D R (M * N) = pauliLift b L D R M * pauliLift b L D R N

theorem MIPRE.Introspection.BinaryComplete.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 ℓ t : ℕ} [NeZero m] (b : 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) {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 b L D R (M a)

theorem MIPRE.Introspection.BinaryComplete.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 ℓ t : ℕ} [NeZero m] (b : 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) (M : Matrix (QLD.Honest.Register F m) (QLD.Honest.Register F m) ℂ) : pauliLift b L D R (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1) = aOp (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (registerOp (Weyl.binEquiv b).symm M) 1)

noncomputable def MIPRE.Introspection.BinaryComplete.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 ℓ t : ℕ} [NeZero m] (b : 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) (q : QLD.Question F m) : Answer F A m t 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.BinaryComplete.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 ℓ t : ℕ} [NeZero m] (b : 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) (q : QLD.Question F m) : IsPVM (pauliOp b L D R hm q)

noncomputable def MIPRE.Introspection.BinaryComplete.auxOp {F : Type u_1} {A : Type u_2} [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} (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) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (q : Honest.AuxQuestion ℓ) (a : Answer F A m t d) : Matrix (Space L D R) (Space L D R) ℂ

Equations

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

theorem MIPRE.Introspection.BinaryComplete.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 ℓ t : ℕ} [NeZero m] (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) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (q : Honest.AuxQuestion ℓ) : IsPVM (auxOp L D R hL q)

theorem MIPRE.Introspection.BinaryComplete.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 ℓ t : ℕ} [NeZero m] (b : 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) (W : QLD.Bas) (a : QLD.Answer F m d) (ha : (QLD.Question.pauli W).fmtOk a = false) : pauliOp b L D R hm (QLD.Question.pauli W) (ParsedAnswer.pauli a) = 0

theorem MIPRE.Introspection.BinaryComplete.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 ℓ t : ℕ} [NeZero m] (b : 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) (hb : LowDegree.IsSelfDualBasis b) (hm : m ∣ Fintype.card F) (x : QLD.Honest.Register F m) : pauliOp b L D R hm (QLD.Question.pauli QLD.Bas.X) (ParsedAnswer.pauli (QLD.Answer.pauliAns x)) = aOp (Honest.pauliXOp L D R ((Weyl.binEquiv b) x))

theorem MIPRE.Introspection.BinaryComplete.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 ℓ t : ℕ} [NeZero m] (b : 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) (hb : LowDegree.IsSelfDualBasis b) (hm : m ∣ Fintype.card F) (x : QLD.Honest.Register F m) : pauliOp b L D R hm (QLD.Question.pauli QLD.Bas.Z) (ParsedAnswer.pauli (QLD.Answer.pauliAns x)) = aOp (Honest.pauliZOp L D R ((Weyl.binEquiv b) x))