Documentation

MIPRE.Foundations.Introspection.HonestMagicSquare

The Magic Square extension of an arbitrary anticommuting pair #

This is the concrete operator construction needed by the honest Pauli test. It adds one qubit and retains the original observables at cells zero and four. The row and column identities use the actual Magic Square layout and parity. No game completeness statement is assumed.

source
def MIPRE.Introspection.HonestMagicSquare.cellIndex (c : Fin LCS.MagicSquare.layout.r) (j : Fin 3) :
Fin 9

The actual Magic Square cell, with its fixed nine-cell carrier exposed.

Equations
Instances For
    source
    theorem MIPRE.Introspection.HonestMagicSquare.observable_kronecker {I : Type u_1} [Fintype I] [DecidableEq I] {J : Type u_2} [Fintype J] [DecidableEq J] {A : Matrix I I ℂ} {B : Matrix J J ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) :
    LCS.IsObservable (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B)
    source
    theorem MIPRE.Introspection.HonestMagicSquare.observable_one {I : Type u_1} [Fintype I] [DecidableEq I] :
    LCS.IsObservable 1
    source
    theorem MIPRE.Introspection.HonestMagicSquare.observable_mul {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hc : Commute A B) :
    LCS.IsObservable (A * B)
    source
    theorem MIPRE.Introspection.HonestMagicSquare.tensor_commute {I : Type u_1} [Fintype I] {A B : Matrix I I ℂ} {C D : Matrix (Fin 2) (Fin 2) ℂ} (hAB : Commute A B) (hCD : Commute C D) :
    Commute (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A C) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) B D)
    source
    theorem MIPRE.Introspection.HonestMagicSquare.tensor_anticommute {I : Type u_1} [Fintype I] {A B : Matrix I I ℂ} {C D : Matrix (Fin 2) (Fin 2) ℂ} (hAB : A * B = -(B * A)) (hCD : C * D = -(D * C)) :
    Commute (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A C) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) B D)
    source
    def MIPRE.Introspection.HonestMagicSquare.grid {I : Type u_1} [Fintype I] [DecidableEq I] (A B : Matrix I I ℂ) :
    Fin 9 → Matrix (I × Fin 2) (I × Fin 2) ℂ

    The nine observables, on the original space tensor one additional qubit.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.Introspection.HonestMagicSquare.grid_zero {I : Type u_1} [Fintype I] [DecidableEq I] (A B : Matrix I I ℂ) :
      grid A B 0 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A 1
      source
      @[simp]
      theorem MIPRE.Introspection.HonestMagicSquare.grid_four {I : Type u_1} [Fintype I] [DecidableEq I] (A B : Matrix I I ℂ) :
      grid A B 4 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) B 1
      source
      theorem MIPRE.Introspection.HonestMagicSquare.ZX_anticomm :
      LCS.Pauli.Z * LCS.Pauli.X = -(LCS.Pauli.X * LCS.Pauli.Z)
      source
      theorem MIPRE.Introspection.HonestMagicSquare.grid_isObservable {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) (j : Fin 9) :
      LCS.IsObservable (grid A B j)
      source
      theorem MIPRE.Introspection.HonestMagicSquare.first_second_commute {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hAB : A * B = -(B * A)) (c : Fin LCS.MagicSquare.layout.r) :
      Commute (grid A B (cellIndex c 0)) (grid A B (cellIndex c 1))

      The first two observables in each actual row or column commute.

      source
      theorem MIPRE.Introspection.HonestMagicSquare.third_eq {I : Type u_1} [Fintype I] [DecidableEq I] (A B : Matrix I I ℂ) (c : Fin LCS.MagicSquare.layout.r) :
      grid A B (cellIndex c 2) = (-1) ^ (LCS.MagicSquare.game.b c).val • (grid A B (cellIndex c 0) * grid A B (cellIndex c 1))

      The last cell is the signed product of the first two cells.

      source
      theorem MIPRE.Introspection.HonestMagicSquare.cells_commute {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hAB : A * B = -(B * A)) (c : Fin LCS.MagicSquare.layout.r) (s t : Fin 3) :
      Commute (grid A B (cellIndex c s)) (grid A B (cellIndex c t))
      source
      theorem MIPRE.Introspection.HonestMagicSquare.row_product {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) (c : Fin LCS.MagicSquare.layout.r) :
      grid A B (cellIndex c 0) * grid A B (cellIndex c 1) * grid A B (cellIndex c 2) = (-1) ^ (LCS.MagicSquare.game.b c).val • 1

      Every row has even parity and the last column has odd parity.

      source
      noncomputable def MIPRE.Introspection.HonestMagicSquare.variableOp {I : Type u_1} [Fintype I] [DecidableEq I] (A B : Matrix I I ℂ) (j : Fin 9) (b : ZMod 2) :
      Matrix (I × Fin 2) (I × Fin 2) ℂ

      The binary measurement of an arbitrary cell.

      Equations
      Instances For
        source
        theorem MIPRE.Introspection.HonestMagicSquare.variableOp_isPVM {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) (j : Fin 9) :
        IsPVM (variableOp A B j)
        source
        noncomputable def MIPRE.Introspection.HonestMagicSquare.constraintOp {I : Type u_1} [Fintype I] [DecidableEq I] (A B : Matrix I I ℂ) (c : Fin LCS.MagicSquare.layout.r) (a : Fin 3 → ZMod 2) :
        Matrix (I × Fin 2) (I × Fin 2) ℂ

        The joint measurement of the three cells of a row or column.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def MIPRE.Introspection.HonestMagicSquare.tripleEquiv :
          (Fin 3 → ZMod 2) ≃ (ZMod 2 × ZMod 2) × ZMod 2
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MIPRE.Introspection.HonestMagicSquare.constraintOp_isPVM {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) (c : Fin LCS.MagicSquare.layout.r) :
            IsPVM (constraintOp A B c)
            source
            theorem MIPRE.Introspection.HonestMagicSquare.observable_commute_projector {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (h : Commute A B) (b : ZMod 2) :
            Commute A (LCS.observableToProjector B b)
            source
            theorem MIPRE.Introspection.HonestMagicSquare.variable_constraint_commute {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hAB : A * B = -(B * A)) (c : Fin LCS.MagicSquare.layout.r) (j : Fin 3) (a : Fin 3 → ZMod 2) (b : ZMod 2) :
            Commute (variableOp A B (cellIndex c j) b) (constraintOp A B c a)
            source
            theorem MIPRE.Introspection.HonestMagicSquare.constraint_eigen {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) (c : Fin LCS.MagicSquare.layout.r) (a : Fin 3 → ZMod 2) (j : Fin 3) :
            grid A B (cellIndex c j) * constraintOp A B c a = (-1) ^ (a j).val • constraintOp A B c a
            source
            theorem MIPRE.Introspection.HonestMagicSquare.sign_injective :
            Function.Injective fun (b : ZMod 2) => (-1) ^ b.val
            source
            theorem MIPRE.Introspection.HonestMagicSquare.constraint_wrong_parity {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) (c : Fin LCS.MagicSquare.layout.r) (a : Fin 3 → ZMod 2) (ha : a 0 + a 1 + a 2 ≠ LCS.MagicSquare.game.b c) :
            constraintOp A B c a = 0

            A parity-violating constraint answer has zero effect.

            source
            theorem MIPRE.Introspection.HonestMagicSquare.constraint_disagreement {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) (c : Fin LCS.MagicSquare.layout.r) (a : Fin 3 → ZMod 2) (j : Fin 3) (b : ZMod 2) (hab : a j ≠ b) :
            constraintOp A B c a * variableOp A B (cellIndex c j) b = 0

            A disagreement on an incident cell has zero joint effect.

            source
            theorem MIPRE.Introspection.HonestMagicSquare.constraint_reject_zero {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) (c : Fin LCS.MagicSquare.layout.r) (a : Fin 3 → ZMod 2) (j : Fin 3) (b : ZMod 2) (hr : ¬(a 0 + a 1 + a 2 = LCS.MagicSquare.game.b c ∧ a j = b)) :
            constraintOp A B c a * variableOp A B (cellIndex c j) b = 0

            Both parts of the actual Magic Square incidence check are enforced.

            source
            theorem MIPRE.Introspection.HonestMagicSquare.variableOp_zero {I : Type u_1} [Fintype I] [DecidableEq I] (A B : Matrix I I ℂ) (b : ZMod 2) :
            variableOp A B 0 b = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LCS.observableToProjector A b) 1

            The first distinguished cell retains the original binary measurement.

            source
            theorem MIPRE.Introspection.HonestMagicSquare.variableOp_four {I : Type u_1} [Fintype I] [DecidableEq I] (A B : Matrix I I ℂ) (b : ZMod 2) :
            variableOp A B 4 b = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LCS.observableToProjector B b) 1

            The second distinguished cell retains the original binary measurement.

            source
            theorem MIPRE.Introspection.HonestMagicSquare.projector_measurement {I : Type u_1} [Fintype I] [DecidableEq I] (P : ZMod 2 → Matrix I I ℂ) (hP : LCS.IsMeasurementSystem P) (b : ZMod 2) :
            LCS.observableToProjector (LCS.observableOfMeasurementSystem P) b = P b
            source
            theorem MIPRE.Introspection.HonestMagicSquare.variableOp_embeds_first {I : Type u_1} [Fintype I] [DecidableEq I] (P Q : ZMod 2 → Matrix I I ℂ) (hP : LCS.IsMeasurementSystem P) (b : ZMod 2) :
            variableOp (LCS.observableOfMeasurementSystem P) (LCS.observableOfMeasurementSystem Q) 0 b = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P b) 1
            source
            theorem MIPRE.Introspection.HonestMagicSquare.variableOp_embeds_second {I : Type u_1} [Fintype I] [DecidableEq I] (P Q : ZMod 2 → Matrix I I ℂ) (hQ : LCS.IsMeasurementSystem Q) (b : ZMod 2) :
            variableOp (LCS.observableOfMeasurementSystem P) (LCS.observableOfMeasurementSystem Q) 4 b = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Q b) 1
            source
            theorem MIPRE.Introspection.HonestMagicSquare.transpose_X :
            LCS.Pauli.X.transpose = LCS.Pauli.X
            source
            theorem MIPRE.Introspection.HonestMagicSquare.transpose_Z :
            LCS.Pauli.Z.transpose = LCS.Pauli.Z
            source
            theorem MIPRE.Introspection.HonestMagicSquare.grid_transpose {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hAB : A * B = -(B * A)) (hA : A.transpose = A) (hB : B.transpose = B) (j : Fin 9) :
            (grid A B j).transpose = grid A B j

            Symmetric input observables give symmetric operators throughout the extension.

            source
            theorem MIPRE.Introspection.HonestMagicSquare.variableOp_transpose {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hAB : A * B = -(B * A)) (hA : A.transpose = A) (hB : B.transpose = B) (j : Fin 9) (b : ZMod 2) :
            (variableOp A B j b).transpose = variableOp A B j b
            source
            theorem MIPRE.Introspection.HonestMagicSquare.constraintOp_transpose {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hAB : A * B = -(B * A)) (hA : A.transpose = A) (hB : B.transpose = B) (c : Fin LCS.MagicSquare.layout.r) (a : Fin 3 → ZMod 2) :
            (constraintOp A B c a).transpose = constraintOp A B c a