The bits of the honest Pauli basis test measurements

The honest strategy answers the twenty-six Pauli question types with MIPRE.QLD.Honest.answerOp, and the introspection verifier reads the answers through their bit encoding QLD.PauliAnswerProgram.answerBits (field elements in Shoup's polynomial basis, rows flattened). This file shows that every answer bit is a signed permutation observable, and a diagonal one at the readable (Pauli, Z) question (isXBit_answerOp, isZBit_answerOp_pauliZ):

• the point, line and Pauli answers are F_q-linear functions of the outcome of the X- or Z-basis measurement, and the bits of Shoup's representation are F₂-linear (shoupXorBits_correct), so each answer bit is an F₂-linear functional of the outcome, whose observable is a Weyl operator (exists_encObs_proj_linear); every bit of a Z-basis outcome is a ±1 diagonal;
• the probe answers read ½(1 ± W(c)) of a Weyl operator, and the Magic Square answers the cells of Introspection.HonestMagicSquare.grid of two Weyl operators, which are signed permutations (isSignedPerm_grid); in the inactive branches the answer is constant.

F₂-linear bits

theorem MIPRE.Tailored.Intro.exists_dual_of_xor {X : Type u_1} [AddCommGroup X] [Module (ZMod 2) X] (β : X → Bool) (hβ : ∀ (x y : X), β (x + y) = (β x ^^ β y)) : ∃ (ψ : Module.Dual (ZMod 2) X), ∀ (x : X), β x = decide (ψ x = 1)

A bit that is additive (the bit of a sum is the exclusive or) is an F₂-linear functional.

theorem MIPRE.Tailored.Intro.getD_xorBits (l l' : Cost.BitStr) (h : List.length l = List.length l') (i : ℕ) : List.getD (LowDegree.BinaryPolynomial.xorBits l l') i false = (List.getD l i false ^^ List.getD l' i false)

theorem MIPRE.Tailored.Intro.length_flatten_vecBits {k : ℕ} (hk : 1 ≤ k) {n : ℕ} (v : Fin n → (SAT.shoupBinField k hk).carrier) : ((SAT.shoupBinField k hk).vecBits v).flatten.length = n * k

theorem MIPRE.Tailored.Intro.flatten_vecBits_add {k : ℕ} (hk : 1 ≤ k) {n : ℕ} (v w : Fin n → (SAT.shoupBinField k hk).carrier) : ((SAT.shoupBinField k hk).vecBits (v + w)).flatten = LowDegree.BinaryPolynomial.xorBits ((SAT.shoupBinField k hk).vecBits v).flatten ((SAT.shoupBinField k hk).vecBits w).flatten

The bits of a vector of field elements are additive.

theorem MIPRE.Tailored.Intro.getD_flatten_vecBits_add {k : ℕ} (hk : 1 ≤ k) {n : ℕ} (v w : Fin n → (SAT.shoupBinField k hk).carrier) (i : ℕ) : ((SAT.shoupBinField k hk).vecBits (v + w)).flatten.getD i false = (((SAT.shoupBinField k hk).vecBits v).flatten.getD i false ^^ ((SAT.shoupBinField k hk).vecBits w).flatten.getD i false)

The Pauli measurements

theorem MIPRE.Tailored.Intro.isSignedPerm_basis {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (W : QLD.Bas) (c : QLD.Honest.Register F m) : IsSignedPerm (QLD.Honest.basis W c)

theorem MIPRE.Tailored.Intro.isXBit_pauliOp {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (W : QLD.Bas) (β : QLD.Honest.Register F m → Bool) (hβ : ∀ (x y : QLD.Honest.Register F m), β (x + y) = (β x ^^ β y)) : IsXBit (QLD.Honest.pauliOp W) β

An additive bit of a Pauli outcome is a signed permutation.

theorem MIPRE.Tailored.Intro.isZBit_pauliOp_Z {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (β : QLD.Honest.Register F m → Bool) : IsZBit (QLD.Honest.pauliOp QLD.Bas.Z) β

Every bit of a Z-basis outcome is a ±1 diagonal.

theorem MIPRE.Tailored.Intro.isXBit_pauliLift {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (W : QLD.Bas) (β : QLD.Honest.Register F m → Bool) (hβ : ∀ (x y : QLD.Honest.Register F m), β (x + y) = (β x ^^ β y)) : IsXBit (QLD.Honest.pauliLift W) β

theorem MIPRE.Tailored.Intro.isZBit_pauliLift_Z {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (β : QLD.Honest.Register F m → Bool) : IsZBit (QLD.Honest.pauliLift QLD.Bas.Z) β

theorem MIPRE.Tailored.Intro.probeLabel_add {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : QLD.Omega F m) (W : QLD.Bas) (h h' : QLD.Honest.Register F m) : QLD.Honest.probeLabel ω W (h + h') = QLD.Honest.probeLabel ω W h + QLD.Honest.probeLabel ω W h'

The probe label is additive in the outcome.

theorem MIPRE.Tailored.Intro.isXBit_probeLift {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : QLD.Omega F m) (W : QLD.Bas) (g : ZMod 2 → Bool) : IsXBit (QLD.Honest.probeLift ω W) g

Any bit of the probe's outcome is a signed permutation: a binary outcome's bit is constant or affine, and the probe reads an F₂-linear functional of a Pauli outcome.

theorem MIPRE.Tailored.Intro.ldEnc_add {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (h h' : QLD.Honest.Register F m) : LowDegree.ldEnc (h + h') = LowDegree.ldEnc h + LowDegree.ldEnc h'

theorem MIPRE.Tailored.Intro.lineAnswer_add {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (n : ℕ) (u v : LIDT.Point F m) (h h' : QLD.Honest.Register F m) : QLD.Honest.lineAnswer n u v (h + h') = QLD.Honest.lineAnswer n u v h + QLD.Honest.lineAnswer n u v h'

Binary measurements and the Magic Square

theorem MIPRE.Tailored.Intro.sum_observableToProjector {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (O : Matrix Ω Ω ℂ) : ∑ b : ZMod 2, LCS.observableToProjector O b = 1

theorem MIPRE.Tailored.Intro.isXBit_mul_fst {Ω : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Ω] [DecidableEq Ω] [Fintype A] [Fintype B] {P : A → Matrix Ω Ω ℂ} {Q : B → Matrix Ω Ω ℂ} (hQ : ∑ b : B, Q b = 1) {f : A → Bool} (h : IsXBit P f) : IsXBit (fun (ab : A × B) => P ab.1 * Q ab.2) fun (ab : A × B) => f ab.1

theorem MIPRE.Tailored.Intro.isXBit_mul_snd {Ω : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Ω] [DecidableEq Ω] [Fintype A] [Fintype B] {P : A → Matrix Ω Ω ℂ} {Q : B → Matrix Ω Ω ℂ} (hP : ∑ a : A, P a = 1) {f : B → Bool} (h : IsXBit Q f) : IsXBit (fun (ab : A × B) => P ab.1 * Q ab.2) fun (ab : A × B) => f ab.2

theorem MIPRE.Tailored.Intro.bool_affine (g : ZMod 2 → Bool) (b : ZMod 2) : g b = (g 0 ^^ decide (b = 1) && (g 0 ^^ g 1))

A bit of a binary outcome is constant or affine.

theorem MIPRE.Tailored.Intro.isXBit_observableToProjector {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {O : Matrix Ω Ω ℂ} (hO : IsSignedPerm O) (g : ZMod 2 → Bool) : IsXBit (LCS.observableToProjector O) g

Any bit of the binary measurement ½(1 ± O) of a signed permutation is one.

The answers

noncomputable def MIPRE.Tailored.Intro.answerBit {k : ℕ} (hk : 1 ≤ k) {m d : ℕ} (i : ℕ) (a : QLD.Answer (SAT.shoupBinField k hk).carrier m d) : Bool

The i-th bit of the encoded answer.

Equations

• MIPRE.Tailored.Intro.answerBit hk i a = List.getD (MIPRE.QLD.PauliAnswerProgram.answerBits (MIPRE.SAT.shoupBinField k hk) a) i false

theorem MIPRE.Tailored.Intro.answerBit_add_of {k : ℕ} (hk : 1 ≤ k) {m d : ℕ} [NeZero m] [Algebra (ZMod 2) (SAT.shoupBinField k hk).carrier] {n : ℕ} (a : QLD.Honest.Register (SAT.shoupBinField k hk).carrier m → QLD.Answer (SAT.shoupBinField k hk).carrier m d) (v : QLD.Honest.Register (SAT.shoupBinField k hk).carrier m → Fin n → (SAT.shoupBinField k hk).carrier) (hav : ∀ (h : QLD.Honest.Register (SAT.shoupBinField k hk).carrier m), QLD.PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) (a h) = ((SAT.shoupBinField k hk).vecBits (v h)).flatten) (hv : ∀ (h h' : QLD.Honest.Register (SAT.shoupBinField k hk).carrier m), v (h + h') = v h + v h') (i : ℕ) (h h' : QLD.Honest.Register (SAT.shoupBinField k hk).carrier m) : answerBit hk i (a (h + h')) = (answerBit hk i (a h) ^^ answerBit hk i (a h'))

A bit of an answer whose encoding is that of a vector additive in the outcome is additive.

theorem MIPRE.Tailored.Intro.isXBit_pauliLift_answer {k : ℕ} (hk : 1 ≤ k) {m d : ℕ} [NeZero m] [Algebra (ZMod 2) (SAT.shoupBinField k hk).carrier] {n : ℕ} (W : QLD.Bas) (a : QLD.Honest.Register (SAT.shoupBinField k hk).carrier m → QLD.Answer (SAT.shoupBinField k hk).carrier m d) (v : QLD.Honest.Register (SAT.shoupBinField k hk).carrier m → Fin n → (SAT.shoupBinField k hk).carrier) (hav : ∀ (h : QLD.Honest.Register (SAT.shoupBinField k hk).carrier m), QLD.PauliAnswerProgram.answerBits (SAT.shoupBinField k hk) (a h) = ((SAT.shoupBinField k hk).vecBits (v h)).flatten) (hv : ∀ (h h' : QLD.Honest.Register (SAT.shoupBinField k hk).carrier m), v (h + h') = v h + v h') (i : ℕ) : IsXBit (fibSum (QLD.Honest.pauliLift W) a) (answerBit hk i)

theorem MIPRE.Tailored.Intro.isXBit_answerOp {k : ℕ} (hk : 1 ≤ k) {m d : ℕ} [NeZero m] [Algebra (ZMod 2) (SAT.shoupBinField k hk).carrier] (hm : m ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (q : QLD.Question (SAT.shoupBinField k hk).carrier m) (i : ℕ) : IsXBit (QLD.Honest.answerOp hm q) (answerBit hk i)

Every answer bit of the honest Pauli basis test measurement is a signed permutation.

theorem MIPRE.Tailored.Intro.isZBit_answerOp_pauliZ {k : ℕ} (hk : 1 ≤ k) {m d : ℕ} [NeZero m] [Algebra (ZMod 2) (SAT.shoupBinField k hk).carrier] (hm : m ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (i : ℕ) : IsZBit (QLD.Honest.answerOp hm (QLD.Question.pauli QLD.Bas.Z)) (answerBit hk i)

Every answer bit of the honest (Pauli, Z) measurement is a ±1 diagonal.