The answer-reduced sampler

Slice P4h of planning/aldous-lyons-track.md: the sampler of the output tailored verifier of the answer reduction, as the contract TailoredAnswerReduction asks for it, a function of the input sampler and the parameters (λ, μ, σ) whose program is computed from the input sampler's in polynomial time (arSamplerProg_eq).

• arTyped: the typed sampler, the oracularized input sampler (oracleSampler) and the low-degree half (LdFamily.directSampler) side by side (TypedSampler.prodDirect); its CL functions are the answer-reduced family arCl (arTyped_cl), an answer-reduced sampler (arSampler_arCl).
• arSampler: the typed sampler detyped along the complete graph with loops (CL.Detyping.sampler), of level max (ℓ + 1) 3 + 2.
• arSampler_dist: its question distribution, read along the numbering of the detyped coordinates (vectorEquiv), is the detyped game's, which the presented answer-reduced game takes (dist_arPresented): the sampler half of TailoredVerifier.MeetsAt.

The parameters of the low-degree half come from a routine (LdRoutine), fixed with the rest of the parameters in P4i.

structure MIPRE.Tailored.AnsRed.Typed.LdRoutine : Type

A parameter routine for the low-degree half: the families of parameters at each (λ, μ, σ), and a polynomial-time map from (λ, μ, σ) to a closed program computing them at each index.

• fam : ℕ → ℕ → ℕ → LdFamily

  The parameters of the low-degree half at (λ, μ, σ).

• parPF : Cost.PolyTimeFun (ℕ × ℕ × ℕ) Cost.Prog

  The parameter program, from (λ, μ, σ).

• closed (lam mu sigma : ℕ) : Cost.Prog.WellScoped 1 (self.parPF.toFun (lam, mu, sigma))
• runs (lam mu sigma n : ℕ) : ∃ (t : ℕ), (self.parPF.toFun (lam, mu, sigma)).Runs (Cost.encode n) ((self.fam lam mu sigma).pd n) t

noncomputable def MIPRE.Tailored.AnsRed.Typed.LdRoutine.ldDirect (R : LdRoutine) (lam mu sigma : ℕ) : CL.DirectSampler 3 LIDT.CL.Ty

The low-degree half at (λ, μ, σ), directly answered.

Equations

• R.ldDirect lam mu sigma = (R.fam lam mu sigma).directSampler (R.parPF.toFun (lam, mu, sigma)) ⋯ ⋯

noncomputable def MIPRE.Tailored.AnsRed.Typed.LdRoutine.arTyped (R : LdRoutine) (lam mu sigma : ℕ) {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) : CL.TypedSampler (max (ℓ + 1) 3) (Role × LIDT.CL.Ty)

The answer-reduced typed sampler: the oracularized input sampler and the low-degree half, side by side.

Equations

• R.arTyped lam mu sigma S = (MIPRE.oracleSampler S).prodDirect (R.ldDirect lam mu sigma) (max (ℓ + 1) 3) ⋯ ⋯ ⋯

