Exact Pauli observables from a simultaneous pair measurement

Blueprint lem:qld-exact-paulis, the part of it that is exact: given a projective measurement S whose outcomes are pairs (g_X, g_Z) and a map cd sending an outcome to a vector of F_q^n, the appendix builds binary observables on the enlarged space dA (x) (C^q)^{(x) n} which satisfy the generalized Pauli relations with no error term at all. This file is that construction and those relations.

Nothing here is approximate, and nothing here mentions the game: every statement is an identity in the algebra, with IsPVMIn S and IsWeylFamily w the only hypotheses. That is the point --- the blueprint's proof paragraph says exactness comes "from projectivity of the simultaneous measurement together with the group law of the Pauli basis", and this file is the formalization of exactly that sentence. thm:linearity is not used.

Over a ⋆-algebra

Stated in a bipartite model (Phase 5 of planning/mipco-track.md): the pair measurement is a projective measurement S : G × G → R in any ⋆-algebra R --- in use, a player's algebra of a model, where IsPVMIn is what the strategy's projectivity supplies --- and the operators the appendix writes on dA (x) (C^q)^{(x) n} are the F_q^n × F_q^n matrices over R, the register the new outer index: an element X of R tensored with a matrix P of scalars on the register is smulKron X P (MIPRE/Foundations/AncillaModel.lean), the adjoint is star, and a product of two such tensors is taken factorwise by smulKron_mul. The matrix statements of the earlier version are the instances R = Matrix dA dA ℂ, up to the register-outer layout of smulKron. Every statement is still an exact identity, and nothing needs the algebra to be finite-dimensional.

The construction

Write pi for one of the two projections (g_X, g_Z) |→ g_W. Then

• sCoarse S pi g is the W-marginal S^W_g, a projective measurement by IsPVMIn.coarse;
• mTilde is the appendix's eq:tilde_M, M~^{W,u}_a = sum_g S^W_g (x) tau^W_{cd(g) . u + a}(u), where tau^W_c(u) is the syndrome projector MIPRE.Weyl.syn w u c --- the level set of the pairing with u --- so that mTilde is a projective measurement with outcomes in F_q;
• wTilde is eq:def-tildewj, the binary observable W~^e(u) = sum_a (-1)^{tr(e a)} M~^{W,u}_a, at a field element e (the appendix takes e in a self-dual basis of F_q over F_2, which this file does not need).

The one identity everything follows from

wTilde_eq: the observable factorizes,

W~^e(u) = pvmObs S (p |→ (-1)^{tr(e (cd (pi p) . u))}) (x) w (e . u),

a signed sum of the pair measurement tensor a genuine Weyl operator. The F_q-valued syndrome label is what makes this work: summing the syndrome projectors against the character of a reassembles the Weyl operator on the line r |→ r . u (MIPRE.Weyl.eq_sum_proj), and the cd(g) . u shift becomes the sign the first factor carries.

Self-adjointness (wTilde_conjTranspose) and involutivity (wTilde_mul_self) are then the pvmObs calculus of MIPRE/Foundations/Measurement.lean on the left factor and the group law on the right. The twisted commutation (wTilde_mul_wTilde) is the same: the two left factors are weightings of one projective measurement, so they commute exactly (IsPVMIn.pvmObs_comm), and the whole phase comes from the right factors' MIPRE.Weyl.wX_mul_wZ.

A repair carried over from the paper

