What winning the Pauli basis test implies #
Blueprint lem:qld-win, the paper's lem:qld-win-implications (qld-commutation.tex). A
strategy succeeding with probability 1 - ฮต satisfies one cross-party consistency relation per
subtest, each at error O(ฮต) --- and the blueprint's proof is exactly one sentence: "each item
is the definition of the value of the corresponding subtest, divided by the probability that the
subtest is selected".
This file makes that sentence mechanical, in two steps.
Step one: every subtest is selected with probability at least 1/86 #
qldGame's question distribution is uniform over TyEdge ร Content, so a question pair arising
from a fixed ordered type edge has probability at least 1/86 times the conditional
probability of its content (le_qldGame_mu). subtest_le is the consequence: for any edge
(t, u) of the type graph, the content-averaged conditional failure at that edge is at most
86 ฮต. The 86 is card_adj, the ordered pairs of the type graph, and it is where the
paper's "the probability of any of the subtests being executed is at least some universal
constant" becomes a number.
Nothing here is about which subtest it is: one lemma serves all seven, because the distribution factors.
Step two: each item is an agreement subtest #
BipartiteModel.xSqNorm_sum_le_condFail turns "the decider accepts iff f a = g b" into a bound
on the cross-party deviation of the POVMs coarse-grained along f and g. So each item of the
lemma is: name f and g, check the decider against them, and compose with subtest_le. That
composition is agree_subtest_le, and the seven items below are its instances --- the
identity for the plain consistency check, a polynomial evaluation for the low-degree check, the
low-degree encoding for Pauli-basis consistency, a projection for the commutation check, and the
trace probe prb for the two commutation- and Magic-Square-consistency checks.
The Magic Square item itself is not of this shape --- it is a statement about the value of a
conditional Magic Square strategy, which is what lem:ms-direct-anticomm consumes --- and it is
in MIPRE/Background/QLD/WinMS.lean.
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 _ โฌ); its value is M.povmValue, its conditional
failures M.condFail, and the cross-party deviation M.xSqNorm a b = โ(ฯA a - ฯB b) ฯโยฒ. The
matrix statements on a unit vector ฯ : dA ร dB โ โ are the instances at the tensor-product
model BipartiteModel.tensor ฯ with the families POVM.toIn, through povmValue_eq_tensor,
condFail_eq_tensor, xSqNorm_eq_tensor and xPovmDist_eq_tensor. Nothing here uses
projectivity, so the families are arbitrary POVMs, and the projective strategies of the later
files apply these statements as they are. The combinatorial half --- the size of the sample
space, the readings, the gates, the format inversions --- mentions no state and is unchanged.
The size of the sample space #
Every subtest is selected with probability at least 1/86 #
The question distribution in closed form: the fraction of samples that produce the pair.
A subtest at a fixed edge of the type graph carries at least 1/86 of the mass. The
sample space is an ordered type edge times the content, drawn independently and uniformly, so
conditioning on the edge costs exactly the 86 ordered pairs of card_adj.
The content-averaged conditional failure of a subtest is at most 86 ฮต. This is the
blueprint's "divided by the probability that the subtest is selected", with the probability
computed. The sum is over any set S of contents, since a rule gated on ฮณ fires only on part
of the sample space; dropping the rest only decreases a sum of nonnegative terms.
Each item is an agreement subtest #
The master estimate for the Pauli basis test. A subtest that accepts only when two
post-processings of the answers agree gives, at error 172 ฮต, cross-party closeness of the
coarse-grained measurements --- averaged over the verifier's content, which is the "on average
over ..." of every item of lem:qld-win.
S is the set of contents on which the rule fires: everything for the ungated rules, the
commuting or the anticommuting tuples for the four rules gated on ฮณ. The weight is 1/#Content
throughout, so for a gated rule this is the unconditional average with the gate's indicator
inside; the paper's conditional form is this divided by the gate's probability, which is where
fact:omega-anticomm-prob and the hypothesis 6md โค q enter.
The 172 is 2 ยท 86: the factor 2 of BipartiteModel.xSqNorm_sum_le_condFail and the
selection probability 1/86 of subtest_le.
The readings each rule compares #
A rule of fig:decider_pauli compares a post-processing of Alice's answer with one of Bob's.
Each is named here, with 0 on answers of the wrong format --- which costs nothing, because the
format check rejects those before any rule runs, and xSqNorm_sum_le_condFail only needs
accept implies agree.
The field element a point answer reports.
Equations
- MIPRE.QLD.rdVal (MIPRE.QLD.Answer.val a) = a
- MIPRE.QLD.rdVal xโ = 0
Instances For
The value at y of an axis-parallel line answer, at the parameter of y on the line.
Equations
- MIPRE.QLD.rdAPoly uโ w y (MIPRE.QLD.Answer.apoly p) = p.eval (MIPRE.LIDT.CL.lineParam uโ w y)
- MIPRE.QLD.rdAPoly uโ w y xโ = 0
Instances For
The value at y of a diagonal line answer.
Equations
- MIPRE.QLD.rdDPoly uโ w y (MIPRE.QLD.Answer.dpoly p) = p.eval (MIPRE.LIDT.CL.lineParam uโ w y)
- MIPRE.QLD.rdDPoly uโ w y xโ = 0
Instances For
The low-degree encoding of a (Pauli, W) answer, evaluated at y: the paper's
g_h(y).
Equations
- MIPRE.QLD.rdPauli y (MIPRE.QLD.Answer.pauliAns h) = (MvPolynomial.eval y) (MIPRE.LowDegree.ldEnc h)
- MIPRE.QLD.rdPauli y xโ = 0
Instances For
The bit a (Pair, W) or Variable_j answer reports.
Equations
- MIPRE.QLD.rdBit (MIPRE.QLD.Answer.bit b) = b
- MIPRE.QLD.rdBit xโ = 0
Instances For
The W-component of a Pair answer.
Equations
- MIPRE.QLD.rdBitPair W (MIPRE.QLD.Answer.bitPair ฮฒ) = ฮฒ W
- MIPRE.QLD.rdBitPair W xโ = 0
Instances For
The trace probe tr(a ยท r) of a point answer: the two-outcome measurement the commutation
and Magic Square checks compare against.
Equations
- MIPRE.QLD.rdProbe r (MIPRE.QLD.Answer.val a) = MIPRE.QLD.prb a r
- MIPRE.QLD.rdProbe r xโ = 0
Instances For
The axis-parallel direction the seed selects.
Equations
- MIPRE.QLD.dirOf hm c = Pi.single (MIPRE.LIDT.CL.chi hm c.s) 1
Instances For
Bob's reading of an axis-parallel line answer, at the point the same content gives Alice.
Equations
- MIPRE.QLD.rdALineAt hm W c = MIPRE.QLD.rdAPoly (MIPRE.LIDT.CL.rep (MIPRE.QLD.dirOf hm c) (c.pt W)) (MIPRE.QLD.dirOf hm c) (c.pt W)
Instances For
Bob's reading of a diagonal line answer, at the point the same content gives Alice.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The commuting and anticommuting contents #
Four rules are gated on ฮณ(ฯ) and check nothing on the other value, so their statements carry
the gate as a restriction of the content average.
The contents whose tuple is commuting, ฮณ(ฯ) = 0.
Equations
- MIPRE.QLD.commSet = {c : MIPRE.QLD.Content F m | MIPRE.QLD.gam c.omega = 0}
Instances For
The contents whose tuple is anticommuting, ฮณ(ฯ) โ 0.
Equations
- MIPRE.QLD.acommSet = {c : MIPRE.QLD.Content F m | MIPRE.QLD.gam c.omega โ 0}
Instances For
The edges the rules live on #
The items #
Each is agree_subtest_le at a named edge with the two readings the rule compares.
Item 1, the consistency check. At equal types the two players' measurements are
cross-party consistent at error 172 ฮต, and so is any common reading of their answers: the
rule accepts only when the answers are equal, and equal answers have equal readings. That is the
data-processing inequality, and it comes for free from agree_subtest_le rather than as a
separate fact.
The parameter agreement a line-against-point acceptance yields.
Item 2a, the low-degree check against an axis-parallel line. The line polynomial,
evaluated at the parameter of the sampled point, agrees with the point answer, at error
172 ฮต. This is the seeded CL decider's own check (lowDeg_eq_cl).
Item 2b, the low-degree check against a diagonal line.
Item 3, Pauli basis consistency. The low-degree encoding of the full (Pauli, W)
outcome, evaluated at the sampled point, agrees with the point answer.
Item 4, the commutation check, on the commuting tuples: the (Pair, W) bit agrees with
the W-component of the Pair answer. On an anticommuting tuple the rule checks nothing, by
design, which is why the average is restricted.
The trace probe of a point answer against the W-side qubit basis element of the
content.
Equations
- MIPRE.QLD.rdProbeAt W c = MIPRE.QLD.rdProbe (c.omega.r W)
Instances For
Item 5, commutation consistency, on the commuting tuples: the trace probe of the point
answer agrees with the (Pair, W) bit.
Item 7 for X, Magic Square consistency, on the anticommuting tuples: the trace probe
of the (Point, X) answer agrees with the Variable_1 bit --- var 0 at this file's
0-indexing.
Item 7 for Z.