Perfect PCC play of the actual Magic Square game

The arbitrary anticommuting pair is extended by one qubit. Constraint triples are encoded as assignments with zeroes outside the queried constraint. This file uses the existing game's exact distribution and decision predicate.

def MIPRE.Introspection.HonestMagicSquare.assignment (c : Fin LCS.MagicSquare.layout.r) (a : Fin 3 → ZMod 2) : Fin LCS.MagicSquare.layout.s → ZMod 2

Extend the three reported bits by zero outside the queried constraint.

Equations

• MIPRE.Introspection.HonestMagicSquare.assignment c a j = if j ∈ MIPRE.LCS.MagicSquare.layout.V c then a (MIPRE.LCS.MagicSquare.cellIdx c j) else 0

@[simp]

theorem MIPRE.Introspection.HonestMagicSquare.assignment_cell (c : Fin LCS.MagicSquare.layout.r) (a : Fin 3 → ZMod 2) (j : Fin 3) : assignment c a (LCS.MagicSquare.cell c j) = a j

theorem MIPRE.Introspection.HonestMagicSquare.assignment_parity (c : Fin LCS.MagicSquare.layout.r) (a : Fin 3 → ZMod 2) : ∑ j ∈ LCS.MagicSquare.layout.V c, assignment c a j = a 0 + a 1 + a 2

def MIPRE.Introspection.HonestMagicSquare.constraintAnswer (c : Fin LCS.MagicSquare.layout.r) (a : Fin 3 → ZMod 2) : LCS.MagicSquare.layout.Answer

Equations

• MIPRE.Introspection.HonestMagicSquare.constraintAnswer c a = Sum.inl (MIPRE.Introspection.HonestMagicSquare.assignment c a)

noncomputable def MIPRE.Introspection.HonestMagicSquare.questionOp {I : Type u_1} [Fintype I] [DecidableEq I] (A B : Matrix I I ℂ) : LCS.MagicSquare.layout.Question → LCS.MagicSquare.layout.Answer → Matrix (I × Fin 2) (I × Fin 2) ℂ

The actual shared answer alphabet, including zero effects for wrong shapes.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.HonestMagicSquare.questionOp A B (Sum.inr j) = MIPRE.fibSum (MIPRE.Introspection.HonestMagicSquare.variableOp A B j) Sum.inr

theorem MIPRE.Introspection.HonestMagicSquare.questionOp_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)) (q : LCS.MagicSquare.layout.Question) : IsPVM (questionOp A B q)

theorem MIPRE.Introspection.HonestMagicSquare.coarse_commute {I : Type u_1} [Fintype I] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] {U : Type u_4} {V : Type u_5} [DecidableEq U] [DecidableEq V] (M : X → Matrix I I ℂ) (N : Y → Matrix I I ℂ) (f : X → U) (g : Y → V) (hc : ∀ (x : X) (y : Y), Commute (M x) (N y)) (u : U) (v : V) : Commute (fibSum M f u) (fibSum N g v)

theorem MIPRE.Introspection.HonestMagicSquare.questionOp_incidence_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 LCS.MagicSquare.layout.s) (hj : j ∈ LCS.MagicSquare.layout.V c) (a b : LCS.MagicSquare.layout.Answer) : Commute (questionOp A B (Sum.inl c) a) (questionOp A B (Sum.inr j) b)

theorem MIPRE.Introspection.HonestMagicSquare.constraint_incidence_reject {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) (j : Fin LCS.MagicSquare.layout.s) (hj : j ∈ LCS.MagicSquare.layout.V c) (a : Fin 3 → ZMod 2) (b : ZMod 2) (hr : LCS.MagicSquare.game.accepts (Sum.inl c) (Sum.inr j) (constraintAnswer c a) (Sum.inr b) = false) : constraintOp A B c a * variableOp A B j b = 0

theorem MIPRE.Introspection.HonestMagicSquare.questionOp_incidence_reject {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) (j : Fin LCS.MagicSquare.layout.s) (hj : j ∈ LCS.MagicSquare.layout.V c) (a b : LCS.MagicSquare.layout.Answer) (hr : LCS.MagicSquare.game.accepts (Sum.inl c) (Sum.inr j) a b = false) : questionOp A B (Sum.inl c) a * questionOp A B (Sum.inr j) b = 0

theorem MIPRE.Introspection.HonestMagicSquare.positive_incidence (p q : LCS.MagicSquare.layout.Question) (h : 0 < LCS.MagicSquare.nonlocalGame.μ p q) : (∃ (c : Fin LCS.MagicSquare.layout.r) (j : Fin LCS.MagicSquare.layout.s), p = Sum.inl c ∧ q = Sum.inr j ∧ j ∈ LCS.MagicSquare.layout.V c) ∨ ∃ (c : Fin LCS.MagicSquare.layout.r) (j : Fin LCS.MagicSquare.layout.s), p = Sum.inr j ∧ q = Sum.inl c ∧ j ∈ LCS.MagicSquare.layout.V c

theorem MIPRE.Introspection.HonestMagicSquare.questionOp_commute {I : Type u_1} [Fintype I] [DecidableEq I] {A B : Matrix I I ℂ} (hAB : A * B = -(B * A)) (p q : LCS.MagicSquare.layout.Question) (h : 0 < LCS.MagicSquare.nonlocalGame.μ p q) (a b : LCS.MagicSquare.layout.Answer) : Commute (questionOp A B p a) (questionOp A B q b)

theorem MIPRE.Introspection.HonestMagicSquare.questionOp_reject {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)) (p q : LCS.MagicSquare.layout.Question) (h : 0 < LCS.MagicSquare.nonlocalGame.μ p q) (a b : LCS.MagicSquare.layout.Answer) (hr : LCS.MagicSquare.nonlocalGame.D p q a b = false) : questionOp A B p a * questionOp A B q b = 0

noncomputable def MIPRE.Introspection.HonestMagicSquare.strategy {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) : SyncStrategy LCS.MagicSquare.nonlocalGame.doubled

An actual PCC strategy for the existing Magic Square game, on twice the input dimension.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.HonestMagicSquare.doubled_positive (p q : Bool × LCS.MagicSquare.layout.Question) (h : 0 < LCS.MagicSquare.nonlocalGame.doubled.μ p q) : (p.1 = false ∧ q.1 = true) ∧ 0 < LCS.MagicSquare.nonlocalGame.μ p.2 q.2

theorem MIPRE.Introspection.HonestMagicSquare.strategy_isPCC {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) : (strategy hA hB hAB).IsPCC

theorem MIPRE.Introspection.HonestMagicSquare.strategy_value {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) : (strategy hA hB hAB).value = 1

theorem MIPRE.Introspection.HonestMagicSquare.exists_perfectPCC {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] {A B : Matrix I I ℂ} (hA : LCS.IsObservable A) (hB : LCS.IsObservable B) (hAB : A * B = -(B * A)) : ∃ (S : SyncStrategy LCS.MagicSquare.nonlocalGame.doubled), S.IsPCC ∧ S.value = 1 ∧ S.d = 2 * Fintype.card I

The arbitrary anticommuting pair produces a perfect PCC strategy of local dimension 2|I|.