The actual adaptive hiding marginal retaining one dual register

theorem MIPRE.Introspection.Honest.matrix_ite_entry_dual {I : Type u_3} {J : Type u_4} (p : Prop) [Decidable p] (M N : Matrix I J ℂ) (i : I) (j : J) : (if p then M else N) i j = if p then M i j else N i j

def MIPRE.Introspection.Honest.dualLabel {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (a : HideLabel F ι) : ReadLabel F ι

Equations

• MIPRE.Introspection.Honest.dualLabel P k a = (a.1, (MIPRE.CL.proj (P.factorOfPrefix k a.1)) a.2.1)

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

Equations

• MIPRE.Introspection.Honest.dualRegister P k V h = MIPRE.fibSum (MIPRE.Introspection.Honest.hideRegister P k V h) (MIPRE.Introspection.Honest.dualLabel P k)

theorem MIPRE.Introspection.Honest.readDualOp_eq_registerDual {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) (p : ReadLabel F ι) : readDualOp P k h (some p) = registerOp univRestriction (dualRegister P k Finset.univ h p)

theorem MIPRE.Introspection.Honest.dualLabel_join {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {S V : Finset ι} (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (h : (CL.CLFun.cons S L next).SupportedOn V) (k : ℕ) (z : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) (a : HideLabel F ι) (ha : (CL.proj (V \ S)) a.1 = a.1) : dualLabel (CL.CLFun.cons S L next) (k + 1) (joinHide S (z, a)) = ((coordinateInsert S) z.1 + a.1, (CL.proj ((next ((coordinateInsert S) z.1)).factorOfPrefix k a.1)) a.2.1)

theorem MIPRE.Introspection.Honest.dualLabel_join_eq_iff {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {S V : Finset ι} (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (h : (CL.CLFun.cons S L next).SupportedOn V) (k : ℕ) (z : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) (a : HideLabel F ι) (ha : (CL.proj (V \ S)) a.1 = a.1) (y yp : ι → F) : dualLabel (CL.CLFun.cons S L next) (k + 1) (joinHide S (z, a)) = (y, yp) ↔ z.1 = (coordinateRestrict S) y ∧ dualLabel (next ((coordinateInsert S) z.1)) k a = ((CL.proj Sᶜ) y, yp)

theorem MIPRE.Introspection.Honest.localRead_sum_dual {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) : ∑ b : Fin (Fintype.card ↥S) → F, localRead L (a, b) = Weyl.synOf Weyl.wZ (⇑(coordinateLinear L)) a

theorem MIPRE.Introspection.Honest.dualRegister_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) (y yp : ι → F) : dualRegister P 0 V h (y, yp) = if y = 0 then Weyl.synOf Weyl.wX (fun (x : ↥V → F) => CLChecks.dualReadout P 0 0 (insertRegister V x)) yp else 0

theorem MIPRE.Introspection.Honest.coarseOp_registerOp {I : Type u_3} {J : Type u_4} {A : Type u_5} {B : Type u_6} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (e : I ≃ J) (f : A → B) (M : A → Matrix J J ℂ) (b : B) : coarseOp f (fun (a : A) => registerOp e (M a)) b = registerOp e (coarseOp f M b)

theorem MIPRE.Introspection.Honest.dualRegister_cons_succ {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {S V : Finset ι} (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (h : (CL.CLFun.cons S L next).SupportedOn V) (k : ℕ) (y yp : ι → F) : dualRegister (CL.CLFun.cons S L next) (k + 1) V h (y, yp) = registerOp (coordinateSplit S V ⋯) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Weyl.synOf Weyl.wZ (⇑(coordinateLinear L)) ((coordinateRestrict S) y)) (dualRegister (next ((CL.proj S) y)) k (V \ S) ⋯ ((CL.proj Sᶜ) y, yp)))

Summing out the earlier dual coordinate leaves precisely its Z readout; the retained prefix still selects the actual continuation.