The classical low individual degree test

The (m, q, d)-low individual degree test of Ji, Natarajan, Vidick, Wright and Yuen, Quantum soundness of the classical low individual degree test (arXiv:2009.12982, Figure 1), as a two-player game MIPRE.LIDT.lidtGame over a finite field F with q elements. With probability 1/3 each, the verifier runs one of three sub-tests, on a uniform point u ∈ F^m:

• axis-parallel lines: one player (chosen at random) receives the line through u in a uniform coordinate direction and answers a univariate polynomial f of degree ≤ d, the other receives u and answers a ∈ F; accept iff f(u) = a;
• self-consistency: both receive u, accept iff the answers agree;
• diagonal lines: as the first test, with the line through u in a direction v uniform among the vectors whose coordinates beyond a uniform index j vanish (v = 0, a singleton line, is allowed), and a polynomial of degree ≤ m·d.

Polynomials are represented by their coefficients (LinePoly), so that the alphabets are finite types without further ado. A line is a pair (base, direction); the verifier only ever asks the canonical presentation Line.through u v of a line (direction rescaled so that its first nonzero coordinate is 1, base point moved so that this coordinate is 0), so that a line is the same question however it was sampled. Line answers are polynomials in the parameter t of base + t • direction, and are evaluated at the parameter Line.param ℓ u of the sampled point. The question distribution is the push-forward of the verifier's random choices Sample.

@[reducible, inline]

abbrev MIPRE.LIDT.Point (F : Type u_1) (m : ℕ) : Type u_1

Points of F^m.

Equations

• MIPRE.LIDT.Point F m = (Fin m → F)

@[reducible, inline]

abbrev MIPRE.LIDT.LinePoly (F : Type u_1) (n : ℕ) : Type u_1

Univariate polynomials over F of degree at most n, given by their coefficients.

Equations

• MIPRE.LIDT.LinePoly F n = (Fin (n + 1) → F)

def MIPRE.LIDT.LinePoly.eval {F : Type u_2} [Field F] {n : ℕ} (f : LinePoly F n) (t : F) : F

Evaluation of a polynomial of degree at most n.

Equations

• f.eval t = ∑ i : Fin (n + 1), f i * t ^ ↑i

@[reducible, inline]

abbrev MIPRE.LIDT.Line (F : Type u_1) (m : ℕ) : Type u_1

A line in F^m, presented by a base point and a direction: {base + t • direction}.

Equations

• MIPRE.LIDT.Line F m = (MIPRE.LIDT.Point F m × MIPRE.LIDT.Point F m)

