Soundness of answer reduction: the extracted low-degree measurements

Piece AR-5c of planning/answer-reduction.md (claim:ar-3, claim:ar-4): the quantum soundness of the seeded CL test applied to each per-seed strategy of MIPRE/Background/AnswerReduction/SoundIsolate, giving for each copy and each oracle half a pair of projective measurements of polynomials, one in each player's algebra (GA1, GB1 for copies 1–5, JA, JB for the sixth copy), each consistent with the other player's point measurements and with each other, at the error δ_sim of that seed's failure.

The soundness of the seeded test is a hypothesis on the model, hL : LIDT.Simul.SoundIn M, in the shape of LIDT.Simul.clSoundness: that theorem is its tensor-product instance (LIDT.Simul.soundIn_tensor), and its commuting-operator form is Phase 6 of planning/mipco-track.md. The extracted measurements are the ones it provides, chosen per seed.

The errors are averaged over the seeds by Jensen's inequality (sum_deltaSim_le): δ_sim is concave in the failure, so the average error is at most the error of the average failure, which is at most 324 times the typed failure.

theorem MIPRE.LIDT.Simul.sum_rpow_le {ι : Type u_1} [Fintype ι] {b : ℝ} (hb0 : 0 ≤ b) (hb1 : b ≤ 1) (ε : ι → ℝ) (hε : ∀ (i : ι), 0 ≤ ε i) {E : ℝ} (hE : ∑ i : ι, ε i ≤ ↑(Fintype.card ι) * E) : ∑ i : ι, ε i ^ b ≤ ↑(Fintype.card ι) * E ^ b

Jensen's inequality for ε ↦ ε^b, 0 ≤ b ≤ 1, on a finite family with average at most E.

theorem MIPRE.LIDT.Simul.sum_deltaSim_le {ι : Type u_1} [Fintype ι] (q m d r : ℕ) (ε : ι → ℝ) (hε : ∀ (i : ι), 0 ≤ ε i) {E : ℝ} (hE : ∑ i : ι, ε i ≤ ↑(Fintype.card ι) * E) : ∑ i : ι, deltaSim q m d r (ε i) ≤ ↑(Fintype.card ι) * deltaSim q m d r E

δ_sim averages: the average of δ_sim over a family of failures is at most δ_sim of any bound on their average.

theorem MIPRE.LIDT.Simul.deltaSim_nonneg (q m d r : ℕ) {ε : ℝ} (hε : 0 ≤ ε) : 0 ≤ deltaSim q m d r ε

noncomputable def MIPRE.AnswerReduction.eps1 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (r : Role) (i : Fin 5) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : ℝ

The failure of the per-seed strategy of copy i ≤ 5 at role r and oracle half y.

Equations

• MIPRE.AnswerReduction.eps1 V n P hk S S' check B T r i y = 1 - (MIPRE.AnswerReduction.copyStrategy V n P hk S S' check B T r i y).value

noncomputable def MIPRE.AnswerReduction.eps6 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : ℝ

The failure of the sixth copy's per-seed strategy at oracle half y.

Equations

• MIPRE.AnswerReduction.eps6 V n P hk S S' check B T y = 1 - (MIPRE.AnswerReduction.copyStrategy6 V n P hk S S' check B T y).value

theorem MIPRE.AnswerReduction.eps1_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (r : Role) (i : Fin 5) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : 0 ≤ eps1 V n P hk S S' check B T r i y

theorem MIPRE.AnswerReduction.eps6_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : 0 ≤ eps6 V n P hk S S' check B T y

@[reducible, inline]

abbrev MIPRE.AnswerReduction.Poly1 (P : SAT.PcpParams) (hk : 1 ≤ P.k) : Type

The polynomial measurements of copy i ≤ 5: tuples of one polynomial in m variables.

Equations

• MIPRE.AnswerReduction.Poly1 P hk = (Fin 1 → MIPRE.LIDT.LowIndDegPoly)

@[reducible, inline]

abbrev MIPRE.AnswerReduction.Poly6 (P : SAT.PcpParams) (hk : 1 ≤ P.k) : Type

The polynomial measurements of the sixth copy: m' + 6 polynomials in m' variables.

Equations

