ZPC completeness of the answer-reduced game

Slice P4d of planning/aldous-lyons-track.md: a perfect Z-aligned permutation strategy of the input's n-th game gives one of the answer-reduced game presented by the typed data tdata (hasPerfectZPC_ar), on the typed game of any family of CL functions whose questions carry the oracularized input question and a question of the seeded low-degree test (ArSampler).

The strategy (II:10285, the completeness of thm:combi_ans_red):

1. the input's permutation strategy as a synchronous PCC strategy (lem:zpc-pcc), read on the seeded game inSeeded of the input;
2. its oracularization (MIPRE.SeededGame.oracleStrategy): the oracle measures both of its seed's questions jointly, an isolated player its own;
3. pulled back to the typed questions along their roles and oracularized parts (pullStrat), and pushed forward along the honest answers honestAns (arStrat).

It is PCC because the oracularization is, and perfect because the oracularized predicate accepts every outcome it produces and arPred_honest turns that into acceptance by the typed data. Its bit observables are signed permutations, diagonal at the readable bits, by HonestBits.

Support lemmas

theorem MIPRE.Tailored.AnsRed.Typed.exists_of_dist_pos {S : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype S] [Fintype X] [Fintype Y] {qA : S → X} {qB : S → Y} {x : X} {y : Y} (h : 0 < SampledGame.dist qA qB x y) : ∃ (s : S), qA s = x ∧ qB s = y

theorem MIPRE.Tailored.AnsRed.Typed.oDist_oquestion_pos {Vs : Type u_1} {A : Type u_2} [Fintype Vs] [DecidableEq Vs] [Nonempty Vs] (Sd : SeededGame Vs A) (r₁ r₂ : Role) (z : Vs) : 0 < Sd.oDist (Sd.oquestion r₁ z) (Sd.oquestion r₂ z)

The bits of the oracularized measurements

theorem MIPRE.Tailored.AnsRed.Typed.bitObs_oracleOp_oracle {Vs : Type u_1} {A : Type u_2} [Fintype Vs] [DecidableEq Vs] [Nonempty Vs] [Fintype A] [DecidableEq A] (Sd : SeededGame Vs A) (T : SyncStrategy Sd.toGame.doubled) (z : Vs) (g : OAns A → Bool) : bitObs (Sd.oracleOp T (Role.oracle, z)) g = bitObs (fun (ab : A × A) => T.P.M (false, Sd.LA z) ab.1 * T.P.M (true, Sd.LB z) ab.2) fun (ab : A × A) => g (OAns.pair ab.1 ab.2)

theorem MIPRE.Tailored.AnsRed.Typed.bitObs_oracleOp_alice {Vs : Type u_1} {A : Type u_2} [Fintype Vs] [DecidableEq Vs] [Nonempty Vs] [Fintype A] [DecidableEq A] (Sd : SeededGame Vs A) (T : SyncStrategy Sd.toGame.doubled) (x : Vs) (g : OAns A → Bool) : bitObs (Sd.oracleOp T (Role.alice, x)) g = bitObs (T.P.M (false, x)) fun (a : A) => g (OAns.single a)

theorem MIPRE.Tailored.AnsRed.Typed.bitObs_oracleOp_bob {Vs : Type u_1} {A : Type u_2} [Fintype Vs] [DecidableEq Vs] [Nonempty Vs] [Fintype A] [DecidableEq A] (Sd : SeededGame Vs A) (T : SyncStrategy Sd.toGame.doubled) (y : Vs) (g : OAns A → Bool) : bitObs (Sd.oracleOp T (Role.bob, y)) g = bitObs (T.P.M (true, y)) fun (b : A) => g (OAns.single b)

The answer-reduced typed game

def MIPRE.Tailored.AnsRed.Typed.arGraph : Role × LIDT.CL.Ty → Role × LIDT.CL.Ty → Prop

The type graph of the answer-reduced game: complete, loops included.

Equations

