Honest answers in the seeded CL low-degree test

Piece AR-4 of planning/answer-reduction.md needs the completeness of the seeded CL test (def:lidt-cl, MIPRE.LIDT.CL.accepts): a tuple of polynomials of individual degree at most d, answered honestly — its values at a point, its restrictions to a line — passes the test on any two questions of one sample.

• honest — the honest answer of a tuple G of ldc polynomials to a question: the values at a point, the coefficients of the restrictions (MIPRE.LowDegree.lineRestrict) to an axis-parallel or diagonal line.
• accepts_honest — the test accepts the honest answers to the two questions of a sample.
• Regs.sampleOf_eval_question — reading a sample back off the presentation's output gives the question the presentation computes: the base points it outputs are already canonical, so the decider's re-derivation of the base point (rep) changes nothing. This is what lets a decider that reads the sample off a question vector be fed the presentation's questions.

The canonical base point

theorem MIPRE.LIDT.CL.canonLin_canonLin {F : Type u_1} [Field F] {m : ℕ} (S : Submodule F (Fin m → F)) (x : Fin m → F) : (CL.canonLin S) ((CL.canonLin S) x) = (CL.canonLin S) x

theorem MIPRE.LIDT.CL.rep_rep {F : Type u_1} [Field F] {m : ℕ} (w u : Point F m) : rep w (rep w u) = rep w u

theorem MIPRE.LIDT.CL.exists_eq_rep_add {F : Type u_1} [Field F] {m : ℕ} (w u : Point F m) : ∃ (t : F), u = rep w u + t • w

A point lies on the line through its canonical base point.

theorem MIPRE.LIDT.CL.zeroBelow_zeroBelow {F : Type u_1} [Field F] {m : ℕ} (i : Fin m) (v : Point F m) : zeroBelow i (zeroBelow i v) = zeroBelow i v

theorem MIPRE.LIDT.CL.add_lineParam_smul {F : Type u_1} [Field F] {m : ℕ} [DecidableEq F] (u₀ w : Point F m) (t : F) : u₀ + lineParam u₀ w (u₀ + t • w) • w = u₀ + t • w

The parameter of a point of a line is its parameter, when the line is not a point.

Line polynomials

noncomputable def MIPRE.LIDT.CL.lineCo {F : Type u_1} [Field F] {m : ℕ} (n : ℕ) (u₀ w : Point F m) (p : MvPolynomial (Fin m) F) : LinePoly F n

The coefficients of the restriction of p to the line u₀ + t w, as a LinePoly of degree n.

Equations

• MIPRE.LIDT.CL.lineCo n u₀ w p i = (MIPRE.LowDegree.lineRestrict u₀ w p).coeff ↑i

theorem MIPRE.LIDT.CL.eval_lineCo {F : Type u_1} [Field F] {m n : ℕ} {u₀ w : Point F m} {p : MvPolynomial (Fin m) F} (h : (LowDegree.lineRestrict u₀ w p).natDegree ≤ n) (t : F) : (lineCo n u₀ w p).eval t = (MvPolynomial.eval (u₀ + t • w)) p

theorem MIPRE.LIDT.CL.totalDegree_le_of_degreeOf_le {F : Type u_1} [Field F] {m d : ℕ} {p : MvPolynomial (Fin m) F} (h : ∀ (i : Fin m), MvPolynomial.degreeOf i p ≤ d) : p.totalDegree ≤ m * d

Individual degree at most d in each of m variables is total degree at most m d.

Honest answers

noncomputable def MIPRE.LIDT.CL.honest {F : Type u_1} [Field F] {m : ℕ} [Fintype F] [NeZero m] (hm : m ∣ Fintype.card F) {d ldc : ℕ} (G : Fin ldc → MvPolynomial (Fin m) F) : Question F m → Answer F m d ldc

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

Equations

