Bits controlled by readable data

The honest strategy of the answer-reduced game (slice P4d of planning/aldous-lyons-track.md) data-processes a Z-aligned permutation strategy along maps that are F₂-affine in the linear answer bits, with coefficients read off the readable ones (cor:encodings, II:1150): the oracle's linear codewords are affine in the isolated players' linear answers, with coefficients read off their readable answers. This file supplies the closure lemmas for such bits.

• isSignedPerm_controlledSum: a sum ∑_k E_k W_k over a diagonal projective measurement E, each W_k a signed permutation commuting with E, is a signed permutation. On the basis vectors of outcome k it acts as W_k, which keeps them there.
• isXBit_controlledBy: the bit g_{ρ(a)}(a), controlled by a function ρ of the outcome whose coarse-graining is diagonal, is a signed permutation when each g_k is.
• isZBit_comp_of_isDiag: a function of such a ρ is a Z-bit.
• isDiag_coarse_of_isZBit: the coarse-graining along the bits of the outcome below a readable length is diagonal when those bits are Z-bits, which is how ρ arises.
• isXBit_affine: an F₂-affine function of X-bits is an X-bit, and isXBit_of_controlledAffine, isZBit_of_readable put the pieces together: a bit that is a function of Z-bits is a Z-bit, and a bit that is, for each value of the Z-bits, an affine function of X-bits is an X-bit.
• PermStrategy.toSync_bit: the answer bits of the synchronous strategy of a permutation strategy (lem:zpc-pcc) are X-bits, and Z-bits below the readable length.

Diagonal projective measurements

theorem MIPRE.Tailored.diag_mem_zero_one {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_2} [Fintype K] {E : K → Matrix Ω Ω ℂ} (hE : IsPVMIn E) (hd : ∀ (k : K), (E k).IsDiag) (k : K) (i : Ω) : E k i i = 0 ∨ E k i i = 1

theorem MIPRE.Tailored.diag_sum_eq_one {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_2} [Fintype K] {E : K → Matrix Ω Ω ℂ} (hE : IsPVMIn E) (i : Ω) : ∑ k : K, E k i i = 1

theorem MIPRE.Tailored.diag_mul_diag_eq_zero {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_2} [Fintype K] {E : K → Matrix Ω Ω ℂ} (hE : IsPVMIn E) (hd : ∀ (k : K), (E k).IsDiag) {j k : K} (hjk : j ≠ k) (i : Ω) : E j i i * E k i i = 0

theorem MIPRE.Tailored.existsUnique_diag_eq_one {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_2} [Fintype K] {E : K → Matrix Ω Ω ℂ} (hE : IsPVMIn E) (hd : ∀ (k : K), (E k).IsDiag) (i : Ω) : ∃! k : K, E k i i = 1

A diagonal projective measurement puts each basis vector in exactly one outcome.

noncomputable def MIPRE.Tailored.diagOutcome {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_2} [Fintype K] {E : K → Matrix Ω Ω ℂ} (hE : IsPVMIn E) (hd : ∀ (k : K), (E k).IsDiag) (i : Ω) : K

The outcome of a basis vector.

Equations

• MIPRE.Tailored.diagOutcome hE hd i = ⋯.choose

theorem MIPRE.Tailored.diag_diagOutcome {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_2} [Fintype K] {E : K → Matrix Ω Ω ℂ} (hE : IsPVMIn E) (hd : ∀ (k : K), (E k).IsDiag) (i : Ω) : E (diagOutcome hE hd i) i i = 1

theorem MIPRE.Tailored.diag_eq_ite {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_2} [Fintype K] {E : K → Matrix Ω Ω ℂ} [DecidableEq K] (hE : IsPVMIn E) (hd : ∀ (k : K), (E k).IsDiag) (k : K) (i : Ω) : E k i i = if k = diagOutcome hE hd i then 1 else 0

theorem MIPRE.Tailored.diagOutcome_perm {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_2} [Fintype K] {E : K → Matrix Ω Ω ℂ} (hE : IsPVMIn E) (hd : ∀ (k : K), (E k).IsDiag) (σ : Equiv.Perm Ω) (s : Ω → Bool) (hc : ∀ (j : K), E j * signedPermMatrix σ s = signedPermMatrix σ s * E j) (l : Ω) : diagOutcome hE hd (σ l) = diagOutcome hE hd l

