The value of the padded strategy

lem:qld-global-success: the padded strategy of PaddedStrategy.lean wins the seeded low individual degree test at (q, 4m, d, 1) with probability 1 - O(δ_combine + δ_Q + md/q).

The failure probability is the average over the verifier's samples of the conditional failure at the two questions the sample generates (one_sub_povmValue_clGame), and the sample splits into the ordered pair of types and the ambient triple (u, s, raw) (sum_sample_eq). Each of the nine type pairs is bounded by an agreement defect of two families of POVMs indexed by the ambient triple, averaged uniformly:

• a line type against point, in either order, by the agreement of the line measurement read at the sample's point with the opposite party's padded point measurement, which lem:qld-padded-lines bounds (one_sub_agreeSum_lineEval_pt_le, one_sub_agreeSum_pt_lineEval_le);
• point against point by the agreement of the two padded point measurements, which lem:qld-combined-points bounds through the compressions (one_sub_agreeSum_pt_pt_le);
• a line type against itself by polynomial separation (one_sub_sum_bornProb_le_avg_eval): the two line measurements disagree only if they disagree when read at a uniformly random parameter, up to (md + 1)/q, and that disagreement is bounded through the agreement triangle fact:triangle-for-simeq by the three defects above (one_sub_agreeSum_lineEval_lineEval_le);
• the two cross pairs are always accepted.

The parameter of the sample's point is uniform on the line once the raw direction is fixed, because translating the point along the line is a bijection of the sample space that fixes the line (sum_lineEval_shift); a degenerate diagonal direction, for which this fails, has probability at most 1/q.

