Soundness of answer reduction: the PCP's soundness

Piece AR-5e of planning/answer-reduction.md, concluded (lem:ar-ora): the hypothesis PcpSound of SoundDecoded holds for the answer-reduced verifier's game check, with the decoder decAns, which reads a polynomial's Boolean values as the answer vector of a short answer.

An outcome f of the extracted J carries a PCP proof (pcpOf): its five answer polynomials are f's first five components read on their blocks, its constraint polynomials are the rest. When f is placed on its blocks, the evaluations the game check reads are that proof's (eval_ofProof_pcpOf), so the check accepting at more than half the points is the PCP verifier accepting the proof there, and the PCP decider's soundness (SAT.PcpDecider.soundness) decodes the proof's first two answer polynomials to answers the input decider accepts. Those answers are at most inAns long, since the input decider rejects longer ones, and the answer vector determines a short answer (SAT.answerVec_injective), so they are what decAns returns.

The decoder

noncomputable def MIPRE.AnswerReduction.decAns (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B' : ℕ) (g : MvPolynomial (Fin P.m) (Fq P hk)) : Verifier.Answers B'

The decoder: the answer of length at most B' whose answer vector a polynomial's Boolean values are, where there is one.

Equations

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

theorem MIPRE.AnswerReduction.decAns_eq (P : SAT.PcpParams) (hk : 1 ≤ P.k) (B' : ℕ) (h2 : 2 * B' ≤ 2 ^ P.m) {g : MvPolynomial (Fin P.m) (Fq P hk)} {a : Cost.BitStr} (ha : List.length a ≤ B') (hg : LowDegree.coded g = SAT.answerVec (Fq P hk) P.m a) : decAns P hk B' g = ⟨a, ha⟩

The decoder returns the answer a polynomial encodes, when answers of length B' fit in the first half of the 2^m positions.

The PCP proof an outcome carries

noncomputable def MIPRE.AnswerReduction.pcpOf (P : SAT.PcpParams) (hk : 1 ≤ P.k) (f : Poly6 P hk) : SAT.PcpProof P (Fq P hk)

The PCP proof an outcome of J carries: its first five components read on their blocks, then the remaining m' + 1 as the constraint polynomials.

Equations

• MIPRE.AnswerReduction.pcpOf P hk f = { g := fun (i : Fin 5) => MIPRE.AnswerReduction.gPoly P hk i f, c := fun (j : Fin (P.m' + 1)) => (f ⟨↑j + 5, ⋯⟩).toMv, degreeOf_g := ⋯, degreeOf_c := ⋯ }

theorem MIPRE.AnswerReduction.eval_ofProof_pcpOf (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {f : Poly6 P hk} (hbl : BlockLocal P hk f) (z : Fin P.m' → Fq P hk) : (fun (j : Fin (P.m' + 6)) => (MvPolynomial.eval z) ((ofProof hk (pcpOf P hk f)).c j)) = fun (j : Fin (P.m' + 6)) => (f j).eval z

The evaluations of a placed outcome are its proof's: the sixth copy's data built from the proof evaluates as the outcome does.

The PCP's soundness, for the answer-reduced verifier

theorem MIPRE.AnswerReduction.pcpSound (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (hF : ShoupField PD) (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hV : V.Within n (inBudget lam mu n)) (hsz : V.decider.size ≤ sigma) : PcpSound V n ((family PD lam mu sigma).par n) ⋯ (chk PD V lam mu sigma n) (inAns lam mu n) (decAns ((family PD lam mu sigma).par n) ⋯ (inAns lam mu n))

The PCP's soundness, as the decoded strategy needs it, for the answer-reduced verifier's game check and the decoder decAns.

theorem MIPRE.AnswerReduction.val_ge_of_typedGame (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 𝒞 𝒜 ℬ} (hL : LIDT.Simul.SoundIn M) {ω : ValueModel} (hω : ω.OracularSound) (hdom : ω.Dominates M) (hF : ShoupField PD) (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hV : V.Within n (inBudget lam mu n)) (hsz : V.decider.size ≤ sigma) (B : ℕ) (T : M.ProjStrat (typedGame V n ((family PD lam mu sigma).par n) ⋯ ((family PD lam mu sigma).sel n) ((family PD lam mu sigma).sel' n) (chk PD V lam mu sigma n) B)) : 1 - 24 * √(7 * errD V n ((family PD lam mu sigma).par n) ⋯ ((family PD lam mu sigma).sel n) ((family PD lam mu sigma).sel' n) (chk PD V lam mu sigma n) B T) ≤ V.val ω n (inAns lam mu n)

The input verifier's value from a projective strategy for the answer-reduced typed game, in a bipartite model where the low-individual-degree test is sound and a value model where oracularization is sound that dominates it: at least 1 - 24 √(7 errD), errD the combined error of the strategy's analysis.