A signed permutation commuting with a diagonal projective measurement keeps the outcome of every basis vector.

theorem MIPRE.Tailored.isSignedPerm_controlledSum {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_2} [Fintype K] {E : K → Matrix Ω Ω ℂ} (hE : IsPVMIn E) (hd : ∀ (k : K), (E k).IsDiag) (W : K → Matrix Ω Ω ℂ) (hW : ∀ (k : K), IsSignedPerm (W k)) (hc : ∀ (j k : K), E j * W k = W k * E j) : IsSignedPerm (∑ k : K, E k * W k)

A controlled signed permutation: ∑_k E_k W_k, over a diagonal projective measurement E and signed permutations W_k commuting with it, is a signed permutation.

Controlled bits

theorem MIPRE.Tailored.isDiag_finsetSum {Ω : Type u_1} {ι : Type u_2} (s : Finset ι) {A : ι → Matrix Ω Ω ℂ} (h : ∀ (i : ι), (A i).IsDiag) : (∑ i ∈ s, A i).IsDiag

A sum of diagonal matrices is diagonal.

noncomputable def MIPRE.Tailored.coarseAlong {Ω : Type u_1} {Λ : Type u_2} [Fintype Λ] {K : Type u_3} [DecidableEq K] (P : Λ → Matrix Ω Ω ℂ) (ρ : Λ → K) (k : K) : Matrix Ω Ω ℂ

The coarse-graining of P along ρ.

Equations

• MIPRE.Tailored.coarseAlong P ρ k = ∑ a : Λ with ρ a = k, P a

theorem MIPRE.Tailored.coarseAlong_mul_bitObs {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_2} [Fintype Λ] {K : Type u_3} [DecidableEq K] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) (ρ : Λ → K) (k : K) (g : Λ → Bool) : coarseAlong P ρ k * bitObs P g = ∑ a : Λ with ρ a = k, bitSign (g a) • P a

theorem MIPRE.Tailored.bitObs_controlled {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_2} [Fintype Λ] {K : Type u_3} [Fintype K] [DecidableEq K] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) (ρ : Λ → K) (g : K → Λ → Bool) : (bitObs P fun (a : Λ) => g (ρ a) a) = ∑ k : K, coarseAlong P ρ k * bitObs P (g k)

A bit observable controlled by ρ is the controlled sum of the bit observables.

theorem MIPRE.Tailored.commute_coarseAlong_bitObs {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_2} [Fintype Λ] {K : Type u_3} [DecidableEq K] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) (ρ : Λ → K) (k : K) (g : Λ → Bool) : coarseAlong P ρ k * bitObs P g = bitObs P g * coarseAlong P ρ k

theorem MIPRE.Tailored.isXBit_controlledBy {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_2} [Fintype Λ] {K : Type u_3} [Fintype K] [DecidableEq K] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) (ρ : Λ → K) (hd : ∀ (k : K), (coarseAlong P ρ k).IsDiag) (g : K → Λ → Bool) (hg : ∀ (k : K), IsXBit P (g k)) : IsXBit P fun (a : Λ) => g (ρ a) a

A bit controlled by readable data: if the coarse-graining of P along ρ is diagonal, the bit g_{ρ(a)}(a) is a signed permutation when each g_k is.

theorem MIPRE.Tailored.isZBit_comp_of_isDiag {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_2} [Fintype Λ] {K : Type u_3} [Fintype K] [DecidableEq K] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) (ρ : Λ → K) (hd : ∀ (k : K), (coarseAlong P ρ k).IsDiag) (f : K → Bool) : IsZBit P (f ∘ ρ)

A function of readable data is a Z-bit.

theorem MIPRE.Tailored.isDiag_coarse_of_isZBit {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_2} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) {r : ℕ} (bits : Λ → Fin r → Bool) (hZ : ∀ (i : Fin r), IsZBit P fun (a : Λ) => bits a i) (v : Fin r → Bool) : (coarseAlong P bits v).IsDiag

Readable bits give a diagonal coarse-graining: if the bits of the outcome below r are Z-bits, the coarse-graining along those bits is diagonal.

Affine bits

