The full honest Read measurement and the reading edge

The auxiliary answer is measured using the original strategy at the question reported by the adaptive register measurement. Its marginal is exactly the honest Introspect measurement, on the full answer alphabet.

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

The complete honest Read operator: adaptive register data and the original answer.

Equations

• MIPRE.Introspection.Honest.fullReadOp L D R w h a = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (MIPRE.Introspection.Honest.readOp (L w) h a.1) (R.P.M (w, a.1.1) a.2)

theorem MIPRE.Introspection.Honest.fullReadOp_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) (w : Bool) (h : (L w).SupportedOn Finset.univ) : IsPVM (fullReadOp L D R w h)

theorem MIPRE.Introspection.Honest.fullReadOp_marginal {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) (y : ι → F) (a : A) : ∑ yp : ι → F, fullReadOp L D R w h ((y, yp), a) = coreOp L D R (false, w) (y, a)

Forgetting only the dual output gives the original honest Introspect operator exactly.

theorem MIPRE.Introspection.Honest.introspect_read_mul {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) (ya : (ι → F) × A) (v : ReadLabel F ι × A) : coreOp L D R (false, w) ya * fullReadOp L D R w h v = if ya = (v.1.1, v.2) then fullReadOp L D R w h v else 0

The Introspect/Read product selects exactly equal questions and original answers.

theorem MIPRE.Introspection.Honest.read_introspect_mul {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) (ya : (ι → F) × A) (v : ReadLabel F ι × A) : fullReadOp L D R w h v * coreOp L D R (false, w) ya = if ya = (v.1.1, v.2) then fullReadOp L D R w h v else 0

theorem MIPRE.Introspection.Honest.introspect_read_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) (ya : (ι → F) × A) (v : ReadLabel F ι × A) : Commute (coreOp L D R (false, w) ya) (fullReadOp L D R w h v)

Honest Introspect and Read commute for every label, without needing source PCC.

theorem MIPRE.Introspection.Honest.read_typed_check {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} {PA : Type u_5} (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (w : Bool) (ya : (ι → F) × A) (v : ReadLabel F ι × A) : TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.introspect, w)) (Sum.inr (AuxType.read, w)) (ParsedAnswer.pair ya.1 ya.2) (ParsedAnswer.read v.1.1 v.1.2 v.2) = decide (ya = (v.1.1, v.2))

theorem MIPRE.Introspection.Honest.read_typed_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} {PA : Type u_5} (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (w : Bool) (h : (L w).SupportedOn Finset.univ) (ya : (ι → F) × A) (v : ReadLabel F ι × A) (hr : TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.introspect, w)) (Sum.inr (AuxType.read, w)) (ParsedAnswer.pair ya.1 ya.2) (ParsedAnswer.read v.1.1 v.1.2 v.2) = false) : coreOp L D R (false, w) ya * fullReadOp L D R w h v = 0

Rejection on the actual parsed Introspect/Read edge has zero honest operator product.