The padded strategy for the seeded low individual degree test #

Stage 4 of the Pauli basis test's analysis (lem:qld-global-setup, lem:qld-global-success) assembles the padded point and line measurements of lem:qld-padded-points and lem:qld-padded-lines into a strategy for the seeded test clGame at parameters (q, 4m, d, 1), and shows that it succeeds with probability 1 - O(δ_combine + δ_Q + md/q). This file defines the strategy and bounds its conditional failure at each of the seeded test's question pairs by an agreement defect of the measurements it is built from; the averages over the verifier's samples, and the value bound, are in PaddedValue.lean.

The model, and why the strategy is a family of POVMs #

The strategy lives in the expanded model M.reg (Anc F m) of stage 2: each player's measurements are elements of Matrix (Anc F m) (Anc F m) R over the player's algebra R (the player's own algebra and the expansion's ancilla, register outer). There is no register for the combining coefficients: it was inert in every padded measurement. The point measurement is the sandwich M^Z_b M^X_a M^Z_b of the hatted point measurements (POVMIn.sand), coarse-grained along (a, b) ↦ α a + β b; its line measurements are the padded line measurements padLineMats, averaged over the raw directions. Both are POVMs --- the point elements are coarse-grainings of Gram elements (X_a Z_b)⋆ (X_a Z_b), the line elements averages of pasted sandwiches --- and neither is projective, so the strategy is a family of POVMs, and one Halmos dilation at the end makes it the projective strategy the soundness theorem takes. The dilated point measurement of lem:qld-padded-points is not used: every bound of stage 3 is stated for the sandwich itself (combined_points_pts, padded_lines_consistency).

In a bipartite model #

Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The strategy of each player is padStrat hm hm4 hS for a projective family S : Question F m → POVMIn (Answer F m d) R (the design's padStratIn; the cited names padStrat, padPt, padPtPair, padLinePOVM, lineMeas are the model versions), the conditional failures are those of any bipartite model whose algebras are the two players' Matrix (Anc F m) (Anc F m) _ (in particular M.reg (Anc F m)), and polynomial separation holds in any bipartite model. The model forms of the matrix helpers POVM.ofPosSemidef, POVM.avgOn and the support lemmas of coarse-grainings are POVMIn.ofNonneg, POVMIn.avgOn, POVMIn.map_congr_of_support, POVMIn.map_op_eq_zero_of_forall_ne and POVMIn.map_const_op below.

A function of the question #

The seeded test asks for a measurement per question, while padLineMats is indexed by the data ⟨pt, s, raw⟩ a sample generates the question from. A line question carries the canonical base point u₀ of the line, the seed, and for a diagonal line the truncated direction v'; the strategy answers it with the padded line measurement at the data ⟨u₀, s, raw⟩, averaged over the raw directions that produce the question (rawFiber). Two things make this the right choice. The decider reads the answer polynomial at the parameter of the sampled point relative to u₀, and moving the data's point to the sampled point along the line does not change the padded line measurement (pasteLine_subPair_padShift), so what the decider reads is padLineMats at the sample's own data, coarse-grained by evaluation at the sample's point --- exactly the quantity lem:qld-padded-lines controls (lineMeas_map_eval_mats). And the sample distribution averages uniformly over the raw direction, so by linearity of the Born rule the strategy's failure at a question is the average of the per-sample quantities.

POVMs in a `⋆`-algebra from nonnegative families, uniform averages, and supports #

The model forms of POVM.ofPosSemidef, POVM.avgOn and three facts about coarse-grainings (MIPRE/Foundations/POVMMix.lean), which the padded strategy needs in a player's algebra.

The padded strategy for the seeded low individual degree test #

The model, and why the strategy is a family of POVMs #

In a bipartite model #

A function of the question #

POVMs in a ⋆-algebra from nonnegative families, uniform averages, and supports #

The padded point measurement #

The padded line measurements, as POVMs #

The questions of a sample #

The strategy #

The support of the strategy's answers #

The line measurement read at the sampled point #

The conditional failures of the strategy, question pair by question pair #

Polynomial separation #

POVMs in a `⋆`-algebra from nonnegative families, uniform averages, and supports #