The honest Pauli strategy passes its actual low-degree edges

The coefficient vectors used by the measurements are restrictions of the same multilinear encoding. Both seeded line types include their sampled point, including zero diagonal directions. Coarse measurements of the same Pauli PVM therefore commute and have zero product on every rejected pair.

theorem MIPRE.QLD.Honest.eval_lineAnswer {F : Type u_1} [Field F] {m n : ℕ} (u v : LIDT.Point F m) (h : Register F m) (hn : (LowDegree.lineRestrict u v (LowDegree.ldEnc h)).natDegree ≤ n) (t : F) : (lineAnswer n u v h).eval t = (MvPolynomial.eval (u + t • v)) (LowDegree.ldEnc h)

theorem MIPRE.QLD.Honest.lowDeg_lineAnswer_rep {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m n : ℕ} (v u : LIDT.Point F m) (h : Register F m) (hn : (LowDegree.lineRestrict (LIDT.CL.rep v u) v (LowDegree.ldEnc h)).natDegree ≤ n) : lowDeg (LIDT.CL.rep v u) v u (lineAnswer n (LIDT.CL.rep v u) v h) ((MvPolynomial.eval u) (LowDegree.ldEnc h)) = true

The seeded representative and parameter recover even a degenerate line.

theorem MIPRE.QLD.Honest.lowDeg_axis_lineAnswer {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} (hd : 1 ≤ d) (i : Fin m) (u : LIDT.Point F m) (h : Register F m) : lowDeg (LIDT.CL.rep (Pi.single i 1) u) (Pi.single i 1) u (lineAnswer d (LIDT.CL.rep (Pi.single i 1) u) (Pi.single i 1) h) ((MvPolynomial.eval u) (LowDegree.ldEnc h)) = true

theorem MIPRE.QLD.Honest.lowDeg_diagonal_lineAnswer {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} (hd : 1 ≤ d) (v u : LIDT.Point F m) (h : Register F m) : lowDeg (LIDT.CL.rep v u) v u (lineAnswer (m * d) (LIDT.CL.rep v u) v h) ((MvPolynomial.eval u) (LowDegree.ldEnc h)) = true

theorem MIPRE.QLD.Honest.answerOp_aline_point_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (c : Content F m) (W : Bas) (a b : Answer F m d) : Commute (answerOp hm (Content.question hm c (Ty.aline W)) a) (answerOp hm (Content.question hm c (Ty.point W)) b)

theorem MIPRE.QLD.Honest.answerOp_dline_point_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (c : Content F m) (W : Bas) (a b : Answer F m d) : Commute (answerOp hm (Content.question hm c (Ty.dline W)) a) (answerOp hm (Content.question hm c (Ty.point W)) b)

theorem MIPRE.QLD.Honest.answerOp_pauli_point_commute {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (c : Content F m) (W : Bas) (a b : Answer F m d) : Commute (answerOp hm (Content.question hm c (Ty.pauli W)) a) (answerOp hm (Content.question hm c (Ty.point W)) b)

theorem MIPRE.QLD.Honest.answerOp_aline_point_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) (c : Content F m) (W : Bas) (a b : Answer F m d) (hr : accepts hm (Content.question hm c (Ty.aline W)) (Content.question hm c (Ty.point W)) a b = false) : answerOp hm (Content.question hm c (Ty.aline W)) a * answerOp hm (Content.question hm c (Ty.point W)) b = 0

theorem MIPRE.QLD.Honest.answerOp_dline_point_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) (c : Content F m) (W : Bas) (a b : Answer F m d) (hr : accepts hm (Content.question hm c (Ty.dline W)) (Content.question hm c (Ty.point W)) a b = false) : answerOp hm (Content.question hm c (Ty.dline W)) a * answerOp hm (Content.question hm c (Ty.point W)) b = 0

theorem MIPRE.QLD.Honest.answerOp_pauli_point_reject {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (c : Content F m) (W : Bas) (a b : Answer F m d) (hr : accepts hm (Content.question hm c (Ty.pauli W)) (Content.question hm c (Ty.point W)) a b = false) : answerOp hm (Content.question hm c (Ty.pauli W)) a * answerOp hm (Content.question hm c (Ty.point W)) b = 0