Correctness of the adaptive honest Read measurement

The adaptive register measurement refines the actual CL question readout. Consequently attaching the original question-dependent answer measurement gives the honest Read PVM and perfect commutation and acceptance on Introspect/Read.

theorem MIPRE.Introspection.Honest.restrict_insertRegister {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] (S V : Finset ι) (h : S ⊆ V) (x : ↥V → F) : (coordinateRestrict S) (insertRegister V x) = ((coordinateSplit S V h) x).1

theorem MIPRE.Introspection.Honest.linear_insertRegister {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {S V : Finset ι} (h : S ⊆ V) (L : CL.RegLinear F S) (x : ↥V → F) : L (insertRegister V x) = (coordinateInsert S) ((coordinateLinear L) ((coordinateSplit S V h) x).1)

theorem MIPRE.Introspection.Honest.tail_insertRegister {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] (S V : Finset ι) (h : S ⊆ V) (x : ↥V → F) : (CL.proj Sᶜ) (insertRegister V x) = insertRegister (V \ S) ((coordinateSplit S V h) x).2

theorem MIPRE.Introspection.Honest.localRead_entry_nonzero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {S : Finset ι} (L : CL.RegLinear F S) (a : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) (x x' : Fin (Fintype.card ↥S) → F) (h : localRead L a x x' ≠ 0) : (coordinateLinear L) x = a.1

theorem MIPRE.Introspection.Honest.readRegister_entry_nonzero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (V : Finset ι) (h : P.SupportedOn V) (a : ReadLabel F ι) (x x' : ↥V → F) (ha : readRegister P V h a x x' ≠ 0) : P.eval (insertRegister V x) = a.1

A nonzero Read entry has the claimed CL question on its computational row.

theorem MIPRE.Introspection.Honest.readout_mul_readRegister {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (V : Finset ι) (h : P.SupportedOn V) (y : ι → F) (a : ReadLabel F ι) : readout (fun (x : ↥V → F) => P.eval (insertRegister V x)) y * readRegister P V h a = if y = a.1 then readRegister P V h a else 0

Multiplying by the CL question readout selects precisely the reported question.

theorem MIPRE.Introspection.Honest.readRegister_marginal {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (V : Finset ι) (h : P.SupportedOn V) (y : ι → F) : ∑ yp : ι → F, readRegister P V h (y, yp) = readout (fun (x : ↥V → F) => P.eval (insertRegister V x)) y

The first marginal of the honest Read PVM is exactly the source CL readout.

def MIPRE.Introspection.Honest.univRestriction {F : Type u_1} {ι : Type u_2} [Fintype ι] : (ι → F) ≃ (↥Finset.univ → F)

Equations

• MIPRE.Introspection.Honest.univRestriction = { toFun := fun (x : ι → F) (i : ↥Finset.univ) => x ↑i, invFun := fun (x : ↥Finset.univ → F) (i : ι) => x ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MIPRE.Introspection.Honest.insertRegister_univ {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] (x : ι → F) : insertRegister Finset.univ (univRestriction x) = x

noncomputable def MIPRE.Introspection.Honest.readOp {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (h : P.SupportedOn Finset.univ) (a : ReadLabel F ι) : Matrix (ι → F) (ι → F) ℂ

The full adaptive Read measurement on the ambient Pauli register.

Equations

• MIPRE.Introspection.Honest.readOp P h a = MIPRE.Introspection.registerOp MIPRE.Introspection.Honest.univRestriction (MIPRE.Introspection.Honest.readRegister P Finset.univ h a)

theorem MIPRE.Introspection.Honest.readOp_isPVM {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (h : P.SupportedOn Finset.univ) : IsPVM (readOp P h)

theorem MIPRE.Introspection.Honest.readout_mul_readOp {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (h : P.SupportedOn Finset.univ) (y : ι → F) (a : ReadLabel F ι) : readout P.eval y * readOp P h a = if y = a.1 then readOp P h a else 0

theorem MIPRE.Introspection.Honest.readOp_marginal {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (h : P.SupportedOn Finset.univ) (y : ι → F) : ∑ yp : ι → F, readOp P h (y, yp) = readout P.eval y