Soundness of answer reduction: the setup

Piece AR-5a of planning/answer-reduction.md (lem:ar-soundness-setup): a strategy for the answer-reduced verifier's game at the answer cut, of value at least 1 - ε, gives a strategy for the typed answer-reduced game (typedGame, with the predicate typedPred) of value at least 1 - 16^{54} ε, on the same state (typedStrategy_value_ge). This is the detyping restriction in a bipartite model (CL.Detyping.restrict_povmValue_ge), after reading the compiled verifier's questions in the finite detyped game (CL.Detyping.DeciderProgram.vectorEquiv), through the typed decider's acceptance law (typedPredicate_eq).

The strategy stays a projective strategy in a bipartite model (BipartiteModel.ProjStrat): two families of projective measurements, one per player. The paper symmetrizes it first (lem:symmetric-strat); the Lean does not, and derives every relation for each ordered pair of players from the ordered pair of types that carries it.

@[reducible, inline]

noncomputable abbrev MIPRE.AnswerReduction.arTypedGame (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) : Game (CL.Detyping.Question ArTy (Fin (dim V n ((family PD lam mu sigma).par n)))) (CL.Detyping.Question ArTy (Fin (dim V n ((family PD lam mu sigma).par n)))) (Verifier.Answers (cutVal ((family PD lam mu sigma).par n))) (Verifier.Answers (cutVal ((family PD lam mu sigma).par n)))

The typed answer-reduced game of V at index n, at the answer cut.

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.AnswerReduction.arFiniteGame (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) : Game (CL.Detyping.Coord ArTy (Fin ((typedSampler V.sampler PD lam mu sigma).dim n)) → ZMod 2) (CL.Detyping.Coord ArTy (Fin ((typedSampler V.sampler PD lam mu sigma).dim n)) → ZMod 2) (Verifier.Answers ((arCut PD lam mu sigma).outer n)) (Verifier.Answers ((arCut PD lam mu sigma).outer n))

The finite detyped game the answer-reduced verifier's game at the answer cut numbers. The derived decidable equality of the types is large, and its question set's Fintype instance needs a larger instance search.

Equations

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

noncomputable def MIPRE.AnswerReduction.typedStrategy (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (R : M.ProjStrat ((arVerifier PD lam mu sigma V).game n (cutVal (arPar PD lam mu sigma n)))) : M.ProjStrat (arTypedGame PD lam mu sigma V n)

The typed strategy of a projective strategy, in a bipartite model, for the answer-reduced verifier's game at the answer cut: the strategy read in the finite detyped game its questions number (CL.Detyping.DeciderProgram.vectorEquiv), then detyping's restriction to the fixed graph views, read in the typed game with the predicate typedPred. The same measurements, asked at other questions: projective, on the same state.

Equations

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

theorem MIPRE.AnswerReduction.typedStrategy_value_ge (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (R : M.ProjStrat ((arVerifier PD lam mu sigma V).game n (cutVal (arPar PD lam mu sigma n)))) {ε : ℝ} (hR : 1 - ε ≤ R.value) : 1 - 16 ^ Fintype.card ArTy * ε ≤ (typedStrategy PD lam mu sigma V n R).value

Detyping soundness for answer reduction, in a bipartite model: the typed strategy loses at most a factor 16^{54} in failure probability.