The presentation's output is a function of its question

Piece AR-5b of planning/answer-reduction.md needs the converse of Regs.questionOf_eval: the vector a type's presentation outputs is supported on the copy's own registers, and is a fixed function (Regs.embedQ) of the seeded question it computes (Regs.pres_eval). So a strategy that answers a question vector of the answer-reduced verifier answers, through embedQ, the seeded low-degree test's question, and the two games' questions correspond one to one.

def MIPRE.LIDT.CL.Question.ty {F : Type u_1} {n : ℕ} : Question F n → Ty

The type of a question.

Equations

• (MIPRE.LIDT.CL.Question.point u).ty = MIPRE.LIDT.CL.Ty.point
• (MIPRE.LIDT.CL.Question.aline u₀ s).ty = MIPRE.LIDT.CL.Ty.aline
• (MIPRE.LIDT.CL.Question.dline u₀ s v).ty = MIPRE.LIDT.CL.Ty.dline

@[simp]

theorem MIPRE.LIDT.CL.Sample.question_ty {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} [NeZero n] (hn : n ∣ Fintype.card F) (sm : Sample F n) (t : Ty) : (question hn sm t).ty = t

noncomputable def MIPRE.LIDT.CL.Regs.embedQ {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) : Question F n → ι → F

The vector a question is presented as: the point written in the point register, the seed decoded by the permutation in the seed register, the direction in the direction register.

Equations

• R.embedQ S (MIPRE.LIDT.CL.Question.point u) = R.putPt u
• R.embedQ S (MIPRE.LIDT.CL.Question.aline u₀ s) = Pi.single R.coord (S.π.symm s) + R.putPt u₀
• R.embedQ S (MIPRE.LIDT.CL.Question.dline u₀ s v) = Pi.single R.coord (S.π.symm s) + R.putDir v + R.putPt u₀

theorem MIPRE.LIDT.CL.Regs.proj_coordSet {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (x : ι → F) : (CL.proj R.coordSet) x = Pi.single R.coord (x R.coord)

theorem MIPRE.LIDT.CL.Regs.pres_eval {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (x : ι → F) : (R.pres S t).eval x = R.embedQ S (Sample.question hn (R.sampleOf S t x) t)

The presentation's output is the embedding of the question it computes.

theorem MIPRE.LIDT.CL.Regs.ptOf_add {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (x y : ι → F) : R.ptOf (x + y) = R.ptOf x + R.ptOf y

theorem MIPRE.LIDT.CL.Regs.dirOf_add {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (x y : ι → F) : R.dirOf (x + y) = R.dirOf x + R.dirOf y

theorem MIPRE.LIDT.CL.Regs.ptOf_single_coord {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (c : F) : R.ptOf (Pi.single R.coord c) = 0

theorem MIPRE.LIDT.CL.Regs.dirOf_single_coord {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (c : F) : R.dirOf (Pi.single R.coord c) = 0

theorem MIPRE.LIDT.CL.Regs.questionOf_embedQ {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (q : Question F n) : R.questionOf S q.ty (R.embedQ S q) = q

Reading a presented question back gives the question.

theorem MIPRE.LIDT.CL.Regs.sampleOf_embedQ {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (sm : Sample F n) (t : Ty) : Sample.question hn (R.sampleOf S t (R.embedQ S (Sample.question hn sm t))) t = Sample.question hn sm t

The sample read off a presented sample question gives the question back.

Two types on one sample

def MIPRE.LIDT.CL.Sample.retype {F : Type u_1} {n : ℕ} (sm : Sample F n) (a b : Ty) : Sample F n

A sample with its two types replaced.

Equations

• sm.retype a b = { tyA := a, tyB := b, u := sm.u, s := sm.s, v := sm.v }

@[simp]

theorem MIPRE.LIDT.CL.Sample.question_retype {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} [NeZero n] (hn : n ∣ Fintype.card F) (sm : Sample F n) (a b t : Ty) : question hn (sm.retype a b) t = question hn sm t

A question depends on the sample's point, seed and direction, not on its types.

def MIPRE.LIDT.CL.Sample.equiv (F : Type u_1) (n : ℕ) : Sample F n ≃ Ty × Ty × Point F n × F × Point F n

A sample is its two types, point, seed and direction.

Equations

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

theorem MIPRE.LIDT.CL.Regs.sum_sampleOf_retype {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) {M : Type u_3} [AddCommMonoid M] (g : Sample F n → M) : ∑ a : Ty, ∑ b : Ty, ∑ x : ι → F, g ((R.sampleOf S a x).retype a b) = Fintype.card F ^ (Fintype.card ι - (2 * n + 1)) • ∑ sm : Sample F n, g sm

Uniform content and a uniform pair of types give a uniform sample: the sample the registers carry at the first type, retyped to a pair of types, summed over both types and all vectors, is every sample q^{|ι| - (2n+1)} times.