Direct Magic Square anticommutation #
Blueprint lem:ms-direct-anticomm: a strategy failing the Magic Square game with probability
ε has ‖{B₁, B₅}|ψ⟩‖² ≤ 186624 ε for the original ±1-observables of the player who receives
the variables --- no isometry and no extracted EPR pairs. This is the only thing the Pauli basis
test consumes from the Magic Square, and it is much weaker than the full rigidity theorem
thm:ms-rigidity, which this repository does not prove.
The shape of the argument #
Alice's constraint answers are repaired to parity-valid ones and pushed forward to a
measurement with four outcomes (repPOVM). Her measurements are projective, and a
coarse-graining of a projective measurement is projective (isPVMIn_repPOVM), so the repaired
measurement is one too. Signed sums of it are reflections that commute within a constraint and
multiply to its sign exactly (MIPRE.IsPVMIn.pvmObs_mul_mul) --- that is what projectivity
buys, and it is why the repair has to happen first.
The rest is norm bookkeeping on the state, in the operator-bound calculus of the model
(MIPRE/Foundations/StateModel.lean): each of Alice's reflections is within γ of the
corresponding Bob observable, γ² ≤ 144 ε; a Bob word of length t can be replaced by the
reversed word of Alice reflections at cost t γ; a within-constraint relation costs 3 γ; and
the six-step path through the six constraints turns d a e b into - d e a b at cost 24 γ.
In a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The strategy is a model
M : BipartiteModel 𝒞 𝒜 ℬ with ‖M.ψ‖ = 1 and two families of POVMs PA, PB in the players'
ordered algebras (POVMIn _ 𝒜, POVMIn _ ℬ). The operators are elements of 𝒜 and ℬ acting
through M.πA and M.πB, the norms are the model's (M.snorm, and M.swap.stateSqNorm for the
second player's ‖(Id ⊗ Y)|ψ⟩‖²), and the value is M.povmValue. The constraint player's
measurements are projective (IsPVMIn), as every strategy of the Pauli basis test is from the
start. So the Naimark dilation of the matrix statement --- whose only purpose was to make the
repaired measurement projective, on one ancilla shared by the six constraints --- is gone: the
repaired measurement is used as it is, on the model's own state, and its reflections are
elements of the first player's algebra. The variable player's measurements stay arbitrary POVMs;
the other player's half of the lemma (ms_direct_anticomm') asks for his to be projective
instead. On a unit vector ψ : dA × dB → ℂ the statement is read at the tensor-product model
BipartiteModel.tensor ψ with the families POVM.toIn (projectivity through IsPVM.toIn),
where M.swap.stateSqNorm Y is ‖stateVecB ψ Y‖² (normSq_stateVecB_eq_tensor) and the value is
povmValue (povmValue_eq_tensor).
Alice's repaired outcomes #
A parity-valid answer to a constraint is determined by its bits at the first two cells, so the
repaired outcome set is ZMod 2 × ZMod 2 and the bit at the third cell is read off the
constraint's right-hand side.
The repaired outcome set of a constraint.
Equations
- MIPRE.QLD.MS.PV = (ZMod 2 × ZMod 2)
Instances For
The sign weighting of constraint c at its j-th cell.
Equations
- MIPRE.QLD.MS.csgn c j k = MIPRE.sgn (MIPRE.QLD.MS.pvBit c k j)
Instances For
The three signs of a constraint multiply to its sign.
Alice's answer to a constraint, repaired to a parity-valid outcome: an assignment
satisfying the constraint keeps its bits at the first two cells, and everything else --- an
assignment violating the parity, or an answer of the wrong shape --- is sent to (0, 0). This
preserves every originally winning pair, which is all the argument needs.
Equations
Instances For
On a parity-valid answer the repair loses nothing: the outcome's bit at each cell is the answer's. For the third cell this is the parity condition.
Numerals for the magic square #
Variable k, in row-major order.
Equations
- MIPRE.QLD.MS.var k h = ⟨k, h⟩
Instances For
Constraint c: the three rows then the three columns.
Equations
- MIPRE.QLD.MS.con c h = ⟨c, h⟩
Instances For
The repaired Alice measurement, and Alice's reflections #
The repaired measurement is the coarse-graining of Alice's constraint measurement along rep,
and it is projective because hers is: this is what replaces the matrix statement's dilation.
Alice's repaired constraint measurement, with the four parity-valid outcomes.
Equations
- MIPRE.QLD.MS.repPOVM PA c k = ∑ d : MIPRE.LCS.MagicSquare.layout.Answer with MIPRE.QLD.MS.rep c d = k, (PA (Sum.inl c)).op d
Instances For
The repaired measurement of a projective measurement is projective: it is a coarse-graining.
Alice's reflection for constraint c at its j-th cell.
Equations
- MIPRE.QLD.MS.refl PA c j = MIPRE.pvmObs (MIPRE.QLD.MS.repPOVM PA c) (MIPRE.QLD.MS.csgn c j)
Instances For
The three reflections of a constraint multiply to its sign, exactly.
The three reflections of a constraint, in the form the relations use: the product of the first two is the constraint's sign times the third.
Alice's reflection is her constraint measurement, signed by the repaired outcome: each original answer contributes with the sign its repaired outcome gives the cell.
Bob's observables #
Bob's ±1-observable at variable j: the difference of the two bit outcomes. Answers of
the wrong shape contribute zero, which is exactly the paper's convention.
Instances For
{B₀, B₄}, the anticommutator the Pauli basis test consumes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An operator fact #
Id - b² is a contraction for a difference b of two operators between 0 and 1. It is a
statement about operators on a Hilbert space, where the functional calculus is: a player's algebra
need not have one.
1 - (P - Q)² is a contraction for 0 ≤ P, Q ≤ 1: it lies between 0 and 1, the
upper bound because (P - Q)² is positive and the lower because 1 - (P - Q)² is the product of
the commuting positive operators 1 - (P - Q) and 1 + (P - Q).
The calculus on the state #
Every estimate of the argument is a state norm M.snorm of an element of the model's algebra,
built from Alice's reflections (through M.πA) and Bob's observables (through M.πB).
An isometry of the first player's algebra is an isometry of the model's.
A product of Bob observables is a contraction.
Appending a Bob suffix costs twice its replacement cost.
Bob's observable is a contraction: the difference of two POVM elements.
Alice's reflection is an isometry of the model's algebra.
The anticommutator is bounded by two.
Id - b² is a contraction, because 0 ≤ b² ≤ 1.
Replacing Bob's letters by Alice's reflections #
A Bob word of length t agrees on the state with the reversed word of Alice reflections to
within t γ: replace the letters one at a time from the right, each replacement costing γ,
and cross the two players' algebras so the Alice letters accumulate in the opposite order. Only
lengths one, two and three occur in the argument, so the three cases are spelled out rather than
induced.
Rewriting inside a word #
A within-constraint relation costs 3 γ. The two Bob letters are transported to the
constraint's two Alice reflections, which costs 2 γ; their product is the third reflection
times the constraint's sign, with no error; and that reflection is returned to Bob for a
further γ.
The six-step path #
d a e b becomes - d e a b by applying the six constraints in turn --- column one, column
two, row three, column three, row two, row one --- at a total cost of 24 γ. The sign appears
exactly once, at column three, which is the constraint of product -1.
The six-step path.
Removing the two outer letters #
The path bounds ‖d (a e + e a) b |ψ⟩‖. Removing d costs the non-projectivity of b_3,
which is ‖(Id - b_3²) W |ψ⟩‖ ≤ (2 + t) γ for a word of length t; removing b costs 2 γ,
because Alice's reflection for variable 1 is unitary and commutes with the anticommutator.
‖(Id - b²)|ψ⟩‖ ≤ 2 γ, from Id - b² = (D + b)(D - b) across the two players.
The anticommutator is within 36 γ of zero on the state.
From the game's value to the closeness hypothesis #
The correlation ⟨ψ| C_{c,j} ⊗ B_j |ψ⟩ is agreement minus disagreement between Alice's
repaired outcome bit and Bob's answer bit, and every winning answer pair agrees --- that is
what the repair preserves. So the correlation is at least 1 - 2 ℓ_{c,j}, and since
δ²_{c,j} = 2 - 2⟨ψ| C B |ψ⟩ - (1 - ⟨ψ| B² |ψ⟩) ≤ 2 - 2⟨ψ| C B |ψ⟩, the reflection is
within 2√ℓ of the observable.
The signed Born mass at an incidence: Alice's repaired outcome bit against Bob's answer
bit, agreement counting +1 and disagreement -1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The total Born mass on Bob's bit answers is at most one.
Every winning answer pair agrees, so the accepted mass is at most the agreeing mass.
The correlation is at least 1 - 2 ℓ.
The correlation is the quadratic form #
The correlation is the quadratic form of C_{c,j} ⊗ B_j. No projectivity: this is the
expansion of the reflection into Alice's original constraint measurement (refl_eq_sum).
The closeness hypothesis, from the game's value #
The closeness hypothesis, with γ = 12 √ε.
The lemma, for the player who receives the variables #
Direct Magic Square anticommutation (blueprint lem:ms-direct-anticomm), for the player
who receives the variable questions, in a bipartite model. No isometry and no extracted EPR
pairs: the bound is on the original observables and the original state. The constraint player's
measurements are projective; the variable player's are arbitrary POVMs.
The other player, by the symmetry of the game #
Exchanging the players is an automorphism of the Magic Square game
(MIPRE.LCS.Layout.questionDist_symm, MIPRE.LCS.Game.accepts_symm), so Alice's half of the
lemma is Bob's half in the swapped model, BipartiteModel.swap.
The value of a Magic Square strategy is unchanged by exchanging the players, in the swapped model.
Direct Magic Square anticommutation for the other player. The game is symmetric in the
players, so this is ms_direct_anticomm in the swapped model; now the variable player's
measurements are the projective ones.
The averaged form. The bound is pointwise, so averaging it over a family of strategies in models over the same algebras costs nothing --- no Jensen step, and the same constant.