The honest adaptive hiding prefixes

The first component of the honest hiding measurement is exactly the preceding CL prefix, for every level of the adaptive construction. The statement concerns the actual recursively constructed operators and the source CL truncation.

theorem MIPRE.Introspection.Honest.stopHide_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 ι) (a : HideLabel F ι) (x x' : ↥V → F) (ha : stopHide P V a x x' ≠ 0) : a.1 = 0

theorem MIPRE.Introspection.Honest.hideRegister_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 ι ℓ) (k : ℕ) (V : Finset ι) (h : P.SupportedOn V) (a : HideLabel F ι) (x x' : ↥V → F) (ha : hideRegister P k V h a x x' ≠ 0) : (CL.CLFun.truncate k P).eval (insertRegister V x) = a.1

The question reported by Hide at level k is the actual first k CL stages.

theorem MIPRE.Introspection.Honest.readout_mul_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 ι) (h : P.SupportedOn V) (y : ι → F) (a : HideLabel F ι) : readout (fun (x : ↥V → F) => (CL.CLFun.truncate k P).eval (insertRegister V x)) y * hideRegister P k V h a = if y = a.1 then hideRegister P k V h a else 0

theorem MIPRE.Introspection.Honest.hideRegister_marginal {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) (y : ι → F) : ∑ yp : (ι → F) × (ι → F), hideRegister P k V h (y, yp) = readout (fun (x : ↥V → F) => (CL.CLFun.truncate k P).eval (insertRegister V x)) y

Forgetting the dual answer and untouched X tail gives exactly the preceding CL prefix.

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

Equations

• MIPRE.Introspection.Honest.hideOp P k h a = MIPRE.Introspection.registerOp MIPRE.Introspection.Honest.univRestriction (MIPRE.Introspection.Honest.hideRegister P k Finset.univ h a)

theorem MIPRE.Introspection.Honest.hideOp_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 : ℕ) (h : P.SupportedOn Finset.univ) : IsPVM (hideOp P k h)

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