• MIPRE.Tailored.AnsRed.Typed.arGraph x✝¹ x✝ = True

@[instance_reducible]

instance MIPRE.Tailored.AnsRed.Typed.instDecidableRelProdRoleTyArGraph : DecidableRel arGraph

Equations

• MIPRE.Tailored.AnsRed.Typed.instDecidableRelProdRoleTyArGraph x✝¹ x✝ = isTrue trivial

instance MIPRE.Tailored.AnsRed.Typed.instNonemptyTy : Nonempty LIDT.CL.Ty

theorem MIPRE.Tailored.AnsRed.Typed.arGraph_symm (u v : Role × LIDT.CL.Ty) : arGraph u v → arGraph v u

theorem MIPRE.Tailored.AnsRed.Typed.arGraph_nonempty : (CL.Graph.edges arGraph).Nonempty

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArQ {t j ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) : Type

The typed questions of the answer-reduced game at index n.

Equations

• MIPRE.Tailored.AnsRed.Typed.ArQ V n = MIPRE.CL.Detyping.Question (MIPRE.Role × MIPRE.LIDT.CL.Ty) (Fin (V.sampler.dim n + MIPRE.Tailored.AnsRed.Typed.D j * t))

noncomputable def MIPRE.Tailored.AnsRed.Typed.arDt {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) (B : ℕ) (u v : ArQ V n) (a b : Verifier.Answers B) : Bool

The reference predicate of the answer-reduced game: the typed data accepts the answers.

Equations

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

structure MIPRE.Tailored.AnsRed.Typed.ArSampler {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) {ℓ : ℕ} (P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ) : Prop

A sampler of the answer-reduced game: CL functions on the typed questions whose questions carry the oracularized input question of the seed's input part, in the type's role, and the question of the seeded low-degree test of the seed's low-degree part, of the type's low-degree type.

• exactlyOn (w : Bool) (u : Role × LIDT.CL.Ty) : (P w u).ExactlyOn Finset.univ
• role (w : Bool) (u : Role × LIDT.CL.Ty) (s : Fin (V.sampler.dim n + D j * t) → ZMod 2) : rolePart t j (V.sampler.dim n) ((P w u).eval s) = ((inSeeded V n).oquestion u.1 (CL.leftPart s)).2
• ld (w : Bool) (u : Role × LIDT.CL.Ty) (s : Fin (V.sampler.dim n + D j * t) → ZMod 2) : ldPart t ht j (V.sampler.dim n) ((P w u).eval s) = ((regs j).pres sel u.2).eval (ldPart t ht j (V.sampler.dim n) s)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.arGame {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 : ℕ) : Game (ArQ V n) (ArQ V n) (Verifier.Answers B) (Verifier.Answers B)

The answer-reduced typed game, on the typed questions of P, accepting by the typed data.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.arGame_support {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 : ℕ) {p q : Bool × ArQ V n} (h : 0 < (arGame d hM sel L hLM V n Cc hm P B).doubled.μ p q) : p.1 = false ∧ q.1 = true ∧ ∃ (s : Fin (V.sampler.dim n + D j * t) → ZMod 2), p.2.2 = (P false p.2.1).eval s ∧ q.2.2 = (P true q.2.1).eval s

On the support of the doubled typed game, the two questions are read off one seed.