theorem MIPRE.Tailored.AnsRed.Typed.LdRoutine.arTyped_cl (R : LdRoutine) (lam mu sigma : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (n : ℕ) (w : Player) (u : Role × LIDT.CL.Ty) : (R.arTyped lam mu sigma V.sampler).cl n w u = arCl ((R.fam lam mu sigma).sel n) n V u

The typed sampler's CL functions are the answer-reduced family.

theorem MIPRE.Tailored.AnsRed.Typed.LdRoutine.arTyped_dim (R : LdRoutine) (lam mu sigma : ℕ) {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (n : ℕ) : (R.arTyped lam mu sigma S).dim n = S.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n

noncomputable def MIPRE.Tailored.AnsRed.Typed.LdRoutine.arSampler (R : LdRoutine) (lam mu sigma : ℕ) {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) : CL.Sampler (max (ℓ + 1) 3 + 2)

The answer-reduced sampler: the typed sampler detyped along the complete graph with loops.

Equations

• R.arSampler lam mu sigma S = MIPRE.CL.Detyping.sampler MIPRE.Tailored.AnsRed.Typed.arGraph (R.arTyped lam mu sigma S) ⋯

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.LdRoutine.qe (R : LdRoutine) (lam mu sigma : ℕ) {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (n : ℕ) : (CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin ((R.arTyped lam mu sigma S).dim n)) → CL.𝔽₂) ≃ (Fin ((R.arSampler lam mu sigma S).dim n) → CL.𝔽₂)

The detyped questions, numbered, as the answer-reduced sampler's questions.

Equations

• R.qe lam mu sigma S n = MIPRE.CL.Detyping.DeciderProgram.vectorEquiv ((R.arTyped lam mu sigma S).dim n)

theorem MIPRE.Tailored.AnsRed.Typed.LdRoutine.arSampler_dist (R : LdRoutine) (lam mu sigma : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (n : ℕ) {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (Dt : CL.Detyping.Question (Role × LIDT.CL.Ty) (Fin ((R.arTyped lam mu sigma V.sampler).dim n)) → CL.Detyping.Question (Role × LIDT.CL.Ty) (Fin ((R.arTyped lam mu sigma V.sampler).dim n)) → A → B → Bool) (x y : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin ((R.arTyped lam mu sigma V.sampler).dim n)) → CL.𝔽₂) : (R.arSampler lam mu sigma V.sampler).dist n ((R.qe lam mu sigma V.sampler n) x) ((R.qe lam mu sigma V.sampler n) y) = (CL.Detyping.game arGraph (fun (x : Bool) (u : Role × LIDT.CL.Ty) => arCl ((R.fam lam mu sigma).sel n) n V u) Dt).μ x y

The question distribution of the answer-reduced sampler is the detyped game's, read along the numbering.

The program

noncomputable def MIPRE.Tailored.AnsRed.Typed.LdRoutine.typedPF (R : LdRoutine) (ℓ : ℕ) : Cost.PolyTimeFun (Cost.Prog × ℕ × ℕ × ℕ) Cost.Prog

The typed sampler's program, from the input sampler's and (λ, μ, σ).

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.LdRoutine.arSamplerProg (R : LdRoutine) (ℓ : ℕ) : Cost.PolyTimeFun (Cost.Prog × ℕ × ℕ × ℕ) Cost.Prog

The answer-reduced sampler's program, from the input sampler's and (λ, μ, σ).

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.LdRoutine.arSamplerProg_eq (R : LdRoutine) (lam mu sigma : ℕ) {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) : (R.arSamplerProg ℓ).toFun (S.prog, lam, mu, sigma) = (R.arSampler lam mu sigma S).prog

The presented game's weights

theorem MIPRE.Tailored.AnsRed.Typed.dist_arPresented {d : ℕ} (R : LdRoutine) (lam mu sigma : ℕ) {ℓ : ℕ} {V : TailoredVerifier (ℓ + 1)} {n : ℕ} {L : PcpDims} {hLM : L.m ≤ 2 ^ (R.fam lam mu sigma).j n} {Cc : V.Questions n → SAT.Circuit} {hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m} {B : ℕ} (x y : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin ((R.arTyped lam mu sigma V.sampler).dim n)) → CL.𝔽₂) : (R.arSampler lam mu sigma V.sampler).dist n ((R.qe lam mu sigma V.sampler n) x) ((R.qe lam mu sigma V.sampler n) y) = (arPresented d ⋯ ((R.fam lam mu sigma).sel n) L hLM V n Cc hm (fun (x : Bool) (u : Role × LIDT.CL.Ty) => arCl ((R.fam lam mu sigma).sel n) n V u) B).μ x y

The answer-reduced sampler's distribution is the presented game's weights, along the numbering of the detyped questions.