Exact Pauli-X readouts under adaptive coordinate splits

theorem MIPRE.Introspection.Honest.matrix_ite_entry_xsplit {I : Type u_6} {J : Type u_7} (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

theorem MIPRE.Introspection.Honest.synX_split_second {F : Type u_1} {I : Type u_2} {J : Type u_3} {K : Type u_4} {Y : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K] [Fintype Y] [DecidableEq Y] (e : (I → F) ≃ (J → F) × (K → F)) (he : ∀ (z : I → F), Weyl.proj Weyl.wX z = registerOp e (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Weyl.proj Weyl.wX (e z).1) (Weyl.proj Weyl.wX (e z).2))) (f : (K → F) → Y) (y : Y) : Weyl.synOf Weyl.wX (fun (z : I → F) => f (e z).2) y = registerOp e (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (Weyl.synOf Weyl.wX f y))

A spectral readout depending only on the second coordinate factor acts as identity on the first one. The split of each X projector is explicit.

theorem MIPRE.Introspection.Honest.synX_split_first {F : Type u_1} {I : Type u_2} {J : Type u_3} {K : Type u_4} {Y : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K] [Fintype Y] [DecidableEq Y] (e : (I → F) ≃ (J → F) × (K → F)) (he : ∀ (z : I → F), Weyl.proj Weyl.wX z = registerOp e (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Weyl.proj Weyl.wX (e z).1) (Weyl.proj Weyl.wX (e z).2))) (f : (J → F) → Y) (y : Y) : Weyl.synOf Weyl.wX (fun (z : I → F) => f (e z).1) y = registerOp e (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Weyl.synOf Weyl.wX f y) 1)

def MIPRE.Introspection.Honest.ambientIndexSplit {ι : Type u_6} [Fintype ι] [DecidableEq ι] (V : Finset ι) : ι ≃ ↥V ⊕ ↥Vᶜ

Equations

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

theorem MIPRE.Introspection.Honest.trDot_ambientSplit {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (V : Finset ι) (x y : ι → F) : Weyl.trDot x y = Weyl.trDot ((ambientSplit V) x).1 ((ambientSplit V) y).1 + Weyl.trDot ((ambientSplit V) x).2 ((ambientSplit V) y).2

theorem MIPRE.Introspection.Honest.pauliX_ambientSplit {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (V : Finset ι) (x : ι → F) : Weyl.proj Weyl.wX x = registerOp (ambientSplit V) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Weyl.proj Weyl.wX ((ambientSplit V) x).1) (Weyl.proj Weyl.wX ((ambientSplit V) x).2))

theorem MIPRE.Introspection.Honest.insertRegister_ambientSplit_snd {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (V : Finset ι) (x : ι → F) : insertRegister Vᶜ ((ambientSplit V) x).2 = (CL.proj Vᶜ) x

theorem MIPRE.Introspection.Honest.dualReadout_prefix_split {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ι : Type u_6} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (h : P.SupportedOn Finset.univ) (k : ℕ) (y yp : ι → F) : Weyl.synOf Weyl.wX (CLChecks.dualReadout P k y) yp = registerOp (ambientSplit (CLChecks.prefixRegister P k y)) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (Weyl.synOf Weyl.wX (fun (x : ↥(CLChecks.prefixRegister P k y)ᶜ → F) => CLChecks.dualReadout P k y (insertRegister (CLChecks.prefixRegister P k y)ᶜ x)) yp))

The selected dual readout has no action on preceding prefix registers.

theorem MIPRE.Introspection.Honest.dualReadout_tail_split {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ι : Type u_6} [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) : Weyl.synOf Weyl.wX (fun (x : ↥V → F) => CLChecks.dualReadout (CL.CLFun.cons S L next) (k + 1) y (insertRegister V x)) yp = registerOp (coordinateSplit S V ⋯) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (Weyl.synOf Weyl.wX (fun (x : ↥(V \ S) → F) => CLChecks.dualReadout (next ((CL.proj S) y)) k ((CL.proj Sᶜ) y) (insertRegister (V \ S) x)) yp))

The dual readout at any later stage ignores the first register.