Binary measurements and the Magic Square grid as permutation observables

The Pauli basis test's honest strategy answers its probe and Magic Square questions with the two-outcome measurements ½(1 ± O) of observables O (MIPRE.LCS.observableToProjector), the observables being Weyl operators on the register and, for the Magic Square, the nine entries of HonestMagicSquare.grid on the register and one ancilla qubit. This file shows:

• encObs_observableToProjector: an answer bit that reads the outcome, possibly flipped, has observable ±O; one that ignores it has observable ±1;
• isSignedPerm_pauliX, isSignedPerm_pauliZ: the qubit Paulis X and Z are signed permutations (unlike Y, which is why the Mermin–Peres grid is not a ZPC strategy);
• isSignedPerm_grid: so are the nine entries of the grid, when A and B are.

Binary measurements

theorem MIPRE.Tailored.univ_zmod_two : Finset.univ = {0, 1}

theorem MIPRE.Tailored.observableSign_eq_bitSign (b : ZMod 2) : LCS.observableSign b = bitSign (decide (b = 1))

theorem MIPRE.Tailored.encObs_observableToProjector {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} (O : R) (enc : ZMod 2 → Fin k → Bool) (i : Fin k) (c : Bool) (h : ∀ (b : ZMod 2), enc b i = (c ^^ decide (b = 1))) : encObs (LCS.observableToProjector O) enc i = bitSign c • O

A bit reading the outcome of ½(1 ± O), flipped by c, has observable (-1)^c O.

theorem MIPRE.Tailored.encObs_observableToProjector_const {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} (O : R) (enc : ZMod 2 → Fin k → Bool) (i : Fin k) (c : Bool) (h : ∀ (b : ZMod 2), enc b i = c) : encObs (LCS.observableToProjector O) enc i = bitSign c • 1

A bit ignoring the outcome of ½(1 ± O) has observable ±1.

The qubit Paulis and the grid

theorem MIPRE.Tailored.pauliX_eq : LCS.Pauli.X = signedPermMatrix (Equiv.swap 0 1) fun (x : Fin 2) => false

theorem MIPRE.Tailored.pauliZ_eq : LCS.Pauli.Z = signedPermMatrix 1 fun (j : Fin 2) => decide (j = 1)

theorem MIPRE.Tailored.isSignedPerm_pauliX : IsSignedPerm LCS.Pauli.X

theorem MIPRE.Tailored.isSignedPerm_pauliZ : IsSignedPerm LCS.Pauli.Z

theorem MIPRE.Tailored.isDiag_pauliZ : LCS.Pauli.Z.IsDiag

theorem MIPRE.Tailored.isSignedPerm_grid {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hA : IsSignedPerm A) (hB : IsSignedPerm B) (j : Fin 9) : IsSignedPerm (Introspection.HonestMagicSquare.grid A B j)

The nine observables of the Magic Square grid are signed permutations when A and B are.