The Pauli basis test #

Blueprint def:qld-game, the paper's game game^pauli_{(q,m,d)} (ldt.tex, sec:qld-game for the question distribution and fig:decider_pauli for the decision procedure). This is the game thm:qld is about and lem:qld-win unpacks.

The test certifies that the players share |EPR_q⟩^{⊗ M}, M = 2^m. A player asked (Pauli, W) measures {τ^W_h}_{h ∈ F_q^M} and reports h; every other question probes limited information about h through its low-degree encoding g_h : F_q^m → F_q (MIPRE.LowDegree.ldEnc), and the subtests check that those probes are consistent with each other and across the two bases.

The three groups of question types #

type^pauli = ({Point, ALine, DLine, Pauli, Pair} × {X, Z}) ∪ type^MS ∪ {Pair} --- twenty-six types, Ty below, in three groups with three different jobs.

(Point, W), (ALine, W), (DLine, W), (Pauli, W) run the classical low-degree test of def:lidt-cl separately in each basis, plus the tie from a point probe to the full outcome. The line and point content is read off the sample exactly as the seeded CL game reads it (MIPRE.LIDT.CL.chi, rep, zeroBelow), which is what makes the distribution a typed CL distribution and lets the soundness proof feed thm:lidt-cl-soundness.
Pair, (Pair, W) are the commutation check. The two two-outcome measurements tr(g_{h_X}(u_X) r_X) and tr(g_{h_Z}(u_Z) r_Z) either commute or anticommute, according to γ(ω) = 0 or not (MIPRE.LowDegree.acGamma, blueprint fact:omega-anticomm-prob); when they commute the verifier asks for both at once and compares.
Constraint_i, Variable_j are the Magic Square, run when they anticommute --- which is exactly when they cannot be measured together. thm:ms-from-ac is the completeness direction, and lem:ms-direct-anticomm (MIPRE/Background/QLD/Anticomm.lean) is the soundness direction this game consumes. The indices here are the layout's own (MIPRE.LCS.MagicSquare.layout), 0-indexed against the paper's 1-indexed Constraint_1..6 and Variable_1..9, so the paper's distinguished pair (Point, X)--Variable_1 and (Point, Z)--Variable_5 is var 0 with X and var 4 with Z here.

The distribution #

adj is the type graph fig:type-graph-pauli: thirty non-loop edges (eighteen Magic Square incidences, six line/point and point/Pauli edges, two point/variable edges, four through the commutation check) and a self-loop at every one of the twenty-six vertices. The verifier draws an ordered pair of adjacent types --- the graph distribution of def:graph-distribution, each non-loop edge contributing two ordered pairs and each self-loop one, so uniform over the 2 * 30 + 26 = 86 ordered pairs --- then (u_X, u_Z, s, v, r_X, r_Z) uniformly, and hands each player the content its type prescribes. Sampling the pair and the content independently and uniformly is what makes Sample a product and μ_sum_one one division.

The decision procedure #

fig:decider_pauli is a format check and then seven rules. Question.fmtOk is the check --- the table at the top of the figure --- and subtests the rules, with accepts their conjunction.

The separation is not cosmetic, and the warning is on the record: the seeded CL game shipped without its format check, which made the test vacuous and thm:lidt-cl-soundness false about it (reports/clgame-format-check-missing.md). The same class of error is available here with twenty-six types instead of three, so every rule below has a witness that it can fail: rejects_* for the format check and for each of the seven rules.

Two structural facts about the rules are worth stating mechanically rather than trusting. subtests_covers_adj says the catch-all --- fig:ld-decider's "in all cases where no action is indicated, accept", which this figure inherits --- is reached only at non-adjacent type pairs, so it never accepts anything the distribution actually asks. And lowDeg_eq_cl says the low-degree rule is the seeded CL decider at ldc = 1 and not a paraphrase of it, which is what the figure prescribes ("accept if D^ld_{(q,m,d,1)} accepts").

The Pauli basis test #

The three groups of question types #

The distribution #

The decision procedure #

Bases #

Question types #

Questions #

The sample space #

The format check #

Inverting the format check #

The rules #

The rules cover the type graph #

The low-degree rule is the seeded CL decider #

Non-vacuity #

The game #