The seeded low-degree questions as CL functions, on any registers

The paper's typed CL functions L_Point, L_ALine, L_DLine (ldt.tex, eq:cl-ptf to eq:cl-dlnf) act on three registers of an ambient space: a point register V_pt ≅ F^n, a coordinate (seed) register V_coord ≅ F and a direction register V_dir ≅ F^n. The answer-reduced sampler (sec:ar-verifier) uses six copies of them on overlapping registers of one ambient space, so the registers are data here: Regs ι n places them in the coordinates ι of the ambient space by two injections and a coordinate.

Every type gets a three-level presentation (pres), the levels being the seed, then the direction, then everything else; the paper's one- and two-level functions are the same with trivial levels, as in QLD.PauliCL.presentation. The presentations are exact on the whole space (pres_exactlyOn), and their full evaluation, read back through the registers (questionOf), is the seeded test's question LIDT.CL.Sample.question for the sample the registers carry (questionOf_eval).

theorem MIPRE.CL.sum_comp_injective {κ : Type u_1} {ι : Type u_2} {F : Type u_3} {M : Type u_4} [Fintype κ] [DecidableEq κ] [Fintype ι] [DecidableEq ι] [Fintype F] [DecidableEq F] [AddCommMonoid M] (e : κ → ι) (he : Function.Injective e) (g : (κ → F) → M) : ∑ x : ι → F, g (x ∘ e) = Fintype.card F ^ (Fintype.card ι - Fintype.card κ) • ∑ y : κ → F, g y

Summing over vectors through an injection of coordinates: x ↦ x ∘ e has fibres of size q^{|ι| - |κ|}.

structure MIPRE.LIDT.CL.Regs (ι : Type u_1) (n : ℕ) : Type u_1

The three registers of a copy of the low-degree test in an ambient space with coordinates ι: the point and direction registers, each n coordinates, and the seed coordinate.

• pt : Fin n → ι

  The point register.

• dir : Fin n → ι

  The direction register.

• coord : ι

  The coordinate (seed) register.

• pt_injective : Function.Injective self.pt
• dir_injective : Function.Injective self.dir
• pt_ne_dir (i j : Fin n) : self.pt i ≠ self.dir j
• pt_ne_coord (i : Fin n) : self.pt i ≠ self.coord
• dir_ne_coord (j : Fin n) : self.dir j ≠ self.coord

structure MIPRE.LIDT.CL.Sel (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] (n : ℕ) [NeZero n] (hn : n ∣ Fintype.card F) : Type u_1

A seed selector: the block index χ(s) a sampler computes from a seed, with a permutation π of the seeds under which it is the test's own chi. The test's chi numbers the field by Fintype.equivFin, which no program can compute; an effective sampler uses an explicit selector with the same block sizes, and the permutation, which only the analysis sees, carries its questions to the test's (questionOf_eval). Sel.canonical is the test's own selector.

• χ : F → Fin n

  The selector.

• π : F ≃ F

  The permutation of the seeds.

• chi_π (s : F) : chi hn (self.π s) = self.χ s

noncomputable def MIPRE.LIDT.CL.Sel.canonical {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} [NeZero n] (hn : n ∣ Fintype.card F) : Sel F n hn

The test's own selector.

Equations

• MIPRE.LIDT.CL.Sel.canonical hn = { χ := MIPRE.LIDT.CL.chi hn, π := Equiv.refl F, chi_π := ⋯ }

theorem MIPRE.LIDT.CL.Sel.exists_perm {F : Type u_1} [Field F] [Fintype F] {n : ℕ} [NeZero n] (hn : n ∣ Fintype.card F) (χ : F → Fin n) (hχ : ∀ (i : Fin n), {s : F | χ s = i}.card = Fintype.card F / n) : ∃ (π : F ≃ F), ∀ (s : F), chi hn (π s) = χ s

Any selector with blocks of size q / n is a seed selector: the permutation matching it to the test's chi exists.

noncomputable def MIPRE.LIDT.CL.Sel.ofSelector {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} [NeZero n] (hn : n ∣ Fintype.card F) (χ : F → Fin n) (hχ : ∀ (i : Fin n), {s : F | χ s = i}.card = Fintype.card F / n) : Sel F n hn

The seed selector of a selector with blocks of size q / n.

Equations

• MIPRE.LIDT.CL.Sel.ofSelector hn χ hχ = { χ := χ, π := ⋯.choose, chi_π := ⋯ }

Reading and writing registers

def MIPRE.LIDT.CL.Regs.ptOf {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} (x : ι → F) : Point F n

The point a vector carries.

Equations

• R.ptOf x i = x (R.pt i)

def MIPRE.LIDT.CL.Regs.dirOf {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} (x : ι → F) : Point F n

The direction a vector carries.

Equations

• R.dirOf x i = x (R.dir i)

noncomputable def MIPRE.LIDT.CL.Regs.putPt {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] : Point F n →ₗ[F] ι → F

Write a point into the point register, zero elsewhere.

Equations

• R.putPt = Function.ExtendByZero.linearMap F R.pt

