The honest answers of the answer-reduced game

The completeness of the answer-reduced game (slice P4d of planning/aldous-lyons-track.md): the honest strategy measures the oracularized input strategy and answers, at a typed question, with the honest low-degree answers of the polynomials of the honest PCP of the input answers (cor:functional_viewpoint_final) — the oracle with all of them, an isolated player with the two of its own answer. This file defines those answers as bit strings and proves the four checks of the answer-reduced predicate on them, for polynomials of the right shape.

• encCws: codewords of field elements as bit strings, the inverse of cw (cw_encCws); honestBits: the honest low-degree answer of a tuple of polynomials, which decAns reads back as LIDT.CL.honest (decAns_honestBits).
• ldPolys: a role's codewords of a PCP, on the test's variables.
• The checks: accepts_honestBits (low degree: LIDT.CL.accepts_honest on the common sample), isoAgrees_honestBits (consistency), indOK_honestBits (indifference: a polynomial missing a variable is constant along its axis), passesV_honestBits (the proof check, from the identities).
• honestAns: the honest answer at a typed question to an answer of the oracularized input game (MIPRE.SeededGame.oracular of inSeeded), and arPred_honest, the functional half of completeness: at two questions read off one seed, answers the oracularized predicate accepts give honest answers the answer-reduced predicate accepts.

Codewords as bit strings

theorem MIPRE.Tailored.AnsRed.Typed.ofBool_decide_eq_one (z : ZMod 2) : LowDegree.ofBool (decide (z = 1)) = z

noncomputable def MIPRE.Tailored.AnsRed.Typed.encCws (t : ℕ) (ht : 1 ≤ t) (k nc : ℕ) (coef : ℕ → ℕ → Fq t ht) : Cost.BitStr

k codewords of nc field elements as a bit string, each element as its t canonical bits, codeword after codeword: the layout cw reads.

Equations

• MIPRE.Tailored.AnsRed.Typed.encCws t ht k nc coef = List.ofFn fun (i : Fin (k * nc * t)) => decide ((MIPRE.SAT.shoupCoordinateEquiv t ht) (coef (↑i / (nc * t)) (↑i / t % nc)) ⟨↑i % t, ⋯⟩ = 1)

theorem MIPRE.Tailored.AnsRed.Typed.length_encCws {t : ℕ} {ht : 1 ≤ t} (k nc : ℕ) (coef : ℕ → ℕ → Fq t ht) : List.length (encCws t ht k nc coef) = k * nc * t

theorem MIPRE.Tailored.AnsRed.Typed.getD_encCws {t : ℕ} {ht : 1 ≤ t} {k nc : ℕ} (coef : ℕ → ℕ → Fq t ht) {c e i : ℕ} (hc : c < k) (he : e < nc) (hi : i < t) : List.getD (encCws t ht k nc coef) ((c * nc + e) * t + i) false = decide ((SAT.shoupCoordinateEquiv t ht) (coef c e) ⟨i, hi⟩ = 1)

theorem MIPRE.Tailored.AnsRed.Typed.cw_encCws {t : ℕ} {ht : 1 ≤ t} (j d : ℕ) (S : LIDT.CL.Ty) {k : ℕ} (coef : ℕ → ℕ → Fq t ht) {c e : ℕ} (hc : c < k) (he : e < ncoef j d S) : cw t ht j d S (encCws t ht k (ncoef j d S) coef) c e = coef c e

cw reads the codewords back.

Honest low-degree answers