def MIPRE.Tailored.AnsRed.Typed.piQ {t j ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (p : Bool × ArQ V n) : Role × V.Questions n

The oracularized part of a typed question, with its role.

Equations

• MIPRE.Tailored.AnsRed.Typed.piQ V n p = (p.2.1.1, MIPRE.Tailored.AnsRed.Typed.rolePart t j (V.sampler.dim n) p.2.2)

theorem MIPRE.Tailored.AnsRed.Typed.piQ_eq {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) {ℓ : ℕ} (P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ) {w : Bool} {u : Role × LIDT.CL.Ty} {s : Fin (V.sampler.dim n + D j * t) → CL.𝔽₂} (hP : ArSampler hM sel V n P) : piQ V n (w, u, (P w u).eval s) = (inSeeded V n).oquestion u.1 (CL.leftPart s)

theorem MIPRE.Tailored.AnsRed.Typed.oDist_piQ_pos {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 : ℕ) (hP : ArSampler hM sel V n P) {p q : Bool × ArQ V n} (h : 0 < (arGame d hM sel L hLM V n Cc hm P B).doubled.μ p q) : 0 < (inSeeded V n).oDist (piQ V n p) (piQ V n q)

On the support, the oracularized parts of two typed questions have positive weight in the oracularized game.

The strategy

noncomputable def MIPRE.Tailored.AnsRed.Typed.auxGame {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 : ℕ) : SynchronousGame (Bool × ArQ V n) (OAns (Verifier.Answers (V.tgame n).maxLen))

The auxiliary game on the typed questions: the weights of the answer-reduced game, and the oracularized predicate on the oracularized parts.

Equations

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

def MIPRE.Tailored.AnsRed.Typed.pullStrat {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 : ℕ) (O : SyncStrategy (inSeeded V n).oracular) : SyncStrategy (auxGame d hM sel L hLM V n Cc hm P B)

The oracularized strategy, pulled back to the typed questions along their oracularized parts.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.inSync {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) : SyncStrategy (inSeeded V n).toGame.doubled

The input's synchronous strategy, read on the seeded game of the input.

Equations

• MIPRE.Tailored.AnsRed.Typed.inSync V n SV = SV.toSync.copy (MIPRE.Tailored.AnsRed.Typed.inSeeded V n).toGame.doubled

theorem MIPRE.Tailored.AnsRed.Typed.inSync_mu {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (x y : Bool × V.Questions n) : (inSeeded V n).toGame.doubled.μ x y = (V.tgame n).toGame.doubled.μ x y

theorem MIPRE.Tailored.AnsRed.Typed.isPCC_inSync {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) : (inSync V n SV).IsPCC

theorem MIPRE.Tailored.AnsRed.Typed.value_inSync {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) (h : SV.value = 1) : (inSync V n SV).value = 1

noncomputable def MIPRE.Tailored.AnsRed.Typed.orStrat {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (SV : PermStrategy (V.tgame n).doubled) : SyncStrategy (inSeeded V n).oracular

The oracularization of the input's strategy.

Equations

• MIPRE.Tailored.AnsRed.Typed.orStrat V n SV = (MIPRE.Tailored.AnsRed.Typed.inSeeded V n).oracleStrategy (MIPRE.Tailored.AnsRed.Typed.inSync V n SV) ⋯

theorem MIPRE.Tailored.AnsRed.Typed.isPCC_pullStrat {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 : ℕ) (SV : PermStrategy (V.tgame n).doubled) (hP : ArSampler hM sel V n P) : (pullStrat d hM sel L hLM V n Cc hm P B (orStrat V n SV)).IsPCC

theorem MIPRE.Tailored.AnsRed.Typed.value_pullStrat {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 : ℕ) (SV : PermStrategy (V.tgame n).doubled) (hP : ArSampler hM sel V n P) (hSV : SV.value = 1) : (pullStrat d hM sel L hLM V n Cc hm P B (orStrat V n SV)).value = 1

noncomputable def MIPRE.Tailored.AnsRed.Typed.arAns {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) {B : ℕ} (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) (p : Bool × ArQ V n) (o : OAns (Verifier.Answers (V.tgame n).maxLen)) : Verifier.Answers B

The honest answer, as an answer of the game.

Equations

• MIPRE.Tailored.AnsRed.Typed.arAns d hM sel L hLM V n Cc hm hB p o = ⟨MIPRE.Tailored.AnsRed.Typed.honestAns d hM L sel hLM V n Cc hm p.2 o, ⋯⟩

noncomputable def MIPRE.Tailored.AnsRed.Typed.arStrat {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 : ℕ} (SV : PermStrategy (V.tgame n).doubled) (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) : SyncStrategy (arGame d hM sel L hLM V n Cc hm P B).doubled

The honest strategy of the answer-reduced game.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.isPCC_arStrat {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 : ℕ} (SV : PermStrategy (V.tgame n).doubled) (hP : ArSampler hM sel V n P) (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) : (arStrat d hM sel L hLM V n Cc hm P SV hB).IsPCC

theorem MIPRE.Tailored.AnsRed.Typed.value_arStrat {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 : ℕ} (SV : PermStrategy (V.tgame n).doubled) {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) (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) (hSV : SV.value = 1) : (arStrat d hM sel L hLM V n Cc hm P SV hB).value = 1

theorem MIPRE.Tailored.AnsRed.Typed.arStrat_support {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 : ℕ} (SV : PermStrategy (V.tgame n).doubled) (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) (q : Bool × ArQ V n) (a : Verifier.Answers B) (ha : ¬List.length ↑a = len t j d L q.2.1) : (arStrat d hM sel L hLM V n Cc hm P SV hB).P.M q a = 0

The honest strategy charges only answers of the types' lengths.

theorem MIPRE.Tailored.AnsRed.Typed.isXBit_arStrat_iff {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 : ℕ} (SV : PermStrategy (V.tgame n).doubled) (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) (q : Bool × ArQ V n) (f : Verifier.Answers B → Bool) : IsXBit ((arStrat d hM sel L hLM V n Cc hm P SV hB).P.M q) f ↔ IsXBit ((inSeeded V n).oracleOp (inSync V n SV) (piQ V n q)) (f ∘ arAns d hM sel L hLM V n Cc hm hB q)

The bit observables of the honest strategy, as those of the oracularized measurement along the honest answers.

theorem MIPRE.Tailored.AnsRed.Typed.isZBit_arStrat_iff {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 : ℕ} (SV : PermStrategy (V.tgame n).doubled) (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) (q : Bool × ArQ V n) (f : Verifier.Answers B → Bool) : IsZBit ((arStrat d hM sel L hLM V n Cc hm P SV hB).P.M q) f ↔ IsZBit ((inSeeded V n).oracleOp (inSync V n SV) (piQ V n q)) (f ∘ arAns d hM sel L hLM V n Cc hm hB q)

theorem MIPRE.Tailored.AnsRed.Typed.isXBit_arStrat {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 : ℕ} (SV : PermStrategy (V.tgame n).doubled) (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) (q : Bool × ArQ V n) (i : ℕ) : IsXBit ((arStrat d hM sel L hLM V n Cc hm P SV hB).P.M q) fun (a : Verifier.Answers B) => List.getD (↑a) i false

The answer bits of the honest strategy are X-bits.

theorem MIPRE.Tailored.AnsRed.Typed.isZBit_arStrat {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 : ℕ} (SV : PermStrategy (V.tgame n).doubled) (hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B) (q : Bool × ArQ V n) {i : ℕ} (hi : i < lenR t j d L q.2.1) : IsZBit ((arStrat d hM sel L hLM V n Cc hm P SV hB).P.M q) fun (a : Verifier.Answers B) => List.getD (↑a) i false

The readable answer bits of the honest strategy are Z-bits.

Completeness

theorem MIPRE.Tailored.AnsRed.Typed.hasPerfectZPC_ar {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 : ℕ} {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) : (presented arGraph (CL.Detyping.game arGraph P (arDt d hM sel L hLM V n Cc hm B)) (tdata t ht j d L (V.sampler.dim n) sel hLM (circOf L V n Cc hm))).doubled.HasPerfectZPC

ZPC completeness of the answer-reduced game (the completeness of thm:combi_ans_red, II:10285): if the input's n-th game has a perfect Z-aligned permutation strategy, so does the answer-reduced game presented by the typed data tdata on the typed game of an answer-reduced sampler — 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.