• MIPRE.AnswerReduction.Poly6 P hk = (Fin (P.m' + 6) → MIPRE.LIDT.LowIndDegPoly)

theorem MIPRE.AnswerReduction.card_fq (P : SAT.PcpParams) (hk : 1 ≤ P.k) : Fintype.card (Fq P hk) = 2 ^ P.k

theorem MIPRE.AnswerReduction.one_le_dPcp : 1 ≤ dPcp

theorem MIPRE.AnswerReduction.exists_ext1 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (r : Role) (i : Fin 5) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : ∃ (GA : POVMIn (Poly1 P hk) 𝒜) (GB : POVMIn (Poly1 P hk) ℬ), IsPVMIn GA.op ∧ IsPVMIn GB.op ∧ M.inconsistency (uniform (Fin P.m → Fq P hk)) (LIDT.Simul.tuplePOVMAIn hm (copyStrategy V n P hk S S' check B T r i y)) (LIDT.Simul.evalTuplePOVMIn GB) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m dPcp 1 (eps1 V n P hk S S' check B T r i y) ∧ M.inconsistency (uniform (Fin P.m → Fq P hk)) (LIDT.Simul.evalTuplePOVMIn GA) (LIDT.Simul.tuplePOVMBIn hm (copyStrategy V n P hk S S' check B T r i y)) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m dPcp 1 (eps1 V n P hk S S' check B T r i y) ∧ (M.inconsistency (uniform Unit) (fun (x : Unit) => GA) fun (x : Unit) => GB) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m dPcp 1 (eps1 V n P hk S S' check B T r i y)

theorem MIPRE.AnswerReduction.exists_ext6 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : ∃ (GA : POVMIn (Poly6 P hk) 𝒜) (GB : POVMIn (Poly6 P hk) ℬ), IsPVMIn GA.op ∧ IsPVMIn GB.op ∧ M.inconsistency (uniform (Fin P.m' → Fq P hk)) (LIDT.Simul.tuplePOVMAIn hm' (copyStrategy6 V n P hk S S' check B T y)) (LIDT.Simul.evalTuplePOVMIn GB) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m' dPcp (P.m' + 6) (eps6 V n P hk S S' check B T y) ∧ M.inconsistency (uniform (Fin P.m' → Fq P hk)) (LIDT.Simul.evalTuplePOVMIn GA) (LIDT.Simul.tuplePOVMBIn hm' (copyStrategy6 V n P hk S S' check B T y)) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m' dPcp (P.m' + 6) (eps6 V n P hk S S' check B T y) ∧ (M.inconsistency (uniform Unit) (fun (x : Unit) => GA) fun (x : Unit) => GB) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m' dPcp (P.m' + 6) (eps6 V n P hk S S' check B T y)

noncomputable def MIPRE.AnswerReduction.GA1 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (r : Role) (i : Fin 5) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : POVMIn (Poly1 P hk) 𝒜

Alice's polynomial measurement of copy i ≤ 5 at role r and oracle half y.

Equations

• MIPRE.AnswerReduction.GA1 V n P hk S S' check B T hL r i y = ⋯.choose

noncomputable def MIPRE.AnswerReduction.GB1 {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (r : Role) (i : Fin 5) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : POVMIn (Poly1 P hk) ℬ

Bob's polynomial measurement of copy i ≤ 5 at role r and oracle half y.

Equations

• MIPRE.AnswerReduction.GB1 V n P hk S S' check B T hL r i y = ⋯.choose

noncomputable def MIPRE.AnswerReduction.JA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : POVMIn (Poly6 P hk) 𝒜

Alice's simultaneous polynomial measurement of the sixth copy at oracle half y.

Equations

• MIPRE.AnswerReduction.JA V n P hk S S' check B T hL y = ⋯.choose

noncomputable def MIPRE.AnswerReduction.JB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : POVMIn (Poly6 P hk) ℬ

Bob's simultaneous polynomial measurement of the sixth copy at oracle half y.

Equations

• MIPRE.AnswerReduction.JB V n P hk S S' check B T hL y = ⋯.choose

theorem MIPRE.AnswerReduction.ext1_proj {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (r : Role) (i : Fin 5) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : IsPVMIn (GA1 V n P hk S S' check B T ⋯ r i y).op ∧ IsPVMIn (GB1 V n P hk S S' check B T ⋯ r i y).op

The polynomial measurements of copies 1–5 are projective.

theorem MIPRE.AnswerReduction.ext6_proj {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : IsPVMIn (JA V n P hk S S' check B T ⋯ y).op ∧ IsPVMIn (JB V n P hk S S' check B T ⋯ y).op

The simultaneous polynomial measurements of the sixth copy are projective.

theorem MIPRE.AnswerReduction.ext1_spec {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (r : Role) (i : Fin 5) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : M.inconsistency (uniform (Fin P.m → Fq P hk)) (LIDT.Simul.tuplePOVMAIn hm (copyStrategy V n P hk S S' check B T r i y)) (LIDT.Simul.evalTuplePOVMIn (GB1 V n P hk S S' check B T ⋯ r i y)) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m dPcp 1 (eps1 V n P hk S S' check B T r i y) ∧ M.inconsistency (uniform (Fin P.m → Fq P hk)) (LIDT.Simul.evalTuplePOVMIn (GA1 V n P hk S S' check B T ⋯ r i y)) (LIDT.Simul.tuplePOVMBIn hm (copyStrategy V n P hk S S' check B T r i y)) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m dPcp 1 (eps1 V n P hk S S' check B T r i y) ∧ (M.inconsistency (uniform Unit) (fun (x : Unit) => GA1 V n P hk S S' check B T ⋯ r i y) fun (x : Unit) => GB1 V n P hk S S' check B T ⋯ r i y) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m dPcp 1 (eps1 V n P hk S S' check B T r i y)

The three conclusions for copies 1–5.

theorem MIPRE.AnswerReduction.ext6_spec {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) (hL : LIDT.Simul.SoundIn M) (y : Fin (V.sampler.dim n) → CL.𝔽₂) : M.inconsistency (uniform (Fin P.m' → Fq P hk)) (LIDT.Simul.tuplePOVMAIn hm' (copyStrategy6 V n P hk S S' check B T y)) (LIDT.Simul.evalTuplePOVMIn (JB V n P hk S S' check B T ⋯ y)) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m' dPcp (P.m' + 6) (eps6 V n P hk S S' check B T y) ∧ M.inconsistency (uniform (Fin P.m' → Fq P hk)) (LIDT.Simul.evalTuplePOVMIn (JA V n P hk S S' check B T ⋯ y)) (LIDT.Simul.tuplePOVMBIn hm' (copyStrategy6 V n P hk S S' check B T y)) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m' dPcp (P.m' + 6) (eps6 V n P hk S S' check B T y) ∧ (M.inconsistency (uniform Unit) (fun (x : Unit) => JA V n P hk S S' check B T ⋯ y) fun (x : Unit) => JB V n P hk S S' check B T ⋯ y) ≤ LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m' dPcp (P.m' + 6) (eps6 V n P hk S S' check B T y)

The three conclusions for the sixth copy.

theorem MIPRE.AnswerReduction.sum_deltaSim1_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) {r : Role} {i : Fin 5} (hr : LDStep r i) : ∑ x₀ : Fin (V.sampler.dim n) → CL.𝔽₂, LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m dPcp 1 (eps1 V n P hk S S' check B T r i ((roleFamily (V.sampler.cl n) r).eval x₀)) ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m dPcp 1 (324 * (1 - T.value))

The averaged error of copies 1–5, at a role pair where the copy is tested.

theorem MIPRE.AnswerReduction.sum_deltaSim6_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (B : ℕ) (T : M.ProjStrat (typedGame V n P hk S S' check B)) : ∑ x₀ : Fin (V.sampler.dim n) → CL.𝔽₂, LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m' dPcp (P.m' + 6) (eps6 V n P hk S S' check B T ((roleFamily (V.sampler.cl n) Role.oracle).eval x₀)) ≤ ↑(Fintype.card (Fin (V.sampler.dim n) → CL.𝔽₂)) * LIDT.Simul.deltaSim (Fintype.card (Fq P hk)) P.m' dPcp (P.m' + 6) (324 * (1 - T.value))

The averaged error of the sixth copy.