Signed commutation of the point observables, on the anticommuting tuples #

Blueprint lem:qld-obs-commutation, the anticommuting case. On a tuple omega with gamma(omega) = 1 the two point observables anticommute on the state:

X^{r_X}(u_X) Z^{r_Z}(u_Z) (x) Id  ~  - Z^{r_Z}(u_Z) X^{r_X}(u_X) (x) Id .

Three inputs, all already proved:

item 7 of lem:qld-win (item_ms_consistency_X, item_ms_consistency_Z): each point probe agrees with one of the two distinguished Variable bits on the other side. At the level of observables that is X (x) Id ~ Id (x) V_1 and Z (x) Id ~ Id (x) V_5, at 344 eps each --- item 7 at the two-outcome probe, then xStateDist_obsOf_le;
item 6 (item_magicSquare): those two Variable observables anticommute on the state, at 16049664 eps;
the order reversal BipartiteModel.stateNorm_anticomm_le, which is what carries an anticommutation from Bob's side to Alice's --- and is where the sign comes from.

Why this case costs `eps` and not `sqrt(eps)` #

The paper states lem:qld-obs-commutation at O(sqrt(eps)), and that is what its commuting case costs: it needs the Pair measurement to be projective, which a general POVM strategy's is not, so it goes through the orthogonalization corollary (cor:ortho-from-consistency) and pays a square root. Here the first player's measurements are projective by hypothesis, and the blueprint states the lemma at the constant proved below. The anticommuting case needs no projectivity: every input is already a squared-norm bound linear in eps, and the only inequalities used are the triangle inequality and (u+v+w)^2 <= 3(u^2+v^2+w^2). So the constant here is honest and there is no square root --- 48157248 eps, from 12 * 344 + 12 * 344 + 3 * 16049664.

The commuting case below is linear in eps as well: the strategy's Pair measurement is projective, so no orthonormalization, and no square root, enters either half.

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, the first of them projective (IsPVMIn), as every strategy of the Pauli basis test is. The observables are elements of the players' algebras --- a two-outcome POVM's ±1-observable is the difference of its two elements, POVMIn.obs2 --- their norms on the state are M.stateSqNorm, M.swap.stateSqNorm and M.xSqNorm, and a two-outcome observable is a contraction on the Hilbert space (M.Bnd, from BipartiteModel.bnd_πA_sub) rather than in the algebra, which need not have a functional calculus.

The first player's projectivity is used twice: by item 6 (item_magicSquare, through lem:ms-direct-anticomm), and in the commuting case, where Alice's joint Pair measurement is a coarse-graining of her projective Pair measurement and so is projective itself (isPVMIn_pairPOVM). That is the projective measurement the commutation analysis needs, so the matrix route's de la Salle orthonormalization (cor:ortho-from-consistency, which replaced that POVM by a nearby projective measurement) is gone, and with it the slack η its strict hypothesis asked for. Every constant of the matrix statements is kept. On a unit vector ψ : dA × dB → ℂ the statements are read at the tensor-product model BipartiteModel.tensor ψ with the families POVM.toIn.

Two-outcome observables in an ordered `⋆`-ring #

The model form of MIPRE.obs2: the ±1-observable of a POVM with outcomes in F_2 is the difference of its two elements.

Signed commutation of the point observables, on the anticommuting tuples #

Why this case costs eps and not sqrt(eps) #

In a bipartite model #

Two-outcome observables in an ordered ⋆-ring #

The two observables #

The weight: uniform on the anticommuting tuples #

Item 7 at the level of observables #

Item 6's anticommutator, in terms of the variable observables #

The lemma #

The inconsistency of a pair of POVMs #

The commuting case #

The three links #

The three averaged inputs #

The per-content bound #

Both halves #

Why this case costs `eps` and not `sqrt(eps)` #

Two-outcome observables in an ordered `⋆`-ring #