The seeded CL low individual degree test

Blueprint def:lidt-cl, the paper's typed low-degree game game^ld (ldt.tex, sec:ld-game and fig:ld-decider), with parameters (q, m, d, ldc), q = #F admissible and m ∣ q. This is the test the paper's padded and simultaneous Pauli uses, and it is not the canonical-line test MIPRE.LIDT.lidtGame whose soundness is formalized: the two differ in which lines they sample and in how they label answers, which is the whole content of lem:lidt-reduction-setup.

What makes it "seeded"

A question of type ALine is a pair (u₀, s) ∈ F^m × F, not a line. The seed s selects the direction e_{χ(s)}, where χ(s) reads off which of the m equal blocks of F (there are q/m elements each, using m ∣ q) the element s falls into. So q/m seeds describe the same geometric line, and they remain different questions: a strategy is free to answer differently on two descriptions of one line, which is exactly why the reduction to the canonical-line test needs a choice or averaging argument.

DLine questions are triples (u₀, s, v') where v' is v with its first χ(s) coordinates zeroed. Base points are the canonical representatives u₀ = L^Ln_w(u) of MIPRE.CL.canonLin (blueprint def:cl-canonical), w being the direction.

The distribution

The verifier samples the ordered type pair uniformly from the nine possibilities and (u, s, v) uniformly from F^m × F × F^m, then hands each player the content its type prescribes. Every sample has the same weight, so normalization is one division rather than the subtest bookkeeping the canonical-line game needs.

The decision predicate

fig:ld-decider is a format check and then three numbered subtests. The check is the table at the top of the figure, and the text around it is explicit that it rejects: "If the answers returned by the players do not fit this format the decision procedure rejects." The subtests are: equal types, accept iff the answers agree; a line type against Point, accept iff every one of the ldc polynomials evaluated at the parameter of the point gives the corresponding coordinate of the point answer; and "in all cases where no action is indicated, accept".

Question.fmtOk is the check and subtests the rest, with accepts their conjunction. The separation matters because the two clauses that look alike are not: an answer of the wrong format for its question type is rejected, while a well-formatted answer to one of the two cross type pairs (ALine, DLine) and (DLine, ALine) is accepted --- that is the 2/9 of the question mass on which this test checks nothing.

Leaving the format check out makes the test vacuous, and an earlier version of this file did leave it out. The constant strategy answering values 0 to every question, the two line types included, then passes every subtest through the catch-all, so the game has a value-1 strategy whose point measurements are an arbitrary function of the point --- and thm:lidt-cl-soundness, which concludes that those measurements are consistent with evaluations of a low-individual-degree polynomial measurement, is false for it. accepts_aline_values_eq_false and accepts_point_apolys_eq_false pin the two rejections, and accepts_aline_dline pins the acceptance that must survive.

The one place this file is stricter than the paper

Where the paper writes "t ∈ F is such that x = u₀ + t w", the point may fail to lie on the line, and the condition is then vacuous. This file requires membership, as MIPRE.LIDT.lidtGame already does for the canonical-line test: the two agree on the support of the question distribution, where the point is always on the line, and keeping the convention of the test whose soundness is proved is what makes the two comparable at all.

The seed function

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

χ(s): which of the m blocks of q/m field elements the seed s falls into, under the fixed bijection F ≃ Fin q. The paper's eq:chi-func, 0-indexed. Needs m ∣ q.

Equations

• MIPRE.LIDT.CL.chi hm s = ⟨↑((Fintype.equivFin F) s) / (Fintype.card F / m), ⋯⟩

theorem MIPRE.LIDT.CL.card_div_pos {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) : 0 < Fintype.card F / m

The block size q / m, positive and with m * (q/m) = q.

theorem MIPRE.LIDT.CL.chi_val {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (s : F) : ↑(chi hm s) = ↑((Fintype.equivFin F) s) / (Fintype.card F / m)

theorem MIPRE.LIDT.CL.card_chi_fiber {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (i : Fin m) : {s : F | chi hm s = i}.card = Fintype.card F / m

Each seed block has exactly q / m elements. This is what makes the axis-parallel line distribution the seeded test induces uniform over lines, and it is the input lem:lidt-test-transfer consumes: q/m seeds describe each line, so a uniform seed gives a uniform direction index. It is where m ∣ q earns its place among the hypotheses.

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

π_i(v): v with its first i coordinates zeroed (the paper's π_{i-1} at a 0-indexed i).

Equations

• MIPRE.LIDT.CL.zeroBelow i v k = if ↑k < ↑i then 0 else v k

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

The canonical representative of the line through u in direction w: the paper's L^Ln_w(u), the canonical linear map with kernel span{w} applied to u.

Equations

• MIPRE.LIDT.CL.rep w u = (MIPRE.CL.canonLin (F ∙ w)) u

def MIPRE.LIDT.CL.lineParam {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (u₀ w x : Point F m) : F

The parameter of x on the line u₀ + t · w: with j the first nonzero coordinate of w, the unique t with x j = u₀ j + t · w j; 0 for a singleton line. Unlike MIPRE.LIDT.Line.param this does not assume the direction normalized, the seeded test's diagonal directions being arbitrary.

Equations

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

Questions, answers, and samples

inductive MIPRE.LIDT.CL.Ty : Type

The three question types.

• point : Ty
• aline : Ty
• dline : Ty

@[instance_reducible]

instance MIPRE.LIDT.CL.instDecidableEqTy : DecidableEq Ty

Equations

• MIPRE.LIDT.CL.instDecidableEqTy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MIPRE.LIDT.CL.instFintypeTy : Fintype Ty

Equations

• MIPRE.LIDT.CL.instFintypeTy = { elems := {MIPRE.LIDT.CL.Ty.point, MIPRE.LIDT.CL.Ty.aline, MIPRE.LIDT.CL.Ty.dline}, complete := ⋯ }

inductive MIPRE.LIDT.CL.Question (F : Type u_1) (m : ℕ) : Type u_1

Questions: a point, a seeded axis-parallel line, or a seeded diagonal line.

• point {F : Type u_1} {m : ℕ} (u : Point F m) : Question F m
• aline {F : Type u_1} {m : ℕ} (u₀ : Point F m) (s : F) : Question F m
• dline {F : Type u_1} {m : ℕ} (u₀ : Point F m) (s : F) (v : Point F m) : Question F m

def MIPRE.LIDT.CL.instDecidableEqQuestion.decEq {F✝ : Type u_2} {m✝ : ℕ} [DecidableEq F✝] (x✝ x✝¹ : Question F✝ m✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LIDT.CL.instDecidableEqQuestion.decEq (MIPRE.LIDT.CL.Question.point a) (MIPRE.LIDT.CL.Question.point b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqQuestion.decEq (MIPRE.LIDT.CL.Question.point u) (MIPRE.LIDT.CL.Question.aline u₀ s) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqQuestion.decEq (MIPRE.LIDT.CL.Question.point u) (MIPRE.LIDT.CL.Question.dline u₀ s v) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqQuestion.decEq (MIPRE.LIDT.CL.Question.aline u₀ s) (MIPRE.LIDT.CL.Question.point u) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqQuestion.decEq (MIPRE.LIDT.CL.Question.aline u₀ s) (MIPRE.LIDT.CL.Question.dline u₀_1 s_1 v) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqQuestion.decEq (MIPRE.LIDT.CL.Question.dline u₀ s v) (MIPRE.LIDT.CL.Question.point u) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqQuestion.decEq (MIPRE.LIDT.CL.Question.dline u₀ s v) (MIPRE.LIDT.CL.Question.aline u₀_1 s_1) = isFalse ⋯

@[instance_reducible]

instance MIPRE.LIDT.CL.instDecidableEqQuestion {F✝ : Type u_2} {m✝ : ℕ} [DecidableEq F✝] : DecidableEq (Question F✝ m✝)

Equations

• MIPRE.LIDT.CL.instDecidableEqQuestion = MIPRE.LIDT.CL.instDecidableEqQuestion.decEq

@[instance_reducible]

instance MIPRE.LIDT.CL.instFintypeQuestion {F✝ : Type u_2} {m✝ : ℕ} [Fintype F✝] : Fintype (Question F✝ m✝)

Equations

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

inductive MIPRE.LIDT.CL.Answer (F : Type u_1) (m d ldc : ℕ) : Type u_1

Answers: ldc field elements, or ldc polynomials of degree ≤ d or ≤ m·d.

• values {F : Type u_1} {m d ldc : ℕ} (a : Fin ldc → F) : Answer F m d ldc
• apolys {F : Type u_1} {m d ldc : ℕ} (f : Fin ldc → LinePoly F d) : Answer F m d ldc
• dpolys {F : Type u_1} {m d ldc : ℕ} (f : Fin ldc → LinePoly F (m * d)) : Answer F m d ldc

@[instance_reducible]

instance MIPRE.LIDT.CL.instDecidableEqAnswer {F✝ : Type u_2} {m✝ d✝ ldc✝ : ℕ} [DecidableEq F✝] : DecidableEq (Answer F✝ m✝ d✝ ldc✝)

Equations

• MIPRE.LIDT.CL.instDecidableEqAnswer = MIPRE.LIDT.CL.instDecidableEqAnswer.decEq

def MIPRE.LIDT.CL.instDecidableEqAnswer.decEq {F✝ : Type u_2} {m✝ d✝ ldc✝ : ℕ} [DecidableEq F✝] (x✝ x✝¹ : Answer F✝ m✝ d✝ ldc✝) : Decidable (x✝ = x✝¹)

Equations

• MIPRE.LIDT.CL.instDecidableEqAnswer.decEq (MIPRE.LIDT.CL.Answer.values a) (MIPRE.LIDT.CL.Answer.values b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqAnswer.decEq (MIPRE.LIDT.CL.Answer.values a) (MIPRE.LIDT.CL.Answer.apolys f) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqAnswer.decEq (MIPRE.LIDT.CL.Answer.values a) (MIPRE.LIDT.CL.Answer.dpolys f) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqAnswer.decEq (MIPRE.LIDT.CL.Answer.apolys f) (MIPRE.LIDT.CL.Answer.values a) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqAnswer.decEq (MIPRE.LIDT.CL.Answer.apolys a) (MIPRE.LIDT.CL.Answer.apolys b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqAnswer.decEq (MIPRE.LIDT.CL.Answer.apolys f) (MIPRE.LIDT.CL.Answer.dpolys f_1) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqAnswer.decEq (MIPRE.LIDT.CL.Answer.dpolys f) (MIPRE.LIDT.CL.Answer.values a) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqAnswer.decEq (MIPRE.LIDT.CL.Answer.dpolys f) (MIPRE.LIDT.CL.Answer.apolys f_1) = isFalse ⋯
• MIPRE.LIDT.CL.instDecidableEqAnswer.decEq (MIPRE.LIDT.CL.Answer.dpolys a) (MIPRE.LIDT.CL.Answer.dpolys b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MIPRE.LIDT.CL.instFintypeAnswer {F✝ : Type u_2} {m✝ d✝ ldc✝ : ℕ} [Fintype F✝] : Fintype (Answer F✝ m✝ d✝ ldc✝)

Equations

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

structure MIPRE.LIDT.CL.Sample (F : Type u_1) (m : ℕ) : Type u_1

The verifier's random choices: the ordered pair of types, and the ambient (u, s, v) ∈ F^m × F × F^m.

• tyA : Ty

  Alice's type.

• tyB : Ty

  Bob's type.

• u : Point F m

  The point.

• s : F

  The seed.

• v : Point F m

  The raw diagonal direction.

def MIPRE.LIDT.CL.instDecidableEqSample.decEq {F✝ : Type u_2} {m✝ : ℕ} [DecidableEq F✝] (x✝ x✝¹ : Sample F✝ m✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance MIPRE.LIDT.CL.instDecidableEqSample {F✝ : Type u_2} {m✝ : ℕ} [DecidableEq F✝] : DecidableEq (Sample F✝ m✝)

Equations

• MIPRE.LIDT.CL.instDecidableEqSample = MIPRE.LIDT.CL.instDecidableEqSample.decEq

@[instance_reducible]

instance MIPRE.LIDT.CL.instFintypeSample {F✝ : Type u_2} {m✝ : ℕ} [Fintype F✝] : Fintype (Sample F✝ m✝)

Equations

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

noncomputable def MIPRE.LIDT.CL.Sample.question {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (sm : Sample F m) : Ty → Question F m

The question a player of type t receives. The paper's typed CL functions L_Point, L_ALine, L_DLine of eq:cl-ptf–eq:cl-dlnf, read off the ambient sample.

Equations

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

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

The direction a line question describes.

Equations

• MIPRE.LIDT.CL.Question.dir hm (MIPRE.LIDT.CL.Question.point a) = 0
• MIPRE.LIDT.CL.Question.dir hm (MIPRE.LIDT.CL.Question.aline a a_1) = Pi.single (MIPRE.LIDT.CL.chi hm a_1) 1
• MIPRE.LIDT.CL.Question.dir hm (MIPRE.LIDT.CL.Question.dline a a_1 a_2) = a_2

def MIPRE.LIDT.CL.Question.base {F : Type u_1} {m : ℕ} : Question F m → Point F m

The base point a question carries.

Equations

• (MIPRE.LIDT.CL.Question.point a).base = a
• (MIPRE.LIDT.CL.Question.aline a a_1).base = a
• (MIPRE.LIDT.CL.Question.dline a a_1 a_2).base = a

theorem MIPRE.LIDT.CL.aline_question_ne {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (sm : Sample F m) (s' : F) (hs : chi hm s' = chi hm sm.s) (hne : s' ≠ sm.s) : Sample.question hm { tyA := sm.tyA, tyB := sm.tyB, u := sm.u, s := s', v := sm.v } Ty.aline ≠ Sample.question hm sm Ty.aline

Two seeds in the same block of q/m describe the same geometric line --- the base point and the direction agree --- but are different questions. This is the "seeded" in the test's name, and the reason lem:lidt-reduction-setup needs a choice or averaging argument to convert a seeded strategy into one for the canonical-line test: a strategy may answer differently on two descriptions of one line.

The decision predicate

def MIPRE.LIDT.CL.lineVsPoint {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m ldc : ℕ} (u₀ w x : Point F m) {n : ℕ} (f : Fin ldc → LinePoly F n) (a : Fin ldc → F) : Bool

A line answer against a point answer: the point lies on the line, and each of the ldc polynomials evaluated at the parameter of the point gives the corresponding coordinate.

Equations

• MIPRE.LIDT.CL.lineVsPoint u₀ w x f a = decide ((∃ (t : F), x = u₀ + t • w) ∧ ∀ (j : Fin ldc), (f j).eval (MIPRE.LIDT.CL.lineParam u₀ w x) = a j)

def MIPRE.LIDT.CL.Question.fmtOk {F : Type u_1} {m d ldc : ℕ} : Question F m → Answer F m d ldc → Bool

Whether an answer has the format the question's type prescribes, which is the table at the top of fig:ld-decider: a Point question is answered by ldc field elements, an ALine question by ldc polynomials of degree ≤ d, a DLine question by ldc polynomials of degree ≤ m·d. The decider's first step checks this and rejects if it fails ("If the answers returned by the players do not fit this format the decision procedure rejects").

Equations

• (MIPRE.LIDT.CL.Question.point u).fmtOk (MIPRE.LIDT.CL.Answer.values a) = true
• (MIPRE.LIDT.CL.Question.aline u₀ s).fmtOk (MIPRE.LIDT.CL.Answer.apolys f) = true
• (MIPRE.LIDT.CL.Question.dline u₀ s v).fmtOk (MIPRE.LIDT.CL.Answer.dpolys f) = true
• x✝¹.fmtOk x✝ = false

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

The three numbered subtests of fig:ld-decider, on correctly formatted answers: equal types accept iff the answers agree, a line type against Point accepts iff each polynomial evaluated at the parameter of the point gives the corresponding coordinate, and "in all cases where no action is indicated, accept" --- which after the format check of accepts means exactly the two cross type pairs (ALine, DLine) and (DLine, ALine).

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LIDT.CL.subtests hm (MIPRE.LIDT.CL.Question.point u) (MIPRE.LIDT.CL.Question.point u_1) (MIPRE.LIDT.CL.Answer.values a) (MIPRE.LIDT.CL.Answer.values b) = decide (a = b)
• MIPRE.LIDT.CL.subtests hm (MIPRE.LIDT.CL.Question.aline u₀ s) (MIPRE.LIDT.CL.Question.aline u₀_1 s_1) (MIPRE.LIDT.CL.Answer.apolys f) (MIPRE.LIDT.CL.Answer.apolys g) = decide (f = g)
• MIPRE.LIDT.CL.subtests hm (MIPRE.LIDT.CL.Question.dline u₀ s v) (MIPRE.LIDT.CL.Question.dline u₀_1 s_1 v_1) (MIPRE.LIDT.CL.Answer.dpolys f) (MIPRE.LIDT.CL.Answer.dpolys g) = decide (f = g)
• MIPRE.LIDT.CL.subtests hm x✝³ x✝² x✝¹ x✝ = true

noncomputable def MIPRE.LIDT.CL.accepts {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (x y : Question F m) (a b : Answer F m d ldc) : Bool

The decision predicate of fig:ld-decider: the format check, then the subtests.

Equations

• MIPRE.LIDT.CL.accepts hm x y a b = (x.fmtOk a && y.fmtOk b && MIPRE.LIDT.CL.subtests hm x y a b)

The format check rejects

These are the cases the catch-all of subtests would otherwise accept, and they are why the check cannot be left out: without it the constant strategy answering values 0 to every question --- including the two line types, for which that is the wrong format --- passes every subtest, so the test has a value-1 strategy whose point measurements are an arbitrary function of the point, and thm:lidt-cl-soundness is false for the game.

@[simp]

theorem MIPRE.LIDT.CL.accepts_eq_false_left {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) {x y : Question F m} {a b : Answer F m d ldc} (h : x.fmtOk a = false) : accepts hm x y a b = false

@[simp]

theorem MIPRE.LIDT.CL.accepts_eq_false_right {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) {x y : Question F m} {a b : Answer F m d ldc} (h : y.fmtOk b = false) : accepts hm x y a b = false

theorem MIPRE.LIDT.CL.accepts_aline_values_eq_false {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (u₀ : Point F m) (s : F) (y : Question F m) (a : Fin ldc → F) (b : Answer F m d ldc) : accepts hm (Question.aline u₀ s) y (Answer.values a) b = false

A line question answered in the point format is rejected --- the case that made the test vacuous before the format check was added.

theorem MIPRE.LIDT.CL.accepts_point_apolys_eq_false {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (u : Point F m) (y : Question F m) (f : Fin ldc → LinePoly F d) (b : Answer F m d ldc) : accepts hm (Question.point u) y (Answer.apolys f) b = false

A point question answered in a line format is rejected.

theorem MIPRE.LIDT.CL.accepts_aline_dline {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (u₀ : Point F m) (s : F) (u₀' : Point F m) (s' : F) (v : Point F m) (f : Fin ldc → LinePoly F d) (g : Fin ldc → LinePoly F (m * d)) : accepts hm (Question.aline u₀ s) (Question.dline u₀' s' v) (Answer.apolys f) (Answer.dpolys g) = true

The two cross type pairs are still accepted on well-formatted answers, as fig:ld-decider's "in all cases where no action is indicated, accept" prescribes. This is the 2/9 of the question mass on which the test checks nothing.

The game

noncomputable def MIPRE.LIDT.CL.clGame {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d ldc : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) : Game (Question F m) (Question F m) (Answer F m d ldc) (Answer F m d ldc)

The seeded CL low individual degree test as a game (blueprint def:lidt-cl).

Equations

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

Vocabulary for the soundness statement

The reduction to the canonical-line test (MIPRE.LIDT.Adapter) concludes about the players' point measurements, so those need a name on this side too. MIPRE.LIDT.Answer.toValue is the same reading for the canonical-line test.

def MIPRE.LIDT.CL.Answer.toValue {F : Type u_1} [Field F] {m d : ℕ} : Answer F m d 1 → F

The field element a point answer carries, for ldc = 1; answers of the wrong format are read as 0, which only helps the strategy since the test rejects them (Question.fmtOk).

Equations

• (MIPRE.LIDT.CL.Answer.values a).toValue = a 0
• x✝.toValue = 0

noncomputable def MIPRE.LIDT.CL.pointPOVMA {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (S : TensorProductStrategy (clGame hm)) (u : Point F m) : POVM F (Fin S.dA)

The point measurements of player A in a strategy for the seeded test, as POVMs with outcomes in F.

Equations

• MIPRE.LIDT.CL.pointPOVMA S u = MIPRE.POVM.map MIPRE.LIDT.CL.Answer.toValue (S.PA.toPOVM (MIPRE.LIDT.CL.Question.point u))

noncomputable def MIPRE.LIDT.CL.pointPOVMB {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (S : TensorProductStrategy (clGame hm)) (u : Point F m) : POVM F (Fin S.dB)

The point measurements of player B in a strategy for the seeded test, as POVMs with outcomes in F.

Equations

• MIPRE.LIDT.CL.pointPOVMB S u = MIPRE.POVM.map MIPRE.LIDT.CL.Answer.toValue (S.PB.toPOVM (MIPRE.LIDT.CL.Question.point u))