The exact Pauli measurement at an arbitrary probe

lem:qld-exact-paulis gives M~^{W, ind_m(u)}, the exact Pauli measurement at the low-degree encoding of a point. lem:qld-pauli-selfcons --- the self-consistency the swap isometry's item 1 needs --- is stated at a uniform u-tilde in F_q^M, and that is not a point's encoding: the encodings are a tiny subset of F_q^M. Getting the two confused is the omission that created that node in the first place, so the two probes are kept apart here by name.

mTildeAnc is the measurement at an arbitrary probe. Nothing about it is new --- the generic mTilde of ExactPauli.lean already takes the probe as an argument, and mTildeAt is its value at indVec u --- but the chain of lem:qld-pauli-selfcons runs at a probe that is not of that form, and every statement it makes has to be available there. mTildeAt_eq_mTildeAnc is the one place the two meet.

Stated in a bipartite model

Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The pair measurement is the SA of a SimulPair M S K ι δ, a projective measurement in the first algebra 𝒜' of the model K, so mTildeAnc is, as mTildeAt is, a matrix over 𝒜' on the register Anc F m (register outer, smulKron): projective in the sense of IsPVMIn, and conjugated by the swap unitary swapA and its adjoint star swapA to the bare syndrome projector smulKron 1 (syn …).

noncomputable def MIPRE.QLD.SimulPair.mTildeAnc {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {K : BipartiteModel 𝒞' 𝒜' ℬ'} {ι : (M.reg (Anc F m)).Embedding K} {δ : ℝ} (P : SimulPair M S K ι δ) (W : Bas) (v : Anc F m) (a : F) : Matrix (Anc F m) (Anc F m) 𝒜'

The paper's M~^{W, u-tilde}_a at an arbitrary probe: a matrix over K's first algebra on the register. mTildeAt is this at ind_m(u).

Equations

• P.mTildeAnc W v a = MIPRE.QLD.mTilde P.SA.op (MIPRE.QLD.PolyPair.proj W) MIPRE.QLD.cubeData (MIPRE.QLD.weylOf W) v a

theorem MIPRE.QLD.SimulPair.isPVM_mTildeAnc {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {K : BipartiteModel 𝒞' 𝒜' ℬ'} {ι : (M.reg (Anc F m)).Embedding K} {δ : ℝ} (P : SimulPair M S K ι δ) [StarModule ℂ 𝒜'] (W : Bas) (v : Anc F m) : IsPVMIn (P.mTildeAnc W v)

It is a projective measurement, at every probe.

theorem MIPRE.QLD.SimulPair.mTildeAt_eq_mTildeAnc {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {K : BipartiteModel 𝒞' 𝒜' ℬ'} {ι : (M.reg (Anc F m)).Embedding K} {δ : ℝ} (P : SimulPair M S K ι δ) (W : Bas) (u : LIDT.Point F m) : P.mTildeAt W u = P.mTildeAnc W (LowDegree.indVec u)

At a point's encoding it is the measurement lem:qld-exact-paulis speaks of. The only place the two probes meet.

theorem MIPRE.QLD.SimulPair.swapU_conj_mTildeAnc {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {𝒞' : Type u_5} {𝒜' : Type u_6} {ℬ' : Type u_7} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {hm : m ∣ Fintype.card F} {M : BipartiteModel 𝒞 𝒜 ℬ} {S : M.ProjStrat (qldGame hm)} {K : BipartiteModel 𝒞' 𝒜' ℬ'} {ι : (M.reg (Anc F m)).Embedding K} {δ : ℝ} (P : SimulPair M S K ι δ) [StarModule ℂ 𝒜'] (W : Bas) (v : Anc F m) (a : F) : P.swapA * P.mTildeAnc W v a * star P.swapA = smulKron 1 (Weyl.syn (weylOf W) v a)

Display eq:qld-unitary-6 at an arbitrary probe. Conjugation by the swap unitary strips the pair measurement off the exact Pauli measurement whatever the probe, since the cancellation is between the outcome's shift and the conjugation's, and both are written with the same pairing.