The global polynomial measurements: applying the seeded soundness theorem #

lem:qld-global-pvm. By lem:qld-global-success (padStrat_value), the padded strategy (padStrat hm hm4 S.projA, padStrat hm hm4 S.projB) wins the seeded low individual degree test at (q, 4m, d, 1) in the expanded model M.reg (Anc F m) with probability at least 1 - δ_GS, where δ_GS = 5 m² δ_P(ε, md/q + 1/q) + 4 δ_Q(ε) + (md + 1)/q. This file feeds it to the seeded soundness theorem and reads the conclusion back in the form stages 4b and 4c consume.

The dilation, and where the soundness theorem is applied #

The padded strategy is a pair of families of POVMs (its point answers are sandwich combinations, its line answers averages of pasted measurements), and the soundness theorem is about projective strategies. So each player's family is Halmos-dilated (exists_pvm_dilation_ge) on the padding register PadAnc F m d K, both at one common size K (exists_padDilation): the dilated families are a projective strategy D of the padded model padModel (Anc F m) F m d M K, the register model extended by each player's padding register in the product vector |t₀⟩ ⊗ |t₀⟩ (MIPRE/Background/QLD/PhysModel.lean), whose reference entries are the padded strategy's. A Born probability of the padded model is the Born probability of the reference entries (BipartiteModel.bornProb_expand_basisVec), so D has the padded strategy's value (BipartiteModel.povmValue_expand_basisVec).

The soundness theorem enters as a hypothesis hL on the model: the seeded test is sound (LIDT.Simul.SoundIn) in every extension M.expand e of M by a unit vector. The padded model is such an extension up to associativity, so the test is sound in it (soundIn_padModel), and it is applied to D at one codeword (r = 1). Its conclusion is read back along Fin 1 → F ≃ F (BipartiteModel.inconsistency_map_equiv), and the dilated point measurements are replaced by the padded point measurements extended by the identity on the padding register (their pushforward along the inert embedding of the register model): both have the padded point measurement as reference entry, so every inconsistency on the padded model is the same (BipartiteModel.inconsistency_expand_basisVec_congr). The final form, exists_globalPair, mentions no dilation.

The interface `GlobalPair` #

A GlobalPair M S K ι δ is the output of the lemma in any model K into which the register model embeds along ι (BipartiteModel.Embedding): two projective low-degree measurements GA, GB in K's algebras, consistent with the opposite party's padded point measurements carried along ι, and with each other. Stages 4b and 4c are theorems about a GlobalPair, and every expectation of an operator carried along ι is its expectation in the register model, so the conclusions of stages 2 and 3 transfer. exists_globalPair gives one at K = padModel …, ι the inert embedding, for every padding size beyond a threshold, so that the two runs of stage 4 (at S and at the strategy with the players exchanged) can share one padding size. GlobalPair.toSimulPair builds the interface SimulPair in the same model, with no reindexing.

The error #

δ_ld = deltaLD q m d ε = deltaSim q (4m) d 1 (deltaGS q m d ε): the seeded soundness theorem's error at (q, 4m, d, 1), one codeword, for a strategy of value 1 - δ_GS. It is of the blueprint's displayed form A (md)^A ((δ_GS)^b + q^{-b} + 2^{-bmd}), since (4md)^A = 4^A (md)^A and 2^{-4bmd} ≤ 2^{-bmd}.

The recovered polynomials live on F^{4m}, while the point measurements read only the 2m + 2 coordinates xBlk, zBlk, alph, bet. The Schwartz--Zippel argument that the polynomials mostly do not read the remaining dummy coordinates is MIPRE/Background/QLD/Dummy.lean; GlobalPair.sum_bad_mass_A_le is lem:qld-global-dummy for the measurements produced here.

Stated in a bipartite model #

Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The matrix proof applied the vendored seeded soundness theorem through LIDT/Adapter/Registers.lean, which Naimark-dilated the padded POVM strategy on an answer ancilla, packaged it on Fin (card) and read the conclusion back on the twice-padded state vector padState ψ along Matrix.reindex. Here the soundness theorem is the hypothesis hL, the dilation is the Halmos dilation in the players' algebras, the twice-padded state is the padded model padModel (with no F × F register: stage 3's joint measurement is internal to the padded strategy), its compressions are the two-sided compression at |t₀⟩ ⊗ |t₀⟩, the doubly extended operators of the matrix statements are operators carried along an embedding (liftOp, liftPt), the swapped padded state is the model K.swap, and GlobalPair is generic in its model, so that toSimulPair needs no register transport.

The global polynomial measurements: applying the seeded soundness theorem #

The dilation, and where the soundness theorem is applied #

The interface GlobalPair #

The error #

Stated in a bipartite model #

The error #

The expanded point measurements, carried to another model #

The commutator weights of the two strategies, carried to another model #

The output of the lemma, as a structure #

The lemma #

Stage 4b, on a GlobalPair #

The errors of stage 4c #

The evaluated marginals of the completed pair measurement #

The interface instance #

lem:qld-simultaneous, from the strategy #

The interface `GlobalPair` #

Stage 4b, on a `GlobalPair` #

`lem:qld-simultaneous`, from the strategy #