Documentation

MIPRE.Foundations.Introspection.ConditionalNormalizerIdealMirror

Exact EPR mirrors of the concrete honest hiding operators #

Every local Weyl readout is symmetric in characteristic two. The adaptive construction, its coordinate transports, and its coarse sums preserve that property, even when later measurements depend on earlier outcomes.

source
theorem MIPRE.Introspection.Honest.synOf_transpose_of_symmetric {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] (w : (ι → F) → Matrix (ι → F) (ι → F) ℂ) (hw : ∀ (x : ι → F), (w x).transpose = w x) {J : Type u_3} [DecidableEq J] (f : (ι → F) → J) (j : J) :
(Weyl.synOf w f j).transpose = Weyl.synOf w f j
source
theorem MIPRE.Introspection.Honest.localRead_transpose {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) × (Fin (Fintype.card ↥S) → F)) :
(localRead L a).transpose = localRead L a
source
theorem MIPRE.Introspection.Honest.stopHide_transpose {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 ι) :
(stopHide P V a).transpose = stopHide P V a
source
theorem MIPRE.Introspection.Honest.hideRegister_transpose {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 ι) :
(hideRegister P k V h a).transpose = hideRegister P k V h a

Adaptive branches preserve symmetry outcome by outcome; no comparison between operators in different branches is required.

source
theorem MIPRE.Introspection.Honest.hideOp_transpose {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 ι) :
(hideOp P k h a).transpose = hideOp P k h a
source
theorem MIPRE.Introspection.Honest.hideCoarseOp_transpose {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) (i : Option (HideLabel F ι)) :
(hideCoarseOp P k h i).transpose = hideCoarseOp P k h i
source
theorem MIPRE.Introspection.Honest.hidingPrefixOp_transpose {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : Option (ι → F)) :
(hidingPrefixOp P k y).transpose = hidingPrefixOp P k y
source
theorem MIPRE.Introspection.Honest.hideCoarseOp_epr_mirror {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) (i : Option (HideLabel F ι)) :
(aOp (hideCoarseOp P k h i)).mulVec (registerEPR (ι → F)) = (bOp (hideCoarseOp P k h i)).mulVec (registerEPR (ι → F))