The pinned paper's display for the commutation relation used to split into e != e' (claiming exact commutation) and e = e' (a phase). That is false: self-duality gives tr(e_j e_{j'}) = delta_{j j'}, but tr(e_j e_{j'} c) need not vanish for c outside F_2, and the quantity in the exponent is e_j e_{j'} (u . v) with u . v an arbitrary field element. The paper now states the general phase, and wTilde_mul_wTilde below is that general phase --- with no case split, and with no reference to a basis, since the relation holds for every pair of field elements.

Two small bilinearity facts

trDot_smul of MIPRE/Foundations/Weyl.lean pulls a scalar out of the left argument of the form. Both of the following pull one out of the right, which is what the two observables' arguments need.

theorem MIPRE.QLD.dotF_smul_right {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (r : F) (u v : n → F) : Weyl.dotF u (r • v) = r * Weyl.dotF u v

Scaling the right argument of the F_q-valued pairing pulls the scalar out.

theorem MIPRE.QLD.trDot_smul_smul {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (r r' : F) (u v : n → F) : Weyl.trDot (r • u) (r' • v) = (Algebra.trace (ZMod 2) F) (r * r' * Weyl.dotF u v)

The form of two scaled vectors. This is the exponent of the phase in wTilde_mul_wTilde, and the reason it is symmetric in the two scalars.

theorem MIPRE.QLD.trDot_smul_right {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (r : F) (u v : n → F) : Weyl.trDot u (r • v) = (Algebra.trace (ZMod 2) F) (r * Weyl.dotF u v)

The form against a scaled vector, in the shape the phase function below is written in.

Bilinearity of the tensor sign over finite sums

The tensor sign is smulKron, and every displayed calculation below moves a sum across it, on either side. These are smulKron_sum_left and smulKron_sum_right of MIPRE/Foundations/AncillaModel.lean at the register of the construction; a scalar moves across it in the same way (smulKron_smul_left, and smulKron_smul_right there).

theorem MIPRE.QLD.sum_kron {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] {iota : Type u_5} (s : Finset iota) (A : iota → R) (B : Matrix (n → F) (n → F) ℂ) : smulKron (∑ x ∈ s, A x) B = ∑ x ∈ s, smulKron (A x) B

(sum_x A x) (x) B = sum_x (A x (x) B).

theorem MIPRE.QLD.kron_sum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] {iota : Type u_5} (s : Finset iota) (A : R) (B : iota → Matrix (n → F) (n → F) ℂ) : smulKron A (∑ x ∈ s, B x) = ∑ x ∈ s, smulKron A (B x)

A (x) (sum_x B x) = sum_x (A (x) B x).

theorem MIPRE.QLD.smulKron_smul_left {R : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] {α : Type u_5} (c : ℂ) (X : R) (P : Matrix α α ℂ) : smulKron (c • X) P = c • smulKron X P

(c X) (x) P = c (X (x) P).

The marginals of a pair measurement

def MIPRE.QLD.sCoarse {G : Type u_3} [Fintype G] [DecidableEq G] {R : Type u_4} [Ring R] (S : G × G → R) (pi : G × G → G) (g : G) : R

A coarse-graining of a measurement along a map on its outcomes. The two marginals of the simultaneous pair measurement are this at Prod.fst and Prod.snd; IsPVMIn.coarse is what makes each of them projective.

Equations

• MIPRE.QLD.sCoarse S pi g = ∑ p : G × G with pi p = g, S p

theorem MIPRE.QLD.isPVM_sCoarse {G : Type u_3} [Fintype G] [DecidableEq G] {R : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] {S : G × G → R} (hS : IsPVMIn S) (pi : G × G → G) : IsPVMIn (sCoarse S pi)

theorem MIPRE.QLD.sum_sCoarse_kron {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {G : Type u_3} [Fintype G] [DecidableEq G] {R : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] {S : G × G → R} (pi : G × G → G) (T : G → Matrix (n → F) (n → F) ℂ) : ∑ g : G, smulKron (sCoarse S pi g) (T g) = ∑ p : G × G, smulKron (S p) (T (pi p))

Summing a family against the marginals is summing it against the measurement, the label read off through the projection. The fibrewise sum, stated once because both the definition of mTilde and its factorization use it.

The measurement and the observable

noncomputable def MIPRE.QLD.mTilde {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {G : Type u_3} [Fintype G] [DecidableEq G] {R : Type u_4} [Ring R] [Algebra ℂ R] (S : G × G → R) (pi : G × G → G) (cd : G → n → F) (w : (n → F) → Matrix (n → F) (n → F) ℂ) (u : n → F) (a : F) : Matrix (n → F) (n → F) R

The appendix's eq:tilde_M. M~^{W,u}_a = sum_g S^W_g (x) tau^W_{cd(g) . u - a}(u); in characteristic two the subtraction is the addition.

Equations

• MIPRE.QLD.mTilde S pi cd w u a = ∑ g : G, MIPRE.smulKron (MIPRE.QLD.sCoarse S pi g) (MIPRE.Weyl.syn w u (MIPRE.Weyl.dotF (cd g) u + a))

theorem MIPRE.QLD.mTilde_eq_sum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {G : Type u_3} [Fintype G] [DecidableEq G] {R : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] (S : G × G → R) (pi : G × G → G) (cd : G → n → F) (w : (n → F) → Matrix (n → F) (n → F) ℂ) (u : n → F) (a : F) : mTilde S pi cd w u a = ∑ p : G × G, smulKron (S p) (Weyl.syn w u (Weyl.dotF (cd (pi p)) u + a))

The same sum indexed by the pair outcomes, which is the form the factorization starts from.

noncomputable def MIPRE.QLD.cdPhase {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] {G : Type u_3} (pi : G × G → G) (cd : G → n → F) (e : F) (u : n → F) : G × G → ZMod 2

The phase the first tensor factor carries, tr(e (cd(pi p) . u)).

Equations

• MIPRE.QLD.cdPhase pi cd e u p = (Algebra.trace (ZMod 2) F) (e * MIPRE.Weyl.dotF (cd (pi p)) u)

noncomputable def MIPRE.QLD.wTilde {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {G : Type u_3} [Fintype G] [DecidableEq G] {R : Type u_4} [Ring R] [Algebra ℂ R] (S : G × G → R) (pi : G × G → G) (cd : G → n → F) (w : (n → F) → Matrix (n → F) (n → F) ℂ) (e : F) (u : n → F) : Matrix (n → F) (n → F) R

The appendix's eq:def-tildewj. The binary observable obtained from mTilde by the character of the field element e.

Equations

• MIPRE.QLD.wTilde S pi cd w e u = ∑ a : F, MIPRE.sgn ((Algebra.trace (ZMod 2) F) (e * a)) • MIPRE.QLD.mTilde S pi cd w u a

The factorization

The whole content of the exactness claim.

theorem MIPRE.QLD.wTilde_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {G : Type u_3} [Fintype G] [DecidableEq G] {R : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] (S : G × G → R) (pi : G × G → G) (cd : G → n → F) (w : (n → F) → Matrix (n → F) (n → F) ℂ) (e : F) (u : n → F) : wTilde S pi cd w e u = smulKron (pvmObs S fun (p : G × G) => sgn (cdPhase pi cd e u p)) (w (e • u))

The observable factorizes as a signed sum of the pair measurement tensor a Weyl operator: W~^e(u) = pvmObs S ((-1)^{cdPhase}) (x) w (e . u).

The proof runs the appendix's displayed calculation backwards. Expanding w (e . u) in its own spectral projectors (eq_sum_proj, which needs no group law) and grouping the eigenvalue patterns by their pairing with u turns the right-hand side into a double sum over outcomes p and syndromes a; the left-hand side is the same double sum after the substitution a |→ cd(pi p) . u + a, which for each fixed p is a bijection of F_q.

The Pauli relations, exactly

theorem MIPRE.QLD.wTilde_conjTranspose {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {G : Type u_3} [Fintype G] [DecidableEq G] {R : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] {S : G × G → R} {pi : G × G → G} {cd : G → n → F} {w : (n → F) → Matrix (n → F) (n → F) ℂ} [StarModule ℂ R] (hS : IsPVMIn S) (hw : Weyl.IsWeylFamily w) (e : F) (u : n → F) : star (wTilde S pi cd w e u) = wTilde S pi cd w e u

The observable is self-adjoint.

theorem MIPRE.QLD.wTilde_mul_self {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {G : Type u_3} [Fintype G] [DecidableEq G] {R : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] {S : G × G → R} {pi : G × G → G} {cd : G → n → F} {w : (n → F) → Matrix (n → F) (n → F) ℂ} (hS : IsPVMIn S) (hw : Weyl.IsWeylFamily w) (e : F) (u : n → F) : wTilde S pi cd w e u * wTilde S pi cd w e u = 1

The observable squares to the identity, so it is a genuine +-1-valued observable. The left factor squares to one because the signs do and the measurement is projective; the right factor because w (e . u) w (e . u) = w (e . u + e . u) = w 0 = 1.

theorem MIPRE.QLD.wTilde_mul_wTilde {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {G : Type u_3} [Fintype G] [DecidableEq G] {R : Type u_4} [Ring R] [StarRing R] [Algebra ℂ R] {S : G × G → R} {cd : G → n → F} (hS : IsPVMIn S) {pi pi' : G × G → G} (e e' : F) (u v : n → F) : wTilde S pi cd Weyl.wX e u * wTilde S pi' cd Weyl.wZ e' v = sgn ((Algebra.trace (ZMod 2) F) (e * e' * Weyl.dotF u v)) • (wTilde S pi' cd Weyl.wZ e' v * wTilde S pi cd Weyl.wX e u)

The exact twisted commutation relation. X~^e(u) Z~^{e'}(v) = (-1)^{tr(e e' (u . v))} Z~^{e'}(v) X~^e(u), for every pair of field elements and every pair of vectors, with no case split.

Both sides factorize by wTilde_eq. The left factors are weightings of the same projective measurement S, so they commute exactly whatever the two projections pi and pi' are (IsPVMIn.pvmObs_comm) --- this is where projectivity of the simultaneous measurement is used, and it is the only place. The entire phase is then the Weyl families' own (-1)^{tr((e . u) . (e' . v))}, which trDot_smul_smul rewrites as the displayed exponent.