Pauli-X projectors under the honest register split

The stopping measurement in Hide uses the X basis of the active register. These identities expose its tensor factors in the coordinate split used by the adaptive CL recursion.

theorem MIPRE.Introspection.Honest.pauliX_entry {F : Type u_1} {I : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype I] [DecidableEq I] (e x y : I → F) : Weyl.proj Weyl.wX e x y = (↑(Fintype.card (I → F)))⁻¹ * sgn (Weyl.trDot (x + y) e)

theorem MIPRE.Introspection.Honest.pauliX_split {F : Type u_1} {I : Type u_2} {J : Type u_3} {K : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K] (e : (I → F) ≃ (J → F) × (K → F)) (hadd : ∀ (a b : I → F), e (a + b) = ((e a).1 + (e b).1, (e a).2 + (e b).2)) (hdot : ∀ (a b : I → F), Weyl.trDot a b = Weyl.trDot (e a).1 (e b).1 + Weyl.trDot (e a).2 (e b).2) (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))

Any additive split preserving the coordinate pairing splits the X spectral projector.

noncomputable def MIPRE.Introspection.Honest.coordinateIndexSplit {ι : Type u_5} [DecidableEq ι] (S V : Finset ι) (h : S ⊆ V) : ↥V ≃ Fin (Fintype.card ↥S) ⊕ ↥(V \ S)

The coordinate partition underlying coordinateSplit, on index types.

Equations

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

theorem MIPRE.Introspection.Honest.trDot_coordinateSplit {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (S V : Finset ι) (h : S ⊆ V) (x y : ↥V → F) : Weyl.trDot x y = Weyl.trDot ((coordinateSplit S V h) x).1 ((coordinateSplit S V h) y).1 + Weyl.trDot ((coordinateSplit S V h) x).2 ((coordinateSplit S V h) y).2

theorem MIPRE.Introspection.Honest.pauliX_coordinateSplit {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (S V : Finset ι) (h : S ⊆ V) (z : ↥V → F) : Weyl.proj Weyl.wX z = registerOp (coordinateSplit S V h) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Weyl.proj Weyl.wX ((coordinateSplit S V h) z).1) (Weyl.proj Weyl.wX ((coordinateSplit S V h) z).2))

The concrete active-register X projector is the tensor product of the current register and untouched-tail X projectors in the honest CL coordinate split.