def MIPRE.Tailored.IsAffine2 {ι : Type u_2} (h : (ι → ZMod 2) → ZMod 2) : Prop

An F₂-affine function on F₂^ι: h (u + v) + h 0 = h u + h v.

Equations

• MIPRE.Tailored.IsAffine2 h = ∀ (u v : ι → ZMod 2), h (u + v) + h 0 = h u + h v

theorem MIPRE.Tailored.two_eq_zero_zmod2 (x : ZMod 2) : x + x = 0

theorem MIPRE.Tailored.IsAffine2.eq_sum {ι : Type u_2} [Fintype ι] [DecidableEq ι] {h : (ι → ZMod 2) → ZMod 2} (hh : IsAffine2 h) (v : ι → ZMod 2) : h v = h 0 + ∑ m : ι, (h (Pi.single m 1) + h 0) * v m

An affine function is its value at 0 plus a linear form.

theorem MIPRE.Tailored.decide_add_eq_one (x y : ZMod 2) : decide (x + y = 1) = (decide (x = 1) ^^ decide (y = 1))

theorem MIPRE.Tailored.decide_mul_ofBool_eq_one (c : ZMod 2) (b : Bool) : decide (c * LowDegree.ofBool b = 1) = (decide (c = 1) && b)

theorem MIPRE.Tailored.isXBit_affine {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_2} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) {ι : Type u_3} [Fintype ι] [DecidableEq ι] (ν : Λ → ι → Bool) (hν : ∀ (m : ι), IsXBit P fun (a : Λ) => ν a m) {h : (ι → ZMod 2) → ZMod 2} (hh : IsAffine2 h) : IsXBit P fun (a : Λ) => decide ((h fun (m : ι) => LowDegree.ofBool (ν a m)) = 1)

An F₂-affine function of X-bits is an X-bit.

theorem MIPRE.Tailored.isXBit_of_controlledAffine {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_2} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) {R : ℕ} (ρ : Λ → Fin R → Bool) (hρ : ∀ (i : Fin R), IsZBit P fun (a : Λ) => ρ a i) {ι : Type u_3} [Fintype ι] [DecidableEq ι] (ν : Λ → ι → Bool) (hν : ∀ (m : ι), IsXBit P fun (a : Λ) => ν a m) (h : (Fin R → Bool) → (ι → ZMod 2) → ZMod 2) (hh : ∀ (k : Fin R → Bool), IsAffine2 (h k)) (f : Λ → Bool) (hf : ∀ (a : Λ), P a ≠ 0 → LowDegree.ofBool (f a) = h (ρ a) fun (m : ι) => LowDegree.ofBool (ν a m)) : IsXBit P f

A bit that is, for each value of some Z-bits, an affine function of X-bits is an X-bit.

theorem MIPRE.Tailored.isZBit_of_readable {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_2} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) {R : ℕ} (ρ : Λ → Fin R → Bool) (hρ : ∀ (i : Fin R), IsZBit P fun (a : Λ) => ρ a i) (φ : (Fin R → Bool) → Bool) (f : Λ → Bool) (hf : ∀ (a : Λ), P a ≠ 0 → f a = φ (ρ a)) : IsZBit P f

A bit that is a function of some Z-bits is a Z-bit.

The answer bits of the synchronous strategy of a permutation strategy

theorem MIPRE.Tailored.PermStrategy.toSync_len {X : Type u_2} [Fintype X] {G : TailoredGame X} (S : PermStrategy G.doubled) (p : Bool × X) (a : Verifier.Answers G.maxLen) (ha : S.toSync.P.M p a ≠ 0) : List.length ↑a = G.len p.2

The synchronous strategy charges only answers of the game's lengths.

theorem MIPRE.Tailored.PermStrategy.toSync_bit {X : Type u_2} [Fintype X] {G : TailoredGame X} (S : PermStrategy G.doubled) (p : Bool × X) (j : ℕ) : (IsXBit (S.toSync.P.M p) fun (a : Verifier.Answers G.maxLen) => List.getD (↑a) j false) ∧ (j < G.lenR p.2 → IsZBit (S.toSync.P.M p) fun (a : Verifier.Answers G.maxLen) => List.getD (↑a) j false)

The answer bits of the synchronous strategy are X-bits, and Z-bits below the readable length.