The typed answer-reduced sampler

Piece AR-3d of planning/answer-reduction.md, concluded: the sampler Ŝ^ar of the typed answer-reduced verifier as a CL.TypedSampler over the types Role × PcpTy, at the level max (ℓ + 1) 3.

It is the product (CL.TypedSampler.prodDirect) of the typed oracularized sampler of the input sampler (oracleSampler, piece O3) and the PCP sampler, answered directly (pcpDirect) with the parameters of family computed by parProg. Its typed CL functions are those of the typed game (typedSampler_cl), and its program depends only on the input sampler's program and on (λ, μ, σ) (typedSampler_prog): the structural half of lem:ar-sampler-independence.

noncomputable def MIPRE.AnswerReduction.pcpDirect (PD : SAT.PcpDecider) (lam mu sigma : ℕ) : CL.DirectSampler 3 Pcp.PcpTy

The PCP half, directly answered.

Equations

• MIPRE.AnswerReduction.pcpDirect PD lam mu sigma = (MIPRE.AnswerReduction.family PD lam mu sigma).directSampler (MIPRE.AnswerReduction.parProg PD lam mu sigma) ⋯ ⋯

noncomputable def MIPRE.AnswerReduction.typedSampler {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (PD : SAT.PcpDecider) (lam mu sigma : ℕ) : CL.TypedSampler (level ℓ) ArTy

The typed answer-reduced sampler.

Equations

• MIPRE.AnswerReduction.typedSampler S PD lam mu sigma = (MIPRE.oracleSampler S).prodDirect (MIPRE.AnswerReduction.pcpDirect PD lam mu sigma) (MIPRE.AnswerReduction.level ℓ) ⋯ ⋯ ⋯

theorem MIPRE.AnswerReduction.typedSampler_cl {ℓ : ℕ} (PD : SAT.PcpDecider) (lam mu sigma : ℕ) (V : Verifier (ℓ + 1)) (n : ℕ) (w : Player) (rt : ArTy) : (typedSampler V.sampler PD lam mu sigma).cl n w rt = cl V n ((family PD lam mu sigma).par n) ⋯ ((family PD lam mu sigma).sel n) ((family PD lam mu sigma).sel' n) rt

The typed CL functions are those of the typed answer-reduced game.

theorem MIPRE.AnswerReduction.typedSampler_dim {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : (typedSampler S PD lam mu sigma).dim n = S.dim n + Pcp.pcpDim (arPar PD lam mu sigma n) * (arPar PD lam mu sigma n).k

theorem MIPRE.AnswerReduction.typedSampler_prog {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (PD : SAT.PcpDecider) (lam mu sigma : ℕ) : (typedSampler S PD lam mu sigma).prog = CL.ProductSampler.prog answerProg dimProg (OracleSampler.prog S.prog) (ℓ + 1) (parProg PD lam mu sigma)

The program depends only on the input sampler's program and on (λ, μ, σ).