The output verifier of the answer reduction, from its specification

Slice P4h of planning/aldous-lyons-track.md, its semantic half. The output tailored verifier of the answer reduction at an index n meets the answer-reduced game presented by the typed data tdata on the typed game of an answer-reduced sampler (ArMeets) when its sampler's distribution is the presented game's weights along an equivalence of the questions, and its two programs output the presented lengths and constraints (TailoredVerifier.MeetsAt). Then its n-th game extends the presented one, and the two clauses of prop:completeness_soundness_combi_ans_red (II:10487) carry over to it:

• hasPerfectZPC_of_arMeets: completeness, from hasPerfectZPC_ar (P4d);
• valStar_sound_of_arMeets: soundness, from valStar_ar_sound (P4e).

What remains for the contract is the output's programs and the proof that they meet the presented game (P4h's programs), and the parameters under which the hypotheses hold (P4i).

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.arPresented {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (L : PcpDims) (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (Cc : V.Questions n → SAT.Circuit) (hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m) {ℓ : ℕ} (P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ) (B : ℕ) : TailoredGame (CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D j * t)) → ZMod 2)

The answer-reduced game presented by the typed data, on the typed game of the CL functions P, with answers bounded by B.

Equations

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

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArMeets {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (L : PcpDims) (hLM : L.m ≤ 2 ^ j) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (Cc : V.Questions n → SAT.Circuit) (hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m) {ℓ : ℕ} (P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ) (B : ℕ) {ℓW : ℕ} (W : TailoredVerifier ℓW) (e : (CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D j * t)) → ZMod 2) ≃ W.Questions n) : Prop

The output verifier W meets the presented answer-reduced game at n along e.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArMeets d hM sel L hLM V n Cc hm P B W e = W.MeetsAt n (MIPRE.Tailored.AnsRed.Typed.arPresented d hM sel L hLM V n Cc hm P B) e

theorem MIPRE.Tailored.AnsRed.Typed.hasPerfectZPC_of_arMeets {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} {sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} {Cc : V.Questions n → SAT.Circuit} {hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m} {ℓ : ℕ} {P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ} {B ℓW : ℕ} {W : TailoredVerifier ℓW} {e : (CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D j * t)) → ZMod 2) ≃ W.Questions n} (h : ArMeets d hM sel L hLM V n Cc hm P B W e) {prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)} {Tt : ℕ} (H : HonestHyp L V n prm Cc Tt) (hd : 17 ≤ d) (hP : ArSampler hM sel V n P) (hℓ : 0 < ℓ) (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) (hV : V.HasPerfectZPC n) : W.HasPerfectZPC n

Completeness of the output verifier: a perfect ZPC strategy of the input's n-th game gives one of the output's, for a degree d ≥ 17, an answer bound at least the types' lengths, and circuits under which the honest PCPs of accepted answers satisfy the checks.

theorem MIPRE.Tailored.AnsRed.Typed.valStar_sound_of_arMeets {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} {sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM} {L : PcpDims} {hLM : L.m ≤ 2 ^ j} {ℓV : ℕ} {V : TailoredVerifier ℓV} {n : ℕ} {Cc : V.Questions n → SAT.Circuit} {hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m} {ℓ : ℕ} {P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ} {B ℓW : ℕ} {W : TailoredVerifier ℓW} {e : (CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D j * t)) → ZMod 2) ≃ W.Questions n} (h : ArMeets d hM sel L hLM V n Cc hm P B W e) {prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)} {Tt : ℕ} (H : HonestHyp L V n prm Cc Tt) (hd : 1 ≤ d) (hP : ArSampler hM sel V n P) (hℓ : 0 < ℓ) (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) (hq : 2 * ((2 ^ j + 1) * d) ≤ Fintype.card (Fq t ht)) (hτ : 2 * (L.m * chkDeg 5 d) ≤ Fintype.card (Fq t ht)) {ε : ℝ} (hε : 0 < ε) (hv : 1 - ε < W.valStar n) : 1 - 24 * √(errAR t ht j d L (16 ^ 9 * ε)) ≤ V.valStar n

Soundness of the output verifier: if the output's n-th game has val* > 1 - ε, then val*(𝒱_n) ≥ 1 - 24 √(errAR (16⁹ ε)), once the field has 2 (M + 1) d and 2 m (5 + 6(d + 1)) elements.