The CL functions of the answer-reduced sampler

The answer-reduced sampler (defn:combi_ans_red, II:10285) is the direct sum of the oracularized input sampler and the seeded low-degree test's presentation, downsized over F₂ along the Shoup basis (as in the MIP* answer reduction's MIPRE.AnswerReduction.cl). Here are its CL functions, one per type (r, S) ∈ Role × LIDT.CL.Ty, the same for both players:

• the oracularized half is roleFamily of the input sampler's CL functions (the oracle reads the seed itself, an isolated player its own question), for an input of level ℓ + 1;
• the low-degree half is the presentation LIDT.CL.Regs.pres of the type, downsized and numbered (ldCl);
• both padded to max (ℓ + 1) 3 levels, the oracularized half first (arCl). Detyping adds two levels (CL.Detyping.sampler), so the output sampler has max (ℓ + 1) 3 + 2 levels, the max ((ℓ + 1) + 2) 5 of TailoredAnswerReduction, as in the MIP* answer reduction's MIPRE.AnswerReduction.level.

arSampler_arCl: they form an answer-reduced sampler (ArSampler), the hypothesis under which hasPerfectZPC_ar and valStar_ar_sound hold. The oracularized game of the input (inSeeded) reads the input's CL functions lifted one level (liftedCl), which have the same values.

def MIPRE.Tailored.AnsRed.Typed.liftedCl {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) : Player → CL.CLFun CL.𝔽₂ (Fin (V.sampler.dim n)) (ℓ + 1)

The input sampler's CL functions at index n, one level up.

Equations

• MIPRE.Tailored.AnsRed.Typed.liftedCl V n w = MIPRE.CL.CLFun.liftTo Finset.univ (ℓ + 1) ⋯ (V.sampler.cl n w)

theorem MIPRE.Tailored.AnsRed.Typed.liftedCl_exactlyOn {ℓ : ℕ} (V : TailoredVerifier ℓ) (n : ℕ) (w : Player) : (liftedCl V n w).ExactlyOn Finset.univ

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldCl (t : ℕ) (ht : 1 ≤ t) {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (S : LIDT.CL.Ty) : CL.CLFun CL.𝔽₂ (Fin (D j * t)) 3

The low-degree half: the presentation of the seeded low-degree test at a type, downsized along the Shoup basis and numbered.

Equations

• MIPRE.Tailored.AnsRed.Typed.ldCl t ht sel S = MIPRE.CL.CLFun.reindex finProdFinEquiv (MIPRE.CL.CLFun.downsize (MIPRE.SAT.shoupPowerBasis t ht) ((MIPRE.Tailored.AnsRed.Typed.regs j).pres sel S))

theorem MIPRE.Tailored.AnsRed.Typed.ldCl_exactlyOn {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (S : LIDT.CL.Ty) : (ldCl t ht sel S).ExactlyOn Finset.univ

noncomputable def MIPRE.Tailored.AnsRed.Typed.arCl {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (n : ℕ) {k : ℕ} (W : TailoredVerifier (k + 1)) (u : Role × LIDT.CL.Ty) : CL.CLFun CL.𝔽₂ (Fin (W.sampler.dim n + D j * t)) (max (k + 1) 3)

The CL function of the answer-reduced sampler at a type: the oracularized input question on the first coordinates, the seeded low-degree test's question on the rest.

Equations

• MIPRE.Tailored.AnsRed.Typed.arCl sel n W u = MIPRE.CL.CLFun.prodCL (max (k + 1) 3) (MIPRE.roleFamily (W.sampler.cl n) u.1) (MIPRE.Tailored.AnsRed.Typed.ldCl t ht sel u.2) ⋯ ⋯

theorem MIPRE.Tailored.AnsRed.Typed.arCl_exactlyOn {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (n : ℕ) {k : ℕ} (W : TailoredVerifier (k + 1)) (u : Role × LIDT.CL.Ty) : (arCl sel n W u).ExactlyOn Finset.univ

theorem MIPRE.Tailored.AnsRed.Typed.eval_arCl {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (n : ℕ) {k : ℕ} (W : TailoredVerifier (k + 1)) (u : Role × LIDT.CL.Ty) (s : Fin (W.sampler.dim n + D j * t) → CL.𝔽₂) : (arCl sel n W u).eval s = Fin.append ((roleFamily (W.sampler.cl n) u.1).eval (CL.leftPart s)) ((ldCl t ht sel u.2).eval (CL.rightPart s))

theorem MIPRE.Tailored.AnsRed.Typed.rolePart_arCl {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (n : ℕ) {k : ℕ} (W : TailoredVerifier (k + 1)) (u : Role × LIDT.CL.Ty) (s : Fin (W.sampler.dim n + D j * t) → CL.𝔽₂) : rolePart t j (W.sampler.dim n) ((arCl sel n W u).eval s) = ((inSeeded W n).oquestion u.1 (CL.leftPart s)).2

The oracularized half of a question is the oracularized question of the seed's input part, in the type's role.

theorem MIPRE.Tailored.AnsRed.Typed.ldPart_arCl {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (n : ℕ) {k : ℕ} (W : TailoredVerifier (k + 1)) (u : Role × LIDT.CL.Ty) (s : Fin (W.sampler.dim n + D j * t) → CL.𝔽₂) : ldPart t ht j (W.sampler.dim n) ((arCl sel n W u).eval s) = ((regs j).pres sel u.2).eval (ldPart t ht j (W.sampler.dim n) s)

The low-degree half of a question is the seeded test's question of the seed's low-degree part.

theorem MIPRE.Tailored.AnsRed.Typed.arSampler_arCl {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (n : ℕ) {k : ℕ} (W : TailoredVerifier (k + 1)) : ArSampler hM sel W n fun (x : Bool) (u : Role × LIDT.CL.Ty) => arCl sel n W u

The answer-reduced sampler's CL functions form an answer-reduced sampler.