The adaptive honest Read and Hide measurements

The recursion follows the CL presentation itself. At a cons node the joint Z/linear and X/dual-linear measurement is made on the current register. Its Z outcome selects the continuation on the complementary register. These are actual projective measurements; no commutation assumption on different continuations is needed.

def MIPRE.Introspection.Honest.adaptiveTensor {I : Type u_1} {J : Type u_2} {A : Type u_3} {B : Type u_4} (P : A → Matrix I I ℂ) (Q : A → B → Matrix J J ℂ) (ab : A × B) : Matrix (I × J) (I × J) ℂ

Measure one register and use its outcome to select a measurement of the other.

Equations

• MIPRE.Introspection.Honest.adaptiveTensor P Q ab = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P ab.1) (Q ab.1 ab.2)

theorem MIPRE.Introspection.Honest.adaptiveTensor_isPVM {I : Type u_1} {J : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (P : A → Matrix I I ℂ) (Q : A → B → Matrix J J ℂ) (hP : IsPVM P) (hQ : ∀ (a : A), IsPVM (Q a)) : IsPVM (adaptiveTensor P Q)

@[reducible, inline]

abbrev MIPRE.Introspection.Honest.ReadLabel (F : Type u_3) (ι : Type u_4) : Type (max u_3 u_4)

Equations

• MIPRE.Introspection.Honest.ReadLabel F ι = ((ι → F) × (ι → F))

@[reducible, inline]

abbrev MIPRE.Introspection.Honest.HideLabel (F : Type u_3) (ι : Type u_4) : Type (max u_3 u_4)

Equations

• MIPRE.Introspection.Honest.HideLabel F ι = ((ι → F) × (ι → F) × (ι → F))

def MIPRE.Introspection.Honest.insertRegister {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] (V : Finset ι) (x : ↥V → F) : ι → F

Extend an assignment on an active register by zero to the ambient space.

Equations

• MIPRE.Introspection.Honest.insertRegister V x i = if h : i ∈ V then x ⟨i, h⟩ else 0

noncomputable def MIPRE.Introspection.Honest.localRead {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [DecidableEq ι] {S : Finset ι} (L : CL.RegLinear F S) (ab : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) : Matrix (Fin (Fintype.card ↥S) → F) (Fin (Fintype.card ↥S) → F) ℂ

The honest commuting local Z/linear and X/dual-linear measurement.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.Honest.localRead_isPVM {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) : IsPVM (localRead L)

noncomputable def MIPRE.Introspection.Honest.joinRead {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] (S : Finset ι) (a : ((Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) × ReadLabel F ι) : ReadLabel F ι

Equations

• MIPRE.Introspection.Honest.joinRead S a = ((MIPRE.Introspection.coordinateInsert S) a.1.1 + a.2.1, (MIPRE.Introspection.coordinateInsert S) a.1.2 + a.2.2)

noncomputable def MIPRE.Introspection.Honest.joinHide {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] (S : Finset ι) (a : ((Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) × HideLabel F ι) : HideLabel F ι

Equations

• MIPRE.Introspection.Honest.joinHide S a = ((MIPRE.Introspection.coordinateInsert S) a.1.1 + a.2.1, (MIPRE.Introspection.coordinateInsert S) a.1.2 + a.2.2.1, a.2.2.2)

def MIPRE.Introspection.Honest.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 ι) : P.SupportedOn V → ReadLabel F ι → Matrix (↥V → F) (↥V → F) ℂ

The register part of the honest Read measurement, including all adaptive stages.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.Honest.readRegister MIPRE.CL.CLFun.zero x x_2 x_1 = if x_1 = (0, 0) then 1 else 0

theorem MIPRE.Introspection.Honest.readRegister_isPVM {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) : IsPVM (readRegister P V h)

Every adaptive Read family is a PVM, even for zero-probability branch labels.

noncomputable def MIPRE.Introspection.Honest.stopHideAnswer {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (V : Finset ι) (x : ↥V → F) : HideLabel F ι

At a stopping node, retain the full X tail and the first dual value, without reading Z.

Equations

• MIPRE.Introspection.Honest.stopHideAnswer P V x = MIPRE.Introspection.Honest.firstHideAnswer P (MIPRE.Introspection.Honest.insertRegister V x)

noncomputable def MIPRE.Introspection.Honest.stopHide {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 ι) : HideLabel F ι → Matrix (↥V → F) (↥V → F) ℂ

Equations

• MIPRE.Introspection.Honest.stopHide P V = MIPRE.Weyl.synOf MIPRE.Weyl.wX (MIPRE.Introspection.Honest.stopHideAnswer P V)

theorem MIPRE.Introspection.Honest.stopHide_isPVM {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 ι) : IsPVM (stopHide P V)

def MIPRE.Introspection.Honest.hideRegister {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (V : Finset ι) : P.SupportedOn V → HideLabel F ι → Matrix (↥V → F) (↥V → F) ℂ

The honest Hide measurement at zero-based stage k. Earlier stages read joint Z/linear and X/dual-linear outcomes; the current stage and remaining tail use X only.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.Honest.hideRegister x_1 0 x_2 x_3 x_4 = MIPRE.Introspection.Honest.stopHide x_1 x_2 x_4
• MIPRE.Introspection.Honest.hideRegister MIPRE.CL.CLFun.zero n.succ x x_2 x_1 = MIPRE.Introspection.Honest.stopHide MIPRE.CL.CLFun.zero x x_1

@[simp]

theorem MIPRE.Introspection.Honest.hideRegister_zero {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 : HideLabel F ι) : hideRegister P 0 V h a = stopHide P V a

theorem MIPRE.Introspection.Honest.hideRegister_zero_fun {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) : hideRegister P 0 V h = stopHide P V

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

Projectivity of every honest hiding level, including the branch-dependent later levels.