The first honest Hide measurement in the full Pauli register

The recursive construction uses the subtype of the active register as its basis. At the full register this is precisely the ordinary Pauli-X coarse measurement, after the explicit computational-basis relabelling.

def MIPRE.Introspection.Honest.univIndex {ι : Type u_2} [Fintype ι] : ↥Finset.univ ≃ ι

Equations

• MIPRE.Introspection.Honest.univIndex = { toFun := Subtype.val, invFun := fun (i : ι) => ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem MIPRE.Introspection.Honest.trDot_univRestriction {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] (x y : ι → F) : Weyl.trDot (univRestriction x) (univRestriction y) = Weyl.trDot x y

theorem MIPRE.Introspection.Honest.pauliX_univRestriction {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] (z : ι → F) : registerOp univRestriction (Weyl.proj Weyl.wX (univRestriction z)) = Weyl.proj Weyl.wX z

theorem MIPRE.Introspection.Honest.hideOp_zero_eq_firstHideOp {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 : HideLabel F ι) : hideOp P 0 h a = firstHideOp P a

The zero-stage recursive Hide PVM is exactly the ordinary full-register X coarsening.

theorem MIPRE.Introspection.Honest.pauliX_hideOp_zero_commute {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) (x : ι → F) (a : HideLabel F ι) : Commute (Weyl.proj Weyl.wX x) (hideOp P 0 h a)

theorem MIPRE.Introspection.Honest.pauliX_hideOp_zero_reject {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) (x : ι → F) (a : HideLabel F ι) (hr : ¬CLChecks.hidingPauli P x a) : Weyl.proj Weyl.wX x * hideOp P 0 h a = 0