Documentation

MIPRE.Foundations.Introspection.HonestFirstHide

The honest first hiding measurement #

At the first hiding type no Z-prefix has yet been measured. The honest measurement is exactly a coarse-graining of the full Pauli-X measurement: read the dual map on the first CL register and retain the untouched X tail. This constructs the measurement and proves perfect acceptance and commutation on the Pauli-X/first-Hide edge, on the entire answer alphabet.

source
noncomputable def MIPRE.Introspection.Honest.firstHideAnswer {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (x : ι → F) :
(ι → F) × (ι → F) × (ι → F)
Equations
Instances For
    source
    theorem MIPRE.Introspection.Honest.dualReadout_first_supported {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (x : ι → F) :
    (CL.proj (P.factorOfPrefix 0 0)) (CLChecks.dualReadout P 0 0 x) = CLChecks.dualReadout P 0 0 x
    source
    theorem MIPRE.Introspection.Honest.firstHideAnswer_check {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (x : ι → F) :
    CLChecks.hidingPauli P x (firstHideAnswer P x)

    The reported dual value and untouched tail satisfy the source test exactly.

    source
    noncomputable def MIPRE.Introspection.Honest.firstHideOp {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (v : (ι → F) × (ι → F) × (ι → F)) :
    Matrix (ι → F) (ι → F) ℂ
    Equations
    Instances For
      source
      theorem MIPRE.Introspection.Honest.firstHideOp_isPVM {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) :
      IsPVM (firstHideOp P)

      The first hiding family is an actual PVM, including zero outcomes off the honest image.

      source
      theorem MIPRE.Introspection.Honest.pauli_mul_firstHide {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (x : ι → F) (v : (ι → F) × (ι → F) × (ι → F)) :
      Weyl.proj Weyl.wX x * firstHideOp P v = if firstHideAnswer P x = v then Weyl.proj Weyl.wX x else 0

      Pauli-X followed by first-Hide retains exactly the selected coarse label.

      source
      theorem MIPRE.Introspection.Honest.pauli_firstHide_commute {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (x : ι → F) (v : (ι → F) × (ι → F) × (ι → F)) :
      Commute (Weyl.proj Weyl.wX x) (firstHideOp P v)

      The honest Pauli-X and first hiding operators commute on all answer labels.

      source
      theorem MIPRE.Introspection.Honest.firstHide_reject_zero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (x : ι → F) (v : (ι → F) × (ι → F) × (ι → F)) (h : ¬CLChecks.hidingPauli P x v) :
      Weyl.proj Weyl.wX x * firstHideOp P v = 0

      Every answer pair rejected on the first hiding edge has zero operator product.

      source
      theorem MIPRE.Introspection.Honest.firstHide_typed_check {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : Type u_3} {A : Type u_4} (L : Bool → CL.CLFun F ι ℓ) (X Z : P) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : P → P → (ι → F) → (ι → F) → Bool) (w : Bool) (k : Fin ℓ) (hk : ↑k = 0) (x : ι → F) (v : (ι → F) × (ι → F) × (ι → F)) :
      TypedPredicate.check L X Z id D DP (Sum.inl X) (Sum.inr (AuxType.hide k, w)) (ParsedAnswer.pauli x) (ParsedAnswer.hide v.1 v.2.1 v.2.2) = decide (CLChecks.hidingPauli (L w) x v)

      The actual parsed Pauli-X/first-Hide predicate is the tested relation used above.

      source
      theorem MIPRE.Introspection.Honest.firstHide_typed_reject_zero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : Type u_3} {A : Type u_4} (L : Bool → CL.CLFun F ι ℓ) (X Z : P) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : P → P → (ι → F) → (ι → F) → Bool) (w : Bool) (k : Fin ℓ) (hk : ↑k = 0) (x : ι → F) (v : (ι → F) × (ι → F) × (ι → F)) (h : TypedPredicate.check L X Z id D DP (Sum.inl X) (Sum.inr (AuxType.hide k, w)) (ParsedAnswer.pauli x) (ParsedAnswer.hide v.1 v.2.1 v.2.2) = false) :
      Weyl.proj Weyl.wX x * firstHideOp (L w) v = 0

      A rejection by the full parsed predicate has zero honest operator product.