noncomputable def MIPRE.LIDT.Line.through {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (u v : Point F m) : Line F m

The canonical presentation of the line through u in direction v: if v ≠ 0 and j is its first nonzero coordinate, the direction is v / v_j and the base point is the point of the line with vanishing j-th coordinate; if v = 0, the pair (u, 0).

Equations

• MIPRE.LIDT.Line.through u v = if h : ∃ (j : Fin m), v j ≠ 0 then have j := Fin.find (fun (j : Fin m) => v j ≠ 0) h; (u - u j • (v j)⁻¹ • v, (v j)⁻¹ • v) else (u, 0)

def MIPRE.LIDT.Line.Mem {F : Type u_1} [Field F] {m : ℕ} (ℓ : Line F m) (x : Point F m) : Prop

Membership of a point in a line.

Equations

• ℓ.Mem x = ∃ (t : F), x = ℓ.1 + t • ℓ.2

@[instance_reducible]

instance MIPRE.LIDT.Line.instDecidablePredPointMem {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (ℓ : Line F m) : DecidablePred ℓ.Mem

Equations

• ℓ.instDecidablePredPointMem x✝ = id inferInstance

noncomputable def MIPRE.LIDT.Line.param {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} (ℓ : Line F m) (x : Point F m) : F

The parameter of a point of a canonically presented line: its coordinate at the first nonzero coordinate of the direction (0 for a singleton line).

Equations

• ℓ.param x = if h : ∃ (j : Fin m), ℓ.2 j ≠ 0 then x (Fin.find (fun (j : Fin m) => ℓ.2 j ≠ 0) h) else 0

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

Questions: a point, an axis-parallel line, or a (diagonal) line.

• point {F : Type u_1} {m : ℕ} (u : Point F m) : Question F m
• axisLine {F : Type u_1} {m : ℕ} (ℓ : Line F m) : Question F m
• diagLine {F : Type u_1} {m : ℕ} (ℓ : Line F m) : Question F m

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

Equations

• MIPRE.LIDT.instDecidableEqQuestion.decEq (MIPRE.LIDT.Question.point a) (MIPRE.LIDT.Question.point b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.LIDT.instDecidableEqQuestion.decEq (MIPRE.LIDT.Question.point u) (MIPRE.LIDT.Question.axisLine ℓ) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqQuestion.decEq (MIPRE.LIDT.Question.point u) (MIPRE.LIDT.Question.diagLine ℓ) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqQuestion.decEq (MIPRE.LIDT.Question.axisLine ℓ) (MIPRE.LIDT.Question.point u) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqQuestion.decEq (MIPRE.LIDT.Question.axisLine a) (MIPRE.LIDT.Question.axisLine b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.LIDT.instDecidableEqQuestion.decEq (MIPRE.LIDT.Question.axisLine ℓ) (MIPRE.LIDT.Question.diagLine ℓ_1) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqQuestion.decEq (MIPRE.LIDT.Question.diagLine ℓ) (MIPRE.LIDT.Question.point u) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqQuestion.decEq (MIPRE.LIDT.Question.diagLine ℓ) (MIPRE.LIDT.Question.axisLine ℓ_1) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqQuestion.decEq (MIPRE.LIDT.Question.diagLine a) (MIPRE.LIDT.Question.diagLine b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• MIPRE.LIDT.instFintypeQuestion = Fintype.ofEquiv (MIPRE.LIDT.Point F✝ m✝ ⊕ MIPRE.LIDT.Line F✝ m✝ ⊕ MIPRE.LIDT.Line F✝ m✝) (MIPRE.LIDT.Question.proxyTypeEquiv F✝ m✝)

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

Answers: a field element, a polynomial of degree ≤ d, or one of degree ≤ m·d.

• value {F : Type u_1} {m d : ℕ} (a : F) : Answer F m d
• axisPoly {F : Type u_1} {m d : ℕ} (f : LinePoly F d) : Answer F m d
• diagPoly {F : Type u_1} {m d : ℕ} (f : LinePoly F (m * d)) : Answer F m d

@[instance_reducible]

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

Equations

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

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

Equations

• MIPRE.LIDT.instDecidableEqAnswer.decEq (MIPRE.LIDT.Answer.value a) (MIPRE.LIDT.Answer.value b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.LIDT.instDecidableEqAnswer.decEq (MIPRE.LIDT.Answer.value a) (MIPRE.LIDT.Answer.axisPoly f) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqAnswer.decEq (MIPRE.LIDT.Answer.value a) (MIPRE.LIDT.Answer.diagPoly f) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqAnswer.decEq (MIPRE.LIDT.Answer.axisPoly f) (MIPRE.LIDT.Answer.value a) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqAnswer.decEq (MIPRE.LIDT.Answer.axisPoly a) (MIPRE.LIDT.Answer.axisPoly b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.LIDT.instDecidableEqAnswer.decEq (MIPRE.LIDT.Answer.axisPoly f) (MIPRE.LIDT.Answer.diagPoly f_1) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqAnswer.decEq (MIPRE.LIDT.Answer.diagPoly f) (MIPRE.LIDT.Answer.value a) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqAnswer.decEq (MIPRE.LIDT.Answer.diagPoly f) (MIPRE.LIDT.Answer.axisPoly f_1) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqAnswer.decEq (MIPRE.LIDT.Answer.diagPoly a) (MIPRE.LIDT.Answer.diagPoly b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

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

Equations

• MIPRE.LIDT.instFintypeAnswer = Fintype.ofEquiv (F✝ ⊕ MIPRE.LIDT.LinePoly F✝ d✝ ⊕ MIPRE.LIDT.LinePoly F✝ (m✝ * d✝)) (MIPRE.LIDT.Answer.proxyTypeEquiv F✝ m✝ d✝)

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

The verifier's random choices: the sub-test, whether the roles are swapped (the line goes to player B), the point u, the direction index i or j, and for diagonal lines the first j + 1 coordinates of the direction (the others vanish).

• axis {F : Type u_1} {m : ℕ} (swap : Bool) (u : Point F m) (i : Fin m) : Sample F m
• selfConsistency {F : Type u_1} {m : ℕ} (u : Point F m) : Sample F m
• diag {F : Type u_1} {m : ℕ} (swap : Bool) (u : Point F m) (j : Fin m) (v : Fin (↑j + 1) → F) : Sample F m

@[instance_reducible]

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

Equations

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

def MIPRE.LIDT.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.
• MIPRE.LIDT.instDecidableEqSample.decEq (MIPRE.LIDT.Sample.axis swap u i) (MIPRE.LIDT.Sample.selfConsistency u_1) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqSample.decEq (MIPRE.LIDT.Sample.axis swap u i) (MIPRE.LIDT.Sample.diag swap_1 u_1 j v) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqSample.decEq (MIPRE.LIDT.Sample.selfConsistency u) (MIPRE.LIDT.Sample.axis swap u_1 i) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqSample.decEq (MIPRE.LIDT.Sample.selfConsistency a) (MIPRE.LIDT.Sample.selfConsistency b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.LIDT.instDecidableEqSample.decEq (MIPRE.LIDT.Sample.selfConsistency u) (MIPRE.LIDT.Sample.diag swap u_1 j v) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqSample.decEq (MIPRE.LIDT.Sample.diag swap u j v) (MIPRE.LIDT.Sample.axis swap_1 u_1 i) = isFalse ⋯
• MIPRE.LIDT.instDecidableEqSample.decEq (MIPRE.LIDT.Sample.diag swap u j v) (MIPRE.LIDT.Sample.selfConsistency u_1) = isFalse ⋯

@[instance_reducible]

instance MIPRE.LIDT.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.Sample.weight {F : Type u_1} [Fintype F] {m : ℕ} : Sample F m → ℝ

The probability of a sample: each sub-test has probability 1/3, and within a sub-test the swap, the point, the direction index and the direction are uniform.

Equations

• (MIPRE.LIDT.Sample.axis a a_1 a_2).weight = 1 / (6 * ↑m * ↑(Fintype.card (MIPRE.LIDT.Point F m)))
• (MIPRE.LIDT.Sample.selfConsistency a).weight = 1 / (3 * ↑(Fintype.card (MIPRE.LIDT.Point F m)))
• (MIPRE.LIDT.Sample.diag a a_1 a_2 a_3).weight = 1 / (6 * ↑m * ↑(Fintype.card (MIPRE.LIDT.Point F m)) * ↑(Fintype.card F) ^ (↑a_2 + 1))

theorem MIPRE.LIDT.Sample.weight_nonneg {F : Type u_1} [Field F] [Fintype F] {m : ℕ} (s : Sample F m) : 0 ≤ s.weight

def MIPRE.LIDT.Sample.equivSum {F : Type u_1} {m : ℕ} : Sample F m ≃ Bool × Point F m × Fin m ⊕ Point F m ⊕ Bool × Point F m × (j : Fin m) × (Fin (↑j + 1) → F)

Samples as a disjoint union of products, for summing over them.

Equations

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

theorem MIPRE.LIDT.Sample.sum_weight {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] : ∑ s : Sample F m, s.weight = 1

The total probability is one (for m ≠ 0).

def MIPRE.LIDT.Sample.extend {F : Type u_1} [Field F] {m : ℕ} {j : Fin m} (v : Fin (↑j + 1) → F) : Point F m

The direction with the given first j + 1 coordinates and vanishing other coordinates.

Equations

• MIPRE.LIDT.Sample.extend v k = if h : ↑k ≤ ↑j then v ⟨↑k, ⋯⟩ else 0

noncomputable def MIPRE.LIDT.Sample.questions {F : Type u_1} [Field F] [DecidableEq F] {m : ℕ} : Sample F m → Question F m × Question F m

The question pair of a sample (first component to player A).

Equations

• One or more equations did not get rendered due to their size.
• (MIPRE.LIDT.Sample.selfConsistency a).questions = (MIPRE.LIDT.Question.point a, MIPRE.LIDT.Question.point a)

noncomputable def MIPRE.LIDT.accepts (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] (m d : ℕ) : Question F m → Question F m → Answer F m d → Answer F m d → Bool

The decision predicate: a line answer f and a point answer a are accepted iff the point lies on the line and f evaluated at the parameter of the point is a; two point answers are accepted iff the points are equal and the answers agree.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.LIDT.accepts F m d (MIPRE.LIDT.Question.point x_4) (MIPRE.LIDT.Question.point y) (MIPRE.LIDT.Answer.value a) (MIPRE.LIDT.Answer.value b) = decide (x_4 = y ∧ a = b)
• MIPRE.LIDT.accepts F m d x✝³ x✝² x✝¹ x✝ = false

noncomputable def MIPRE.LIDT.lidtGame (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] (m d : ℕ) [NeZero m] : Game (Question F m) (Question F m) (Answer F m d) (Answer F m d)

The (m, q, d)-low individual degree test as a game, q = Fintype.card F, m ≠ 0.

Equations

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

Vocabulary for the soundness theorem

@[reducible, inline]

abbrev MIPRE.LIDT.LowIndDegPoly {F : Type u_1} {m d : ℕ} : Type u_1

Polynomials in m variables of individual degree at most d, given by their coefficients on the monomials ∏ᵢ Xᵢ^(eᵢ) with all eᵢ ≤ d.

Equations

• MIPRE.LIDT.LowIndDegPoly = ((Fin m → Fin (d + 1)) → F)

def MIPRE.LIDT.LowIndDegPoly.eval {F : Type u_1} [Field F] {m d : ℕ} (p : LowIndDegPoly) (u : Point F m) : F

Evaluation at a point of F^m.

Equations

• p.eval u = ∑ e : Fin m → Fin (d + 1), p e * ∏ i : Fin m, u i ^ ↑(e i)

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

The field element answered to a point question; ill-typed answers are read as 0 (they are rejected by the test, so this only helps the strategy).

Equations

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

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

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

Equations

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

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

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

Equations

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

noncomputable def MIPRE.LIDT.evalPOVM {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {n : Type u_2} [Fintype n] [DecidableEq n] (G : ProjectiveMeasurement Unit LowIndDegPoly (Matrix n n ℂ)) (u : Point F m) : POVM F n

Evaluation at u of a measurement G with polynomial outcomes: the POVM with outcomes in F whose operator for a is the sum of the operators of the polynomials p with p(u) = a.

Equations

• MIPRE.LIDT.evalPOVM G u = MIPRE.POVM.map (fun (p : MIPRE.LIDT.LowIndDegPoly) => p.eval u) (G.toPOVM ())

noncomputable def MIPRE.LIDT.lidtError (m d q k : ℕ) (ε : ℝ) : ℝ

The error bound of the soundness theorem, as proved in the MIPStarRE development: 100000 · k² · m⁴ · (ε^(1/40000) + (d/q)^(1/40000) + exp(−k / (2560000 m²))).

Equations

• MIPRE.LIDT.lidtError m d q k ε = 100000 * ↑k ^ 2 * ↑m ^ 4 * (ε ^ (1 / 40000) + (↑d / ↑q) ^ (1 / 40000) + Real.exp (-↑k / (2560000 * ↑m ^ 2)))