• MIPRE.LIDT.CL.honest hm G (MIPRE.LIDT.CL.Question.point u) = MIPRE.LIDT.CL.Answer.values fun (j : Fin ldc) => (MvPolynomial.eval u) (G j)
• MIPRE.LIDT.CL.honest hm G (MIPRE.LIDT.CL.Question.aline u₀ s) = MIPRE.LIDT.CL.Answer.apolys fun (j : Fin ldc) => MIPRE.LIDT.CL.lineCo d u₀ (Pi.single (MIPRE.LIDT.CL.chi hm s) 1) (G j)
• MIPRE.LIDT.CL.honest hm G (MIPRE.LIDT.CL.Question.dline u₀ s v) = MIPRE.LIDT.CL.Answer.dpolys fun (j : Fin ldc) => MIPRE.LIDT.CL.lineCo (m * d) u₀ v (G j)

theorem MIPRE.LIDT.CL.fmtOk_honest {F : Type u_1} [Field F] {m : ℕ} [Fintype F] [NeZero m] (hm : m ∣ Fintype.card F) {d ldc : ℕ} (G : Fin ldc → MvPolynomial (Fin m) F) (q : Question F m) : q.fmtOk (honest hm G q) = true

theorem MIPRE.LIDT.CL.lineVsPoint_honest {F : Type u_1} [Field F] {m : ℕ} [Fintype F] [DecidableEq F] {ldc n : ℕ} {G : Fin ldc → MvPolynomial (Fin m) F} {u₀ w x : Point F m} (hx : ∃ (t : F), x = u₀ + t • w) (hG : ∀ (j : Fin ldc), (LowDegree.lineRestrict u₀ w (G j)).natDegree ≤ n) : (lineVsPoint u₀ w x (fun (j : Fin ldc) => lineCo n u₀ w (G j)) fun (j : Fin ldc) => (MvPolynomial.eval x) (G j)) = true

A line answer against a point on the line: the honest answers agree.

theorem MIPRE.LIDT.CL.accepts_honest {F : Type u_1} [Field F] {m : ℕ} [Fintype F] [DecidableEq F] [NeZero m] {hm : m ∣ Fintype.card F} {d ldc : ℕ} {G : Fin ldc → MvPolynomial (Fin m) F} (hG : ∀ (j : Fin ldc) (i : Fin m), MvPolynomial.degreeOf i (G j) ≤ d) (sm : Sample F m) (τ τ' : Ty) : accepts hm (Sample.question hm sm τ) (Sample.question hm sm τ') (honest hm G (Sample.question hm sm τ)) (honest hm G (Sample.question hm sm τ')) = true

The seeded CL test accepts honest answers to the two questions of a sample, for any tuple of polynomials of individual degree at most d.

Reading the sample back

noncomputable def MIPRE.LIDT.CL.recanon {F : Type u_1} [Field F] {m : ℕ} [Fintype F] [NeZero m] {hm : m ∣ Fintype.card F} (q : Question F m) : Question F m

The decider's re-derivation of a question from the sample it reads: the base point made canonical, the diagonal direction zeroed below the seed's block.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LIDT.CL.recanon (MIPRE.LIDT.CL.Question.point u) = MIPRE.LIDT.CL.Question.point u
• MIPRE.LIDT.CL.recanon (MIPRE.LIDT.CL.Question.aline u₀ s) = MIPRE.LIDT.CL.Question.aline (MIPRE.LIDT.CL.rep (Pi.single (MIPRE.LIDT.CL.chi hm s) 1) u₀) s

theorem MIPRE.LIDT.CL.recanon_question {F : Type u_1} [Field F] {m : ℕ} [Fintype F] [NeZero m] {hm : m ∣ Fintype.card F} (sm : Sample F m) (τ : Ty) : recanon (Sample.question hm sm τ) = Sample.question hm sm τ

The sample's own questions are already canonical.

theorem MIPRE.LIDT.CL.Regs.sampleOf_question {F : Type u_1} [Field F] {m : ℕ} [Fintype F] [DecidableEq F] [NeZero m] {hm : m ∣ Fintype.card F} {ι : Type u_2} (R : Regs ι m) (S : Sel F m hm) (τ : Ty) (y : ι → F) : Sample.question hm (R.sampleOf S τ y) τ = recanon (R.questionOf S τ y)

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

Reading the sample back off the presentation's output gives the question it computes.