noncomputable def MIPRE.LIDT.CL.Regs.putDir {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] : Point F n →ₗ[F] ι → F

Write a direction into the direction register, zero elsewhere.

Equations

• R.putDir = Function.ExtendByZero.linearMap F R.dir

@[simp]

theorem MIPRE.LIDT.CL.Regs.putPt_pt {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (w : Point F n) (i : Fin n) : R.putPt w (R.pt i) = w i

@[simp]

theorem MIPRE.LIDT.CL.Regs.putDir_dir {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (w : Point F n) (i : Fin n) : R.putDir w (R.dir i) = w i

theorem MIPRE.LIDT.CL.Regs.putPt_of_not {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] {c : ι} (h : ∀ (i : Fin n), R.pt i ≠ c) (w : Point F n) : R.putPt w c = 0

theorem MIPRE.LIDT.CL.Regs.putDir_of_not {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] {c : ι} (h : ∀ (i : Fin n), R.dir i ≠ c) (w : Point F n) : R.putDir w c = 0

@[simp]

theorem MIPRE.LIDT.CL.Regs.ptOf_putPt {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (w : Point F n) : R.ptOf (R.putPt w) = w

@[simp]

theorem MIPRE.LIDT.CL.Regs.dirOf_putDir {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (w : Point F n) : R.dirOf (R.putDir w) = w

@[simp]

theorem MIPRE.LIDT.CL.Regs.dirOf_putPt {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (w : Point F n) : R.dirOf (R.putPt w) = 0

@[simp]

theorem MIPRE.LIDT.CL.Regs.ptOf_putDir {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (w : Point F n) : R.ptOf (R.putDir w) = 0

@[simp]

theorem MIPRE.LIDT.CL.Regs.putPt_coord {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (w : Point F n) : R.putPt w R.coord = 0

@[simp]

theorem MIPRE.LIDT.CL.Regs.putDir_coord {ι : Type u_1} {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (w : Point F n) : R.putDir w R.coord = 0

The register sets

def MIPRE.LIDT.CL.Regs.coordSet {ι : Type u_1} {n : ℕ} (R : Regs ι n) : Finset ι

The seed register.

Equations

• R.coordSet = {R.coord}

def MIPRE.LIDT.CL.Regs.dirSet {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) : Finset ι

The direction register.

Equations

• R.dirSet = Finset.image R.dir Finset.univ

def MIPRE.LIDT.CL.Regs.finalSet {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) : Finset ι

Everything else: the point register and the coordinates no copy of the test reads.

Equations

• R.finalSet = (Finset.univ \ R.coordSet) \ R.dirSet

theorem MIPRE.LIDT.CL.Regs.dirSet_subset {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) : R.dirSet ⊆ Finset.univ \ R.coordSet

theorem MIPRE.LIDT.CL.Regs.pt_mem_finalSet {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) (i : Fin n) : R.pt i ∈ R.finalSet

theorem MIPRE.LIDT.CL.Regs.dir_mem_dirSet {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) (j : Fin n) : R.dir j ∈ R.dirSet

theorem MIPRE.LIDT.CL.Regs.proj_finalSet_putPt {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (w : Point F n) : (CL.proj R.finalSet) (R.putPt w) = R.putPt w

theorem MIPRE.LIDT.CL.Regs.proj_dirSet_putDir {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (w : Point F n) : (CL.proj R.dirSet) (R.putDir w) = R.putDir w

theorem MIPRE.LIDT.CL.Regs.ptOf_proj_finalSet {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (x : ι → F) : R.ptOf ((CL.proj R.finalSet) x) = R.ptOf x

theorem MIPRE.LIDT.CL.Regs.dirOf_proj_dirSet {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (x : ι → F) : R.dirOf ((CL.proj R.dirSet) x) = R.dirOf x

The stage maps

def MIPRE.LIDT.CL.Regs.zeroBelowLin {n : ℕ} {F : Type u_2} [Field F] (i : Fin n) : Point F n →ₗ[F] Point F n

π_i, zeroing the first i coordinates, as a linear map.

Equations

• MIPRE.LIDT.CL.Regs.zeroBelowLin i = { toFun := MIPRE.LIDT.CL.zeroBelow i, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def MIPRE.LIDT.CL.Regs.ptLin {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (A : Point F n →ₗ[F] Point F n) : CL.RegLinear F R.finalSet

A linear map of the point register, as a map on the final register.

Equations

• R.ptLin A = MIPRE.CL.RegLinear.ofLinearMap R.finalSet (R.putPt ∘ₗ A ∘ₗ LinearMap.funLeft F F R.pt)

theorem MIPRE.LIDT.CL.Regs.ptLin_apply {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (A : Point F n →ₗ[F] Point F n) (x : ι → F) : (R.ptLin A) x = R.putPt (A (R.ptOf x))

noncomputable def MIPRE.LIDT.CL.Regs.dirLin {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (i : Fin n) : CL.RegLinear F R.dirSet

π_i of the direction register.

Equations

• R.dirLin i = MIPRE.CL.RegLinear.ofLinearMap R.dirSet (R.putDir ∘ₗ MIPRE.LIDT.CL.Regs.zeroBelowLin i ∘ₗ LinearMap.funLeft F F R.dir)

theorem MIPRE.LIDT.CL.Regs.dirLin_apply {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (i : Fin n) (x : ι → F) : (R.dirLin i) x = R.putDir (zeroBelow i (R.dirOf x))

def MIPRE.LIDT.CL.Regs.seedLin {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] : Ty → CL.RegLinear F R.coordSet

The first stage: the seed, for the two line types.

Equations

• R.seedLin MIPRE.LIDT.CL.Ty.point = 0
• R.seedLin x✝ = MIPRE.CL.RegLinear.id R.coordSet

noncomputable def MIPRE.LIDT.CL.Regs.secondLin {ι : 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) : Ty → F → CL.RegLinear F R.dirSet

The second stage: π_{χ(s)} of the direction, for the diagonal type.

Equations

• R.secondLin S MIPRE.LIDT.CL.Ty.dline x✝ = R.dirLin (S.χ x✝)
• R.secondLin S x✝¹ x✝ = 0

noncomputable def MIPRE.LIDT.CL.Regs.finalLin {ι : 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) : Ty → F → Point F n → CL.RegLinear F R.finalSet

The third stage: the canonical base point of the line through the point.

Equations

• R.finalLin S MIPRE.LIDT.CL.Ty.point x✝¹ x✝ = R.ptLin LinearMap.id
• R.finalLin S MIPRE.LIDT.CL.Ty.aline x✝¹ x✝ = R.ptLin (MIPRE.CL.canonLin (F ∙ Pi.single (S.χ x✝¹) 1))
• R.finalLin S MIPRE.LIDT.CL.Ty.dline x✝¹ x✝ = R.ptLin (MIPRE.CL.canonLin (F ∙ x✝))

noncomputable def MIPRE.LIDT.CL.Regs.pres {ι : 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) : CL.CLFun F ι 3

The three-level presentation of the question of type t: seed, then direction, then the point register and everything else.

Equations

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

theorem MIPRE.LIDT.CL.Regs.pres_exactlyOn {ι : 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) : (R.pres S t).ExactlyOn Finset.univ

def MIPRE.LIDT.CL.Regs.questionOf {ι : Type u_1} {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) : Question F n

Read the question of type t off a vector, the seed decoded by the selector's permutation.

Equations

• R.questionOf S MIPRE.LIDT.CL.Ty.point x = MIPRE.LIDT.CL.Question.point (R.ptOf x)
• R.questionOf S MIPRE.LIDT.CL.Ty.aline x = MIPRE.LIDT.CL.Question.aline (R.ptOf x) (S.π (x R.coord))
• R.questionOf S MIPRE.LIDT.CL.Ty.dline x = MIPRE.LIDT.CL.Question.dline (R.ptOf x) (S.π (x R.coord)) (R.dirOf x)

def MIPRE.LIDT.CL.Regs.sampleOf {ι : Type u_1} {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) : Sample F n

The sample a vector carries, with both types t, the seed decoded by the selector's permutation.

Equations

• R.sampleOf S t x = { tyA := t, tyB := t, u := R.ptOf x, s := S.π (x R.coord), v := R.dirOf x }

theorem MIPRE.LIDT.CL.Regs.not_mem_coordSet_pt {ι : Type u_1} {n : ℕ} (R : Regs ι n) (i : Fin n) : R.pt i ∉ R.coordSet

theorem MIPRE.LIDT.CL.Regs.not_mem_dirSet_pt {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) (i : Fin n) : R.pt i ∉ R.dirSet

theorem MIPRE.LIDT.CL.Regs.not_mem_coordSet_dir {ι : Type u_1} {n : ℕ} (R : Regs ι n) (j : Fin n) : R.dir j ∉ R.coordSet

theorem MIPRE.LIDT.CL.Regs.coord_mem_coordSet {ι : Type u_1} {n : ℕ} (R : Regs ι n) : R.coord ∈ R.coordSet

theorem MIPRE.LIDT.CL.Regs.questionOf_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.questionOf S t ((R.pres S t).eval x) = Sample.question hn (R.sampleOf S t x) t

The presentation computes the seeded question of the sample the registers carry.

The law of the sample

theorem MIPRE.LIDT.CL.Regs.embed_injective {ι : Type u_1} {n : ℕ} (R : Regs ι n) : Function.Injective (Sum.elim R.pt (Sum.elim (fun (x : Unit) => R.coord) R.dir))

The registers, as one injection of Fin n ⊕ (Unit ⊕ Fin n).

theorem MIPRE.LIDT.CL.Regs.sum_sampleOf {ι : 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] (t : Ty) (g : Sample F n → M) : ∑ x : ι → F, g (R.sampleOf S t x) = Fintype.card F ^ (Fintype.card ι - (2 * n + 1)) • ∑ u : Point F n, ∑ s : F, ∑ v : Point F n, g { tyA := t, tyB := t, u := u, s := s, v := v }

Uniform content gives a uniform sample: summing a function of the sample the registers carry over all vectors is summing it over all samples, q^{|ι| - (2n+1)} times.