Signed permutations built by the honest introspection strategy

Phase 3 of planning/aldous-lyons-track.md (issue #281) shows that the honest strategy of the introspection verifier is a ZPC strategy: all its observables are signed permutation matrices, the readable ones diagonal. The strategy is assembled from Weyl operators and classical read-outs, so the closure lemmas are:

• isSignedPerm_wX, isSignedPerm_wZ, isDiag_wZ: the shift wX a is a permutation matrix, the phase wZ b a ±1 diagonal;
• isSignedPerm_blockDiag: a block-diagonal matrix with signed-permutation blocks is one;
• isSignedPerm_controlled: so is a controlled sum ∑_z readout f z ⊗ U z, the operator applying U (f i) on the second factor when the first is in the basis state i; isDiag_controlled when the blocks are diagonal.

Signs

theorem MIPRE.Tailored.sgn_eq_bitSign (x : ZMod 2) : sgn x = bitSign (decide (x = 1))

The sign of an element of ZMod 2 is the sign of its bit.

Weyl operators

theorem MIPRE.Tailored.wX_eq_signedPermMatrix {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (a : n → F) : Weyl.wX a = signedPermMatrix (Equiv.addRight a) fun (x : n → F) => false

The shift wX a is the permutation matrix of the translation by a.

theorem MIPRE.Tailored.isSignedPerm_wX {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (a : n → F) : IsSignedPerm (Weyl.wX a)

theorem MIPRE.Tailored.wZ_eq_diagonal_bitSign {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (b : n → F) : Weyl.wZ b = Matrix.diagonal fun (i : n → F) => bitSign (decide (Weyl.trDot b i = 1))

The phase wZ b is a ±1 diagonal.

theorem MIPRE.Tailored.isSignedPerm_wZ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (b : n → F) : IsSignedPerm (Weyl.wZ b)

theorem MIPRE.Tailored.isDiag_wZ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (b : n → F) : (Weyl.wZ b).IsDiag

Linear data processing

Paper II, Corollary II:2938 (cor:linear_data_processed_PVM_is_ZPC_and_left_multiplication), in the form the honest strategy uses it: an F₂-linear bit φ of the outcome of the eigenbasis measurement of a Weyl family w has observable w c, where c represents φ through the trace form. Every F₂-linear functional is such a trDot · c (exists_trDotL_eq), since the trace form is nondegenerate.

noncomputable def MIPRE.Tailored.trDotDual {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] : (n → F) →ₗ[ZMod 2] Module.Dual (ZMod 2) (n → F)

The trace form as a linear map to the dual.

Equations

• MIPRE.Tailored.trDotDual = { toFun := MIPRE.Weyl.trDotL, map_add' := ⋯, map_smul' := ⋯ }

theorem MIPRE.Tailored.exists_trDotL_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (φ : Module.Dual (ZMod 2) (n → F)) : ∃ (c : n → F), Weyl.trDotL c = φ

The trace form is nondegenerate: every F₂-linear functional on F_q^n is trDot · c for some c.

theorem MIPRE.Tailored.encObs_proj_trDot {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (w : (n → F) → Matrix (n → F) (n → F) ℂ) {k : ℕ} (c : Fin k → n → F) (i : Fin k) : encObs (Weyl.proj w) (fun (e : n → F) (j : Fin k) => decide (Weyl.trDot e (c j) = 1)) i = w (c i)

The observable of the bit trDot · c of the eigenbasis measurement of w is w c.

theorem MIPRE.Tailored.exists_encObs_proj_linear {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] (w : (n → F) → Matrix (n → F) (n → F) ℂ) {k : ℕ} (φ : Fin k → Module.Dual (ZMod 2) (n → F)) (i : Fin k) : ∃ (c : n → F), encObs (Weyl.proj w) (fun (e : n → F) (j : Fin k) => decide ((φ j) e = 1)) i = w c

Linear data processing (II:2938): the observable of an F₂-linear bit of the outcome of the eigenbasis measurement of w is an operator of the family.

theorem MIPRE.Tailored.isSignedPerm_encObs_xProj {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {k : ℕ} (φ : Fin k → Module.Dual (ZMod 2) (n → F)) (i : Fin k) : IsSignedPerm (encObs Weyl.xProj (fun (e : n → F) (j : Fin k) => decide ((φ j) e = 1)) i)

The X-basis measurement's linear bits are permutation matrices.

theorem MIPRE.Tailored.isSignedPerm_encObs_zProj {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : Type u_2} [Fintype n] [DecidableEq n] {k : ℕ} (enc : (n → F) → Fin k → Bool) (i : Fin k) : IsSignedPerm (encObs Weyl.zProj enc i) ∧ (encObs Weyl.zProj enc i).IsDiag

The Z-basis measurement's bits, linear or not, are ±1 diagonals.

Block-diagonal and controlled sums

def MIPRE.Tailored.blockDiag {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] (V : Ω → Matrix Ω' Ω' ℂ) : Matrix (Ω × Ω') (Ω × Ω') ℂ

The block-diagonal matrix with blocks V i.

Equations

• MIPRE.Tailored.blockDiag V = Matrix.of fun (p q : Ω × Ω') => if p.1 = q.1 then V p.1 p.2 q.2 else 0

theorem MIPRE.Tailored.isSignedPerm_blockDiag {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] (V : Ω → Matrix Ω' Ω' ℂ) (hV : ∀ (i : Ω), IsSignedPerm (V i)) : IsSignedPerm (blockDiag V)

A block-diagonal matrix with signed-permutation blocks is a signed permutation.

theorem MIPRE.Tailored.isDiag_blockDiag {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] (V : Ω → Matrix Ω' Ω' ℂ) (hV : ∀ (i : Ω), (V i).IsDiag) : (blockDiag V).IsDiag

theorem MIPRE.Tailored.controlled_eq_blockDiag {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] [Fintype Ω] {K : Type u_3} [Fintype K] [DecidableEq K] (f : Ω → K) (U : K → Matrix Ω' Ω' ℂ) : ∑ z : K, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Introspection.readout f z) (U z) = blockDiag fun (i : Ω) => U (f i)

A controlled sum is block diagonal.

theorem MIPRE.Tailored.isSignedPerm_controlled {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] [Fintype Ω] {K : Type u_3} [Fintype K] [DecidableEq K] (f : Ω → K) (U : K → Matrix Ω' Ω' ℂ) (hU : ∀ (z : K), IsSignedPerm (U z)) : IsSignedPerm (∑ z : K, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Introspection.readout f z) (U z))

A controlled sum of signed permutations is a signed permutation.

theorem MIPRE.Tailored.isDiag_controlled {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] [Fintype Ω] {K : Type u_3} [Fintype K] [DecidableEq K] (f : Ω → K) (U : K → Matrix Ω' Ω' ℂ) (hU : ∀ (z : K), (U z).IsDiag) : (∑ z : K, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Introspection.readout f z) (U z)).IsDiag

theorem MIPRE.Tailored.encObs_controlled {Ω : Type u_1} {Ω' : Type u_2} [DecidableEq Ω] [DecidableEq Ω'] [Fintype Ω] {K : Type u_3} [Fintype K] [DecidableEq K] [Fintype Ω'] {Λ : Type u_4} [Fintype Λ] {k : ℕ} (f : Ω → K) (Q : K → Λ → Matrix Ω' Ω' ℂ) (enc : K × Λ → Fin k → Bool) (i : Fin k) : encObs (fun (za : K × Λ) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Introspection.readout f za.1) (Q za.1 za.2)) enc i = ∑ z : K, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Introspection.readout f z) (encObs (Q z) (fun (a : Λ) => enc (z, a)) i)

The bit observables of a controlled measurement are controlled bit observables: if the measurement is readout f z ⊗ Q z a at the outcome (z, a), the observable of a bit is the controlled sum of the bit observables of the Q z.

Relabellings and ancillas

theorem MIPRE.Tailored.encObs_submatrix {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {Λ : Type u_3} [Fintype Λ] {k : ℕ} (P : Λ → Matrix Ω Ω ℂ) (e : Ω' → Ω) (enc : Λ → Fin k → Bool) (i : Fin k) : encObs (fun (a : Λ) => (P a).submatrix e e) enc i = (encObs P enc i).submatrix e e

Bit observables commute with a relabelling of the space.

theorem MIPRE.Tailored.encObs_kronecker_one {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {Λ : Type u_3} [Fintype Λ] {k : ℕ} (P : Λ → Matrix Ω Ω ℂ) (enc : Λ → Fin k → Bool) (i : Fin k) : encObs (fun (a : Λ) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P a) 1) enc i = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (encObs P enc i) 1

Bit observables commute with adding an ancilla on which the measurement is the identity.

theorem MIPRE.Tailored.IsSignedPerm.kronecker_one {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {M : Matrix Ω Ω ℂ} (hM : IsSignedPerm M) : IsSignedPerm (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1)

theorem MIPRE.Tailored.IsSignedPerm.submatrix_equiv {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {M : Matrix Ω Ω ℂ} (hM : IsSignedPerm M) (e : Ω' ≃ Ω) : IsSignedPerm (M.submatrix ⇑e ⇑e)

theorem MIPRE.Tailored.isDiag_submatrix_equiv {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {M : Matrix Ω Ω ℂ} (hM : M.IsDiag) (e : Ω' ≃ Ω) : (M.submatrix ⇑e ⇑e).IsDiag

theorem MIPRE.Tailored.isDiag_kronecker_one {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {M : Matrix Ω Ω ℂ} (hM : M.IsDiag) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1).IsDiag