noncomputable def MIPRE.Tailored.AnsRed.Typed.honestCoef {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {k : ℕ} (G : Fin k → MvPolynomial (Fin (2 ^ j)) (Fq t ht)) : LIDT.CL.Question (Fq t ht) (2 ^ j) → ℕ → ℕ → Fq t ht

The coefficients of the honest answer of a tuple of polynomials to a question: the values at a point, the coefficients of the restrictions to a line.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.AnsRed.Typed.honestCoef hM G (MIPRE.LIDT.CL.Question.point u) x✝¹ x✝ = if hc : x✝¹ < k then (MvPolynomial.eval u) (G ⟨x✝¹, hc⟩) else 0
• MIPRE.Tailored.AnsRed.Typed.honestCoef hM G (MIPRE.LIDT.CL.Question.dline u₀ s v) x✝¹ x✝ = if hc : x✝¹ < k then (MIPRE.LowDegree.lineRestrict u₀ v (G ⟨x✝¹, hc⟩)).coeff x✝ else 0

noncomputable def MIPRE.Tailored.AnsRed.Typed.honestBits {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (S : LIDT.CL.Ty) {k : ℕ} (G : Fin k → MvPolynomial (Fin (2 ^ j)) (Fq t ht)) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) : Cost.BitStr

The honest answer of a tuple of polynomials to a question of the low-degree type S, as a bit string.

Equations

• MIPRE.Tailored.AnsRed.Typed.honestBits d hM S G q = MIPRE.Tailored.AnsRed.Typed.encCws t ht k (MIPRE.Tailored.AnsRed.Typed.ncoef j d S) (MIPRE.Tailored.AnsRed.Typed.honestCoef hM G q)

theorem MIPRE.Tailored.AnsRed.Typed.length_honestBits {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (S : LIDT.CL.Ty) {k : ℕ} (G : Fin k → MvPolynomial (Fin (2 ^ j)) (Fq t ht)) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) : List.length (honestBits d hM S G q) = k * ncoef j d S * t

theorem MIPRE.Tailored.AnsRed.Typed.honestCoef_congr {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {k k' : ℕ} {G : Fin k → MvPolynomial (Fin (2 ^ j)) (Fq t ht)} {G' : Fin k' → MvPolynomial (Fin (2 ^ j)) (Fq t ht)} {c c' : ℕ} (hc : c < k) (hc' : c' < k') (h : G ⟨c, hc⟩ = G' ⟨c', hc'⟩) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) (e : ℕ) : honestCoef hM G q c e = honestCoef hM G' q c' e

theorem MIPRE.Tailored.AnsRed.Typed.decAns_honestBits {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (r : Role) (G : Fin (slotsOf L r).length → MvPolynomial (Fin (2 ^ j)) (Fq t ht)) (S : LIDT.CL.Ty) (x : Fin (D j) → Fq t ht) : decAns t ht j d L r S (honestBits d hM S G ((regs j).questionOf sel S x)) = LIDT.CL.honest hM G ((regs j).questionOf sel S x)

decAns reads the honest answer back at a question the presentation computes.

theorem MIPRE.Tailored.AnsRed.Typed.sampleOf_question_ty {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (S S' τ : LIDT.CL.Ty) (x : Fin (D j) → Fq t ht) : LIDT.CL.Sample.question hM ((regs j).sampleOf sel S x) τ = LIDT.CL.Sample.question hM ((regs j).sampleOf sel S' x) τ

theorem MIPRE.Tailored.AnsRed.Typed.accepts_honestBits {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (r : Role) (G : Fin (slotsOf L r).length → MvPolynomial (Fin (2 ^ j)) (Fq t ht)) (hG : ∀ (c : Fin (slotsOf L r).length) (i : Fin (2 ^ j)), MvPolynomial.degreeOf i (G c) ≤ d) (S₁ S₂ : LIDT.CL.Ty) (x : Fin (D j) → Fq t ht) : LIDT.CL.accepts hM ((regs j).questionOf sel S₁ (((regs j).pres sel S₁).eval x)) ((regs j).questionOf sel S₂ (((regs j).pres sel S₂).eval x)) (decAns t ht j d L r S₁ (honestBits d hM S₁ G ((regs j).questionOf sel S₁ (((regs j).pres sel S₁).eval x)))) (decAns t ht j d L r S₂ (honestBits d hM S₂ G ((regs j).questionOf sel S₂ (((regs j).pres sel S₂).eval x)))) = true

The low-degree check accepts honest answers of one tuple of polynomials of individual degree at most d, at two questions of one sample.

A role's codewords of a PCP

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldPolys {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (L : PcpDims) (hLM : L.m ≤ 2 ^ j) (P : Pcp L (Fq t ht)) (r : Role) : Fin (slotsOf L r).length → MvPolynomial (Fin (2 ^ j)) (Fq t ht)

A role's codewords of a PCP, on the low-degree test's variables.

Equations

• MIPRE.Tailored.AnsRed.Typed.ldPolys L hLM P r c = (MvPolynomial.rename (Fin.castLE hLM)) (P.slotPoly ((MIPRE.Tailored.AnsRed.slotsOf L r).get c))

theorem MIPRE.Tailored.AnsRed.Typed.ldPolys_eq {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {L : PcpDims} (hLM : L.m ≤ 2 ^ j) (P : Pcp L (Fq t ht)) (r : Role) (c : Fin (slotsOf L r).length) : ldPolys L hLM P r c = (MvPolynomial.rename (Fin.castLE hLM ∘ ((slotsOf L r).get c).emb)) (P.slot ((slotsOf L r).get c))

theorem MIPRE.Tailored.AnsRed.Typed.degreeOf_ldPolys {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) {L : PcpDims} (hLM : L.m ≤ 2 ^ j) {P : Pcp L (Fq t ht)} {d' : ℕ} (hP : P.IndDeg d') (hd : d' ≤ d) (r : Role) (c : Fin (slotsOf L r).length) (i : Fin (2 ^ j)) : MvPolynomial.degreeOf i (ldPolys L hLM P r c) ≤ d

theorem MIPRE.Tailored.AnsRed.Typed.degreeOf_rename_eq_zero {t : ℕ} {ht : 1 ≤ t} {k N : ℕ} {f : Fin k → Fin N} (hf : Function.Injective f) (p : MvPolynomial (Fin k) (Fq t ht)) {i : Fin N} (hi : ∀ (a : Fin k), f a ≠ i) : MvPolynomial.degreeOf i ((MvPolynomial.rename f) p) = 0

theorem MIPRE.Tailored.AnsRed.Typed.indOK_honestBits {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (hLM : L.m ≤ 2 ^ j) (r : Role) (P : Pcp L (Fq t ht)) (S : LIDT.CL.Ty) (x : Fin (D j) → Fq t ht) : IndOK t ht j d L hM hLM r (honestBits d hM S (ldPolys L hLM P r) ((regs j).questionOf sel S x)) ((regs j).questionOf sel S x)

Indifference holds of honest answers: a codeword whose block misses the direction of an axis-parallel line does not involve that variable, so it is constant along the line.

theorem MIPRE.Tailored.AnsRed.Typed.isoAgrees_honestBits {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (hLM : L.m ≤ 2 ^ j) (r : Role) (P Q : Pcp L (Fq t ht)) (hPQ : ∀ s ∈ slotsOf L r, P.slot s = Q.slot s) (S : LIDT.CL.Ty) (q : LIDT.CL.Question (Fq t ht) (2 ^ j)) : IsoAgrees t ht j d L r S (honestBits d hM S (ldPolys L hLM P r) q) (honestBits d hM S (ldPolys L hLM Q Role.oracle) q)

Consistency holds of honest answers: an isolated role's codewords of a PCP agreeing with another in the role's slots are that PCP's oracle codewords in those slots.

theorem MIPRE.Tailored.AnsRed.Typed.passesV_honestBits {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) {L : PcpDims} (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (hLM : L.m ≤ 2 ^ j) (P : Pcp L (Fq t ht)) (T : MvPolynomial (Fin L.m) (Fq t ht)) (hP : Pcp.Identities T P) (x : Fin (D j) → Fq t ht) : PassesV T (vals t ht j d L (honestBits d hM LIDT.CL.Ty.point (ldPolys L hLM P Role.oracle) ((regs j).questionOf sel LIDT.CL.Ty.point x))) (ptm L hLM ((regs j).questionOf sel LIDT.CL.Ty.point x).base)

The proof check holds of the oracle's honest point answer for a PCP satisfying the identities: its values are the PCP's values at the point.

The honest answers at typed questions

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.qA {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (z : V.Questions n) : V.Questions n

Alice's question map of the input sampler at index n.

Equations

• MIPRE.Tailored.AnsRed.Typed.qA V n z = (V.sampler.cl n MIPRE.Player.alice).eval z

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.qB {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) (z : V.Questions n) : V.Questions n

Bob's question map of the input sampler at index n.

Equations

• MIPRE.Tailored.AnsRed.Typed.qB V n z = (V.sampler.cl n MIPRE.Player.bob).eval z

noncomputable def MIPRE.Tailored.AnsRed.Typed.inSeeded {ℓV : ℕ} (V : TailoredVerifier ℓV) (n : ℕ) : SeededGame (V.Questions n) (Verifier.Answers (V.tgame n).maxLen)

The input's n-th game as a seeded game, the oracularization's input.

Equations

• MIPRE.Tailored.AnsRed.Typed.inSeeded V n = { LA := MIPRE.Tailored.AnsRed.Typed.qA V n, LB := MIPRE.Tailored.AnsRed.Typed.qB V n, D := (V.tgame n).toGame.D }

noncomputable def MIPRE.Tailored.AnsRed.Typed.rolePcp (t : ℕ) (ht : 1 ≤ t) (L : PcpDims) {ℓ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 : ℕ} : Role → OAns (Verifier.Answers B) → V.Questions n → Pcp L (Fq t ht)

The honest PCP a role answers from, at its question, for an answer of the oracularized game: the oracle's of the pair at the questions of the seed, an isolated player's of its own answer paired with itself (whose polynomials in the player's slots are the oracle's, by slot_pairPcp_alice and slot_pairPcp_bob).

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Tailored.AnsRed.Typed.rolePcp t ht L V n Cc hm MIPRE.Role.bob (MIPRE.OAns.single b) x✝ = MIPRE.Tailored.AnsRed.pairPcp L V n (MIPRE.Tailored.AnsRed.circOf L V n Cc hm x✝) (Cc x✝) x✝ x✝ ↑b ↑b
• MIPRE.Tailored.AnsRed.Typed.rolePcp t ht L V n Cc hm x✝² x✝¹ x✝ = MIPRE.Tailored.AnsRed.pairPcp L V n (MIPRE.Tailored.AnsRed.circOf L V n Cc hm x✝) (Cc x✝) x✝ x✝ [] []

theorem MIPRE.Tailored.AnsRed.Typed.indDeg_rolePcp {t : ℕ} {ht : 1 ≤ t} (L : PcpDims) {ℓ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 : ℕ} (r : Role) (o : OAns (Verifier.Answers B)) (z : V.Questions n) : (rolePcp t ht L V n Cc hm r o z).IndDeg 17

noncomputable def MIPRE.Tailored.AnsRed.Typed.honestAns {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (L : PcpDims) (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (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 : CL.Detyping.Question (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D j * t))) (o : OAns (Verifier.Answers B)) : Cost.BitStr

The honest answer at a typed question to an answer of the oracularized game: the honest low-degree answers of the role's codewords of its PCP, at the question's low-degree question.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.length_honestAns {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (L : PcpDims) (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (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 : CL.Detyping.Question (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D j * t))) (o : OAns (Verifier.Answers B)) : List.length (honestAns d hM L sel hLM V n Cc hm u o) = len t j d L u.1

theorem MIPRE.Tailored.AnsRed.Typed.arPred_honest {t : ℕ} {ht : 1 ≤ t} {j : ℕ} (d : ℕ) (hM : 2 ^ j ∣ Fintype.card (Fq t ht)) (L : PcpDims) (sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (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) {prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)} {Tt : ℕ} (H : HonestHyp L V n prm Cc Tt) (hd : 17 ≤ d) (s : Fin (V.sampler.dim n + D j * t) → CL.𝔽₂) (u v : CL.Detyping.Question (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D j * t))) (hu : rolePart t j (V.sampler.dim n) u.2 = ((inSeeded V n).oquestion u.1.1 (CL.leftPart s)).2) (hv : rolePart t j (V.sampler.dim n) v.2 = ((inSeeded V n).oquestion v.1.1 (CL.leftPart s)).2) (hu' : ldPart t ht j (V.sampler.dim n) u.2 = ((regs j).pres sel u.1.2).eval (ldPart t ht j (V.sampler.dim n) s)) (hv' : ldPart t ht j (V.sampler.dim n) v.2 = ((regs j).pres sel v.1.2).eval (ldPart t ht j (V.sampler.dim n) s)) (o₁ o₂ : OAns (Verifier.Answers (V.tgame n).maxLen)) (hacc : (inSeeded V n).oaccepts ((inSeeded V n).oquestion u.1.1 (CL.leftPart s)) ((inSeeded V n).oquestion v.1.1 (CL.leftPart s)) o₁ o₂ = true) : ArPred t ht j d L (V.sampler.dim n) sel hLM (circOf L V n Cc hm) u v (honestAns d hM L sel hLM V n Cc hm u o₁) (honestAns d hM L sel hLM V n Cc hm v o₂)

The functional half of completeness: at two typed questions read off one seed — the oracularized input question of the seed's input part in each role, and the low-degree questions of the seed's low-degree part — answers the oracularized predicate accepts give honest answers the answer-reduced predicate accepts, when the honest PCPs of accepted answers satisfy the checks (HonestHyp) and the degree d is at least 17.