In a bipartite model

Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The padded strategy is a pair of families of POVMs in the expanded model N₀ = M.reg (Anc F m) (padStrat, in the players' Matrix (Anc F m) (Anc F m) _), and the stage-4a interface is padStrat_value: 1 - δ_GS ≤ N₀.povmValue (clGame hm4) (padStrat hm hm4 hPA) (padStrat hm hm4 hPB) for a legally supported projective strategy of value 1 - ε. The point measurement is the sandwich, read along (alpha, beta), so the identical-point subtest is the first agreement bound of combined_points_pts coarse-grained (sum_bornProb_le_fibre) and the line-point subtests are padded_lines_consistency verbatim: no compression is needed, and the matrix route's bornProb_extHat_ptComb_left/_right are gone. The decomposition of the failure probability into the nine type pairs is the model form of one_sub_povmValue_clGame (BipartiteModel.one_sub_povmValue_clGame, below); the per-sample families and the polynomial separation are stated in any bipartite model with the players' algebras of N₀. deltaGS, the error of lem:qld-global-success, is defined here (moved from PaddedLIDT.lean) so that the interface can be stated with it.

theorem MIPRE.BipartiteModel.one_sub_povmValue_clGame {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (PA : LIDT.CL.Question F m → POVMIn (LIDT.CL.Answer F m d ldc) 𝒜) (PB : LIDT.CL.Question F m → POVMIn (LIDT.CL.Answer F m d ldc) ℬ) : 1 - N.povmValue (LIDT.CL.clGame hm) PA PB = (↑(Fintype.card (LIDT.CL.Sample F m)))⁻¹ * ∑ sm : LIDT.CL.Sample F m, N.condFail (LIDT.CL.clGame hm) PA PB (LIDT.CL.Sample.question hm sm sm.tyA) (LIDT.CL.Sample.question hm sm sm.tyB)

The failure probability of a POVM strategy in the seeded test is the average over the verifier's samples of the conditional failure at the two questions the sample generates, in a bipartite model: the model form of MIPRE.LIDT.CL.one_sub_povmValue_clGame.

The error of lem:qld-global-success

noncomputable def MIPRE.QLD.deltaGS (q m d : ℕ) (ε : ℝ) : ℝ

δ_GS, the error of lem:qld-global-success: the padded strategy's failure probability in the seeded test at (q, 4m, d, 1).

Equations

• MIPRE.QLD.deltaGS q m d ε = 5 * (↑m * ↑m * MIPRE.QLD.deltaPairs ε (↑m * ↑d / ↑q + (↑q)⁻¹)) + 4 * MIPRE.QLD.deltaQ ε + (↑m * ↑d + 1) / ↑q

theorem MIPRE.QLD.deltaGS_nonneg {q m d : ℕ} {ε : ℝ} (hε : 0 ≤ ε) : 0 ≤ deltaGS q m d ε

@[reducible, inline]

abbrev MIPRE.QLD.Amb (F : Type u_2) (m : ℕ) : Type u_2

The verifier's ambient sample: the point, the seed and the raw direction.

Equations

• MIPRE.QLD.Amb F m = (MIPRE.LIDT.Point F (4 * m) × F × MIPRE.LIDT.Point F (4 * m))

The families of measurements indexed by the ambient sample

noncomputable def MIPRE.QLD.ptFam {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] [PartialOrder R] [StarOrderedRing R] [StarProper R] {S : Question F m → POVMIn (Answer F m d) R} (hS : ∀ (q : Question F m), IsPVMIn (S q).op) : Amb F m → POVMIn F (Matrix (Anc F m) (Anc F m) R)

The padded point measurement at the sample's point.

Equations

• MIPRE.QLD.ptFam hS x = MIPRE.QLD.padPt hS x.1

noncomputable def MIPRE.QLD.lineFam {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] [PartialOrder R] [StarOrderedRing R] [StarProper R] {S : Question F m → POVMIn (Answer F m d) R} (ty : LIDT.CL.Ty) (hS : ∀ (q : Question F m), IsPVMIn (S q).op) : Amb F m → POVMIn (LIDT.LinePoly F (m * d + 1)) (Matrix (Anc F m) (Anc F m) R)

The strategy's line measurement of type ty at the line the sample generates.

Equations

• MIPRE.QLD.lineFam hm hm4 ty hS x = MIPRE.QLD.lineMeas hm hm4 ty hS (MIPRE.LIDT.CL.rep (MIPRE.QLD.lineDir hm4 ty x.2.1 x.2.2) x.1) x.2.1 (MIPRE.QLD.rawSet hm4 ty x.2.1 x.2.2)

noncomputable def MIPRE.QLD.lineEvalFam {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] [PartialOrder R] [StarOrderedRing R] [StarProper R] {S : Question F m → POVMIn (Answer F m d) R} (ty : LIDT.CL.Ty) (hS : ∀ (q : Question F m), IsPVMIn (S q).op) : Amb F m → POVMIn F (Matrix (Anc F m) (Anc F m) R)

The line measurement read at the parameter of the sample's point.

Equations

• MIPRE.QLD.lineEvalFam hm hm4 ty hS x = MIPRE.POVMIn.map (fun (f : MIPRE.LIDT.LinePoly F (m * d + 1)) => f.eval (MIPRE.QLD.lineTau hm4 ty x.1 x.2.1 x.2.2)) (MIPRE.QLD.lineFam hm hm4 ty hS x)

Averaging over the raw direction

At a diagonal line question the strategy averages the padded line measurement over the fibre of the truncated direction, and the sample averages over the raw direction; the two together are the plain average over the raw direction.

theorem MIPRE.QLD.sum_inv_card_fiber_sum {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq β] (π : α → β) (h : α → ℝ) : ∑ a : α, (↑{a' : α | π a' = π a}.card)⁻¹ * ∑ a' : α with π a' = π a, h a' = ∑ a' : α, h a'

theorem MIPRE.QLD.sum_rawSet_fiber {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] (hm4 : 4 * m ∣ Fintype.card F) (ty : LIDT.CL.Ty) (s : F) (h : LIDT.Point F (4 * m) → ℝ) : ∑ raw : LIDT.Point F (4 * m), (↑(rawSet hm4 ty s raw).card)⁻¹ * ∑ raw' ∈ rawSet hm4 ty s raw, h raw' = ∑ raw' : LIDT.Point F (4 * m), h raw'

The strategy's raw-direction average composed with the sample's is the plain average.

The line-point agreement is the padded consistency quantity

noncomputable def MIPRE.QLD.lineTermL {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (PA : Question F m → POVMIn (Answer F m d) 𝒜) (PB : Question F m → POVMIn (Answer F m d) ℬ) (ty : LIDT.CL.Ty) (u : LIDT.Point F (4 * m)) (s : F) (raw' : LIDT.Point F (4 * m)) : ℝ

The first player's pasted line measurement at the sample's data, coarse-grained by the combining map at the sample's point, against the second player's sandwich there, averaged over the fresh randomness.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.QLD.lineTermR {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (PA : Question F m → POVMIn (Answer F m d) 𝒜) (PB : Question F m → POVMIn (Answer F m d) ℬ) (ty : LIDT.CL.Ty) (u : LIDT.Point F (4 * m)) (s : F) (raw' : LIDT.Point F (4 * m)) : ℝ

The same with the players exchanged: the first player's sandwich against the second player's pasted line.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.QLD.padGL {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (PA : Question F m → POVMIn (Answer F m d) 𝒜) (PB : Question F m → POVMIn (Answer F m d) ℬ) (ty : LIDT.CL.Ty) (a b : F) (cX cZ : LPData F m) : ℝ

The summand of avgSubAB for the first player's line against the second player's point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.QLD.padGR {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (PA : Question F m → POVMIn (Answer F m d) 𝒜) (PB : Question F m → POVMIn (Answer F m d) ℬ) (ty : LIDT.CL.Ty) (a b : F) (cX cZ : LPData F m) : ℝ

The summand of avgSubAB for the first player's point against the second player's line.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.QLD.sum_bornProb_lineEvalFam_ptFam {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) (x : Amb F m) : ∑ a : F, N.bornProb ((lineEvalFam hm hm4 ty hPA x).op a) ((ptFam hPB x).op a) = (↑(rawSet hm4 ty x.2.1 x.2.2).card)⁻¹ * ∑ raw' ∈ rawSet hm4 ty x.2.1 x.2.2, lineTermL hm hm4 N PA PB ty x.1 x.2.1 raw'

theorem MIPRE.QLD.sum_bornProb_ptFam_lineEvalFam {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) (x : Amb F m) : ∑ a : F, N.bornProb ((ptFam hPA x).op a) ((lineEvalFam hm hm4 ty hPB x).op a) = (↑(rawSet hm4 ty x.2.1 x.2.2).card)⁻¹ * ∑ raw' ∈ rawSet hm4 ty x.2.1 x.2.2, lineTermR hm hm4 N PA PB ty x.1 x.2.1 raw'

theorem MIPRE.QLD.card_amb {F : Type u_1} [Fintype F] {m : ℕ} : ↑(Fintype.card (Amb F m)) = ↑(Fintype.card F) ^ (4 * m) * (↑(Fintype.card F) * ↑(Fintype.card F) ^ (4 * m))

theorem MIPRE.QLD.card_subRand {F : Type u_1} [Fintype F] {m : ℕ} : ↑(Fintype.card (SubRand F m)) = ↑(Fintype.card F) * ↑(Fintype.card F) ^ m * (↑(Fintype.card F) * ↑(Fintype.card F) ^ m)

theorem MIPRE.QLD.sum_padGL_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (ty : LIDT.CL.Ty) (s : F) (pt raw : LIDT.Point F (4 * m)) : ∑ eX : F × LIDT.Point F m, ∑ eZ : F × LIDT.Point F m, padGL hm N PA PB ty (alph pt) (bet pt) (subX hm4 hm { pt := pt, s := s, raw := raw } eX) (subZ hm4 hm ty { pt := pt, s := s, raw := raw } eZ) = ↑(Fintype.card (SubRand F m)) * lineTermL hm hm4 N PA PB ty pt s raw

The inner sum of avgSubAB at a fixed padded point and raw direction, for the first player's line.

theorem MIPRE.QLD.sum_padGR_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (ty : LIDT.CL.Ty) (s : F) (pt raw : LIDT.Point F (4 * m)) : ∑ eX : F × LIDT.Point F m, ∑ eZ : F × LIDT.Point F m, padGR hm N PA PB ty (alph pt) (bet pt) (subX hm4 hm { pt := pt, s := s, raw := raw } eX) (subZ hm4 hm ty { pt := pt, s := s, raw := raw } eZ) = ↑(Fintype.card (SubRand F m)) * lineTermR hm hm4 N PA PB ty pt s raw

theorem MIPRE.QLD.avgSubAB_padGL {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (ty : LIDT.CL.Ty) (s : F) : avgSubAB hm4 hm ty s (padGL hm N PA PB ty) = (↑(Fintype.card F) ^ (10 * m + 2))⁻¹ * (↑(Fintype.card (SubRand F m)) * ∑ pt : LIDT.Point F (4 * m), ∑ raw : LIDT.Point F (4 * m), lineTermL hm hm4 N PA PB ty pt s raw)

theorem MIPRE.QLD.avgSubAB_padGR {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (ty : LIDT.CL.Ty) (s : F) : avgSubAB hm4 hm ty s (padGR hm N PA PB ty) = (↑(Fintype.card F) ^ (10 * m + 2))⁻¹ * (↑(Fintype.card (SubRand F m)) * ∑ pt : LIDT.Point F (4 * m), ∑ raw : LIDT.Point F (4 * m), lineTermR hm hm4 N PA PB ty pt s raw)

theorem MIPRE.QLD.inv_card_amb_eq {F : Type u_1} [Field F] [Fintype F] {m : ℕ} : (↑(Fintype.card (Amb F m)))⁻¹ = (↑(Fintype.card F))⁻¹ * ((↑(Fintype.card F) ^ (10 * m + 2))⁻¹ * ↑(Fintype.card (SubRand F m)))

The normalizations agree: the uniform average over the ambient sample is the average over the seed of the padded average avgSubAB.

theorem MIPRE.QLD.agreeSum_lineEvalFam_ptFam {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) : N.agreeSum (uniform (Amb F m)) (lineEvalFam hm hm4 ty hPA) (ptFam hPB) = (↑(Fintype.card F))⁻¹ * ∑ s : F, avgSubAB hm4 hm ty s (padGL hm N PA PB ty)

The agreement of the first player's line read at the sample's point with the second player's padded point measurement is the seed-average of the padded consistency quantity.

theorem MIPRE.QLD.agreeSum_ptFam_lineEvalFam {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (N : BipartiteModel 𝒞 (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) : N.agreeSum (uniform (Amb F m)) (ptFam hPA) (lineEvalFam hm hm4 ty hPB) = (↑(Fintype.card F))⁻¹ * ∑ s : F, avgSubAB hm4 hm ty s (padGR hm N PA PB ty)

From the padded consistency to the agreement bounds

In the expanded model the padded point measurement is the first player's sandwich read along (alpha, beta), which is exactly the point side of padded_lines_consistency and a coarse-graining of the sandwich whose agreement combined_points_pts bounds; nothing has to be compressed.

theorem MIPRE.QLD.presOf_items {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hd : 1 ≤ d) (ty : LIDT.CL.Ty) (W : Bas) : ∑ c : Content F m, (↑(Fintype.card (Content F m)))⁻¹ * ∑ f : LIDT.LinePoly F (m * d), (M.reg (Anc F m)).xSqNorm ((presOf hm ty W).lineMats d PA c f) ((presOf hm ty W).lineMats d PB c f) ≤ 172 * ε ∧ ∑ c : Content F m, (↑(Fintype.card (Content F m)))⁻¹ * ∑ a : F, (M.reg (Anc F m)).xSqNorm (hatMats PA W (c.pt W) a) ((presOf hm ty W).lineEvalMats d PB c a) ≤ 172 * ε

The two items of lem:qld-expanded-lines for the presentation of a line type.

theorem MIPRE.QLD.presOf_items_swap {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hd : 1 ≤ d) (ty : LIDT.CL.Ty) (W : Bas) : ∑ c : Content F m, (↑(Fintype.card (Content F m)))⁻¹ * ∑ a : F, (M.reg (Anc F m)).xSqNorm ((presOf hm ty W).lineEvalMats d PA c a) (hatMats PB W (c.pt W) a) ≤ 172 * ε

The second item with the players exchanged: the first player's line read at the point against the second player's point measurement.

theorem MIPRE.QLD.presOf_coll {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (ty : LIDT.CL.Ty) : ∑ c : Content F m, (↑(Fintype.card (Content F m)))⁻¹ * collProb (presOf hm ty Bas.X) d c ≤ ↑m * ↑d / ↑(Fintype.card F) + (↑(Fintype.card F))⁻¹

The collision probability of the X presentation of a line type is at most md/q + 1/q.

theorem MIPRE.QLD.one_sub_avgSubAB_padGL_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (hd : 1 ≤ d) (ty : LIDT.CL.Ty) (s : F) : 1 - avgSubAB hm4 hm ty s (padGL hm (M.reg (Anc F m)) PA PB ty) ≤ ↑m * ↑m * deltaPairs ε (↑m * ↑d / ↑(Fintype.card F) + (↑(Fintype.card F))⁻¹)

The first player's line against the second player's point, at a fixed seed: lem:qld-padded-lines in the other register version, in the expanded model.

theorem MIPRE.QLD.one_sub_avgSubAB_padGR_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (hd : 1 ≤ d) (ty : LIDT.CL.Ty) (s : F) : 1 - avgSubAB hm4 hm ty s (padGR hm (M.reg (Anc F m)) PA PB ty) ≤ ↑m * ↑m * deltaPairs ε (↑m * ↑d / ↑(Fintype.card F) + (↑(Fintype.card F))⁻¹)

The first player's point against the second player's line, at a fixed seed.

theorem MIPRE.QLD.one_sub_inv_card_mul_sum_le {F : Type u_1} [Field F] [Fintype F] {A : F → ℝ} {B : ℝ} (h : ∀ (s : F), 1 - A s ≤ B) : 1 - (↑(Fintype.card F))⁻¹ * ∑ s : F, A s ≤ B

Averaging a family of bounds over the seed.

theorem MIPRE.QLD.one_sub_agreeSum_lineEval_pt_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (hd : 1 ≤ d) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) : 1 - (M.reg (Anc F m)).agreeSum (uniform (Amb F m)) (lineEvalFam hm hm4 ty hPA) (ptFam hPB) ≤ ↑m * ↑m * deltaPairs ε (↑m * ↑d / ↑(Fintype.card F) + (↑(Fintype.card F))⁻¹)

The line-point subtests, the first player's line: the agreement of the first player's line measurement read at the sample's point with the second player's padded point measurement, averaged over the ambient sample, in the expanded model.

theorem MIPRE.QLD.one_sub_agreeSum_pt_lineEval_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (hd : 1 ≤ d) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) : 1 - (M.reg (Anc F m)).agreeSum (uniform (Amb F m)) (ptFam hPA) (lineEvalFam hm hm4 ty hPB) ≤ ↑m * ↑m * deltaPairs ε (↑m * ↑d / ↑(Fintype.card F) + (↑(Fintype.card F))⁻¹)

The line-point subtests, the second player's line.

The identical-point subtest

theorem MIPRE.QLD.avg_amb_blocks {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] (g : LIDT.Point F m → LIDT.Point F m → ℝ) : ∑ x : Amb F m, (↑(Fintype.card (Amb F m)))⁻¹ * g (xBlk x.1) (zBlk x.1) = ∑ y : LIDT.Point F m × LIDT.Point F m, (↑(Fintype.card (LIDT.Point F m × LIDT.Point F m)))⁻¹ * g y.1 y.2

A function of the two blocks of the sample's point, averaged over the ambient sample, is its average over the pair of blocks.

theorem MIPRE.QLD.one_sub_agreeSum_pt_pt_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) : 1 - (M.reg (Anc F m)).agreeSum (uniform (Amb F m)) (ptFam hPA) (ptFam hPB) ≤ deltaQ ε

The identical-point subtest: the two padded point measurements agree up to δ_Q, by the self-agreement item of lem:qld-combined-points (combined_points_pts), coarse-grained along (alpha, beta): agreement only increases under a common coarse-graining.

The identical-line subtest

Two distinct polynomial outcomes are told apart by reading both at a uniformly random parameter of the line, up to (md + 1)/q; the parameter of the sample's point is uniform on the line once the raw direction is fixed and the line is not degenerate, because translating the point along the line is a bijection of the sample space that fixes the line and shifts the parameter.

theorem MIPRE.QLD.sum_shift_param {F : Type u_1} [Field F] [Fintype F] {n : ℕ} {α : Type u_6} {β : Type u_7} (w : LIDT.Point F n) (LA : LIDT.Point F n → α) (LB : LIDT.Point F n → β) (τ : LIDT.Point F n → F) (hLA : ∀ (u : LIDT.Point F n) (t : F), LA (u + t • w) = LA u) (hLB : ∀ (u : LIDT.Point F n) (t : F), LB (u + t • w) = LB u) (hτ : ∀ (u : LIDT.Point F n) (t : F), τ (u + t • w) = τ u + t) (Φ : α → β → F → ℝ) : ∑ u : LIDT.Point F n, ∑ t : F, Φ (LA u) (LB u) t = ↑(Fintype.card F) * ∑ u : LIDT.Point F n, Φ (LA u) (LB u) (τ u)

The parameter is uniform on the line. For a quantity that depends on the sample's point only through the line it generates and the parameter of the point on it, averaging over a uniform parameter is averaging over the point, when moving the point along the line shifts its parameter by the same amount.

def MIPRE.QLD.evDef {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {𝒞' : Type u_5} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] (N : BipartiteModel 𝒞' (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (LA : POVMIn (LIDT.LinePoly F (m * d + 1)) (Matrix (Anc F m) (Anc F m) 𝒜)) (LB : POVMIn (LIDT.LinePoly F (m * d + 1)) (Matrix (Anc F m) (Anc F m) ℬ)) (t : F) : ℝ

The disagreement of two polynomial measurements read at the parameter t.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.QLD.evDef_nonneg {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {𝒞' : Type u_5} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] (N : BipartiteModel 𝒞' (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (hN : ‖N.ψ‖ = 1) (LA : POVMIn (LIDT.LinePoly F (m * d + 1)) (Matrix (Anc F m) (Anc F m) 𝒜)) (LB : POVMIn (LIDT.LinePoly F (m * d + 1)) (Matrix (Anc F m) (Anc F m) ℬ)) (t : F) : 0 ≤ evDef N LA LB t

theorem MIPRE.QLD.evDef_le_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {𝒞' : Type u_5} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] (N : BipartiteModel 𝒞' (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (LA : POVMIn (LIDT.LinePoly F (m * d + 1)) (Matrix (Anc F m) (Anc F m) 𝒜)) (LB : POVMIn (LIDT.LinePoly F (m * d + 1)) (Matrix (Anc F m) (Anc F m) ℬ)) (t : F) : evDef N LA LB t ≤ 1

theorem MIPRE.QLD.evDef_lineTau {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) {𝒞' : Type u_5} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] (N : BipartiteModel 𝒞' (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (ty : LIDT.CL.Ty) (x : Amb F m) : evDef N (lineFam hm hm4 ty hPA x) (lineFam hm hm4 ty hPB x) (lineTau hm4 ty x.1 x.2.1 x.2.2) = 1 - ∑ a : F, N.bornProb ((lineEvalFam hm hm4 ty hPA x).op a) ((lineEvalFam hm hm4 ty hPB x).op a)

The disagreement of the two line measurements read at the sample's point is the disagreement of the evaluated families.

theorem MIPRE.QLD.sum_avg_evDef_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) {𝒞' : Type u_5} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] (N : BipartiteModel 𝒞' (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (hN : ‖N.ψ‖ = 1) (ty : LIDT.CL.Ty) (s : F) (raw : LIDT.Point F (4 * m)) : ∑ u : LIDT.Point F (4 * m), (↑(Fintype.card F))⁻¹ * ∑ t : F, evDef N (lineFam hm hm4 ty hPA (u, s, raw)) (lineFam hm hm4 ty hPB (u, s, raw)) t ≤ ∑ u : LIDT.Point F (4 * m), evDef N (lineFam hm hm4 ty hPA (u, s, raw)) (lineFam hm hm4 ty hPB (u, s, raw)) (lineTau hm4 ty u s raw) + if lineDir hm4 ty s raw = 0 then ↑(Fintype.card (LIDT.Point F (4 * m))) else 0

At a fixed seed and raw direction, averaging the evaluated disagreement over the parameter is averaging it over the point, unless the direction is degenerate, in which case the average is at most one.

theorem MIPRE.QLD.sum_deg_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] (hm4 : 4 * m ∣ Fintype.card F) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) : (∑ s : F, ∑ raw : LIDT.Point F (4 * m), if lineDir hm4 ty s raw = 0 then 1 else 0) ≤ ↑(Fintype.card (LIDT.Point F (4 * m)))

Degenerate lines are rare: over the seed and the raw direction, a line type other than point describes the zero direction on at most a 1/q fraction of the samples.

theorem MIPRE.QLD.sum_amb_eq {F : Type u_1} [Fintype F] {m : ℕ} (g : Amb F m → ℝ) : ∑ x : Amb F m, g x = ∑ s : F, ∑ raw : LIDT.Point F (4 * m), ∑ u : LIDT.Point F (4 * m), g (u, s, raw)

A sum over the ambient sample, as a sum over the seed, the raw direction and the point.

theorem MIPRE.QLD.uniform_amb_nonneg {F : Type u_1} [Fintype F] {m : ℕ} (x : Amb F m) : 0 ≤ uniform (Amb F m) x

theorem MIPRE.QLD.sum_uniform_amb {F : Type u_1} [Field F] [Fintype F] {m : ℕ} : ∑ x : Amb F m, uniform (Amb F m) x = 1

theorem MIPRE.QLD.one_sub_agreeSum_uniform_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {𝒞' : Type u_5} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] (N : BipartiteModel 𝒞' (Matrix (Anc F m) (Anc F m) 𝒜) (Matrix (Anc F m) (Anc F m) ℬ)) (P : Amb F m → POVMIn F (Matrix (Anc F m) (Anc F m) 𝒜)) (Q : Amb F m → POVMIn F (Matrix (Anc F m) (Anc F m) ℬ)) : 1 - N.agreeSum (uniform (Amb F m)) P Q = ∑ x : Amb F m, uniform (Amb F m) x * (1 - ∑ a : F, N.bornProb ((P x).op a) ((Q x).op a))

The disagreement of two families, as the uniform average of the per-sample disagreements.

theorem MIPRE.QLD.one_sub_agreeSum_lineEval_lineEval_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) {M : BipartiteModel 𝒞 𝒜 ℬ} {ε : ℝ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hε : 0 ≤ ε) (hd : 1 ≤ d) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) : 1 - (M.reg (Anc F m)).agreeSum (uniform (Amb F m)) (lineEvalFam hm hm4 ty hPA) (lineEvalFam hm hm4 ty hPB) ≤ 11 * (↑m * ↑m * deltaPairs ε (↑m * ↑d / ↑(Fintype.card F) + (↑(Fintype.card F))⁻¹) + deltaQ ε)

The identical-line agreement, through the triangle: the first player's line read at the sample's point agrees with the second player's, because each agrees with the padded point measurements there.

The nine subtests, and the value

noncomputable def MIPRE.QLD.padW {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} (M : BipartiteModel 𝒞 𝒜 ℬ) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (tA tB : LIDT.CL.Ty) : ℝ

The failure weight of one ordered pair of types: the conditional failure of the padded strategy in the expanded model at the questions of the two types, averaged over the ambient sample.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.QLD.padW_point_point_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) : padW hm hm4 M hPA hPB LIDT.CL.Ty.point LIDT.CL.Ty.point ≤ deltaQ ε

theorem MIPRE.QLD.padW_line_point_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (hd : 1 ≤ d) (hlegA : LegalSupport PA) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) : padW hm hm4 M hPA hPB ty LIDT.CL.Ty.point ≤ ↑m * ↑m * deltaPairs ε (↑m * ↑d / ↑(Fintype.card F) + (↑(Fintype.card F))⁻¹)

theorem MIPRE.QLD.padW_point_line_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (hd : 1 ≤ d) (hlegB : LegalSupport PB) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) : padW hm hm4 M hPA hPB LIDT.CL.Ty.point ty ≤ ↑m * ↑m * deltaPairs ε (↑m * ↑d / ↑(Fintype.card F) + (↑(Fintype.card F))⁻¹)

theorem MIPRE.QLD.padW_aline_dline_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : ‖M.ψ‖ = 1) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) : padW hm hm4 M hPA hPB LIDT.CL.Ty.aline LIDT.CL.Ty.dline ≤ 0

theorem MIPRE.QLD.padW_dline_aline_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : ‖M.ψ‖ = 1) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) : padW hm hm4 M hPA hPB LIDT.CL.Ty.dline LIDT.CL.Ty.aline ≤ 0

theorem MIPRE.QLD.padW_line_line_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (hε : 0 ≤ ε) (hd : 1 ≤ d) (ty : LIDT.CL.Ty) (hty : ty ≠ LIDT.CL.Ty.point) : padW hm hm4 M hPA hPB ty ty ≤ 11 * (↑m * ↑m * deltaPairs ε (↑m * ↑d / ↑(Fintype.card F) + (↑(Fintype.card F))⁻¹) + deltaQ ε) + (↑m * ↑d + 1) / ↑(Fintype.card F) + (↑(Fintype.card F))⁻¹

The identical-line subtests.

theorem MIPRE.QLD.Sample.question_fst_eq_lineQ {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm4 : 4 * m ∣ Fintype.card F) (tA tB : LIDT.CL.Ty) (u : LIDT.Point F (4 * m)) (s : F) (raw : LIDT.Point F (4 * m)) : LIDT.CL.Sample.question hm4 { tyA := tA, tyB := tB, u := u, s := s, v := raw } tA = lineQ hm4 tA u s raw

theorem MIPRE.QLD.Sample.question_snd_eq_lineQ {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm4 : 4 * m ∣ Fintype.card F) (tA tB : LIDT.CL.Ty) (u : LIDT.Point F (4 * m)) (s : F) (raw : LIDT.Point F (4 * m)) : LIDT.CL.Sample.question hm4 { tyA := tA, tyB := tB, u := u, s := s, v := raw } tB = lineQ hm4 tB u s raw

theorem MIPRE.QLD.sum_ty (f : LIDT.CL.Ty → ℝ) : ∑ t : LIDT.CL.Ty, f t = f LIDT.CL.Ty.point + f LIDT.CL.Ty.aline + f LIDT.CL.Ty.dline

A sum over the three question types.

theorem MIPRE.QLD.one_sub_povmValue_padStrat_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) : 1 - (M.reg (Anc F m)).povmValue (LIDT.CL.clGame hm4) (padStrat hm hm4 hPA) (padStrat hm hm4 hPB) = 9⁻¹ * ∑ tA : LIDT.CL.Ty, ∑ tB : LIDT.CL.Ty, padW hm hm4 M hPA hPB tA tB

The failure probability of the padded strategy is the average over the nine ordered type pairs of their failure weights.

theorem MIPRE.QLD.padStrat_value {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hm4 : 4 * m ∣ Fintype.card F) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {PA : Question F m → POVMIn (Answer F m d) 𝒜} {PB : Question F m → POVMIn (Answer F m d) ℬ} {ε : ℝ} {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : ‖M.ψ‖ = 1) (hfail : 1 - M.povmValue (qldGame hm) PA PB ≤ ε) (hPA : ∀ (q : Question F m), IsPVMIn (PA q).op) (hPB : ∀ (q : Question F m), IsPVMIn (PB q).op) (hε : 0 ≤ ε) (hlegA : LegalSupport PA) (hlegB : LegalSupport PB) (hd : 1 ≤ d) : 1 - deltaGS (Fintype.card F) m d ε ≤ (M.reg (Anc F m)).povmValue (LIDT.CL.clGame hm4) (padStrat hm hm4 hPA) (padStrat hm hm4 hPB)

lem:qld-global-success: the padded strategy wins the seeded low individual degree test at (q, 4m, d, 1) with probability at least 1 - δ_GS, in the expanded model M.reg (Anc F m), with δ_GS = 5 δ_combine + 4 δ_Q + (md + 1)/q and δ_combine = m² δ_P(ε, md/q + 1/q): the stage-4a interface. For a projective strategy S : M.ProjStrat (qldGame hm) the hypotheses are S.ψ_unit, hfail : 1 - S.value ≤ ε, S.projA, S.projB.