Perfect honest Pauli-Z/Sample edges

The Pauli-Z measurement reads the seed register and ignores the original strategy's auxiliary register. Its product with the honest Sample operator is zero unless their complete reported seeds agree.

def MIPRE.Introspection.Honest.pauliZOp {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) (z : ι → F) : Matrix ((ι → F) × Fin R.d) ((ι → F) × Fin R.d) ℂ

Equations

• MIPRE.Introspection.Honest.pauliZOp L D R z = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (MIPRE.Introspection.readout id z) 1

theorem MIPRE.Introspection.Honest.sampleOp_eq {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) (w : Bool) (ya : (ι → F) × A) : coreOp L D R (true, w) ya = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (readout id ya.1) (R.P.M (w, (L w).eval ya.1) ya.2)

theorem MIPRE.Introspection.Honest.pauliZ_sample_mul {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) (w : Bool) (z : ι → F) (ya : (ι → F) × A) : pauliZOp L D R z * coreOp L D R (true, w) ya = if z = ya.1 then coreOp L D R (true, w) ya else 0

theorem MIPRE.Introspection.Honest.sample_pauliZ_mul {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) (w : Bool) (z : ι → F) (ya : (ι → F) × A) : coreOp L D R (true, w) ya * pauliZOp L D R z = if z = ya.1 then coreOp L D R (true, w) ya else 0

theorem MIPRE.Introspection.Honest.pauliZ_sample_commute {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) (w : Bool) (z : ι → F) (ya : (ι → F) × A) : Commute (pauliZOp L D R z) (coreOp L D R (true, w) ya)

theorem MIPRE.Introspection.Honest.sample_typed_check {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) {P : Type u_4} (X Z : P) (DP : P → P → (ι → F) → (ι → F) → Bool) (w : Bool) (z : ι → F) (ya : (ι → F) × A) : TypedPredicate.check L X Z id D DP (Sum.inl Z) (coreType (true, w)) (ParsedAnswer.pauli z) (ParsedAnswer.pair ya.1 ya.2) = decide (z = ya.1)

theorem MIPRE.Introspection.Honest.sample_typed_reject_zero {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) {P : Type u_4} (X Z : P) (DP : P → P → (ι → F) → (ι → F) → Bool) (w : Bool) (z : ι → F) (ya : (ι → F) × A) (h : TypedPredicate.check L X Z id D DP (Sum.inl Z) (coreType (true, w)) (ParsedAnswer.pauli z) (ParsedAnswer.pair ya.1 ya.2) = false) : pauliZOp L D R z * coreOp L D R (true, w) ya = 0

Rejection by the actual Pauli-Z/Sample parsed test has zero honest operator product.