The low-individual-degree test, moved between models

LIDT.Simul.SoundIn M (MIPRE/Background/LIDT/ModelSoundness.lean) is stated through the Born probabilities of M's projective measurements, so it is a property of the model up to isomorphism (BipartiteModel.Iso): a strategy of M is pushed forward along the isomorphism with its value, the extracted measurements are pulled back along its inverse, and the three inconsistencies are carried over (SoundIn.of_iso). The seeded CL test is symmetric in the players --- the verifier samples an ordered pair of types uniformly, and every subtest is written in both orientations (CL.clGame_μ_swap, CL.clGame_D_swap) --- so soundness passes to the model with the players exchanged (SoundIn.swap).

Three consequences for the models the Pauli basis test builds:

• the test is sound in the tensor-product model of a state on any finite factors (soundIn_tensor_fintype), soundIn_tensor read along a numbering of the factors;
• it is sound in every ancilla extension of a tensor-product model (soundIn_expand_tensor), the extension being the tensor-product model of the expanded vector;
• soundness in every extension of a model gives soundness in every extension of the model with the players exchanged (soundIn_swap_expand, and soundIn_swap_expand_of_norm for extensions by unit vectors).

The symmetry of the seeded CL test

def MIPRE.LIDT.CL.Sample.swapTy {F : Type u_1} {m : ℕ} (sm : Sample F m) : Sample F m

A sample with the two players' types exchanged.

Equations

• sm.swapTy = { tyA := sm.tyB, tyB := sm.tyA, u := sm.u, s := sm.s, v := sm.v }

def MIPRE.LIDT.CL.Sample.swapTyEquiv {F : Type u_1} {m : ℕ} : Sample F m ≃ Sample F m

The exchange of the two players' types, an involution of the samples.

Equations

• MIPRE.LIDT.CL.Sample.swapTyEquiv = { toFun := MIPRE.LIDT.CL.Sample.swapTy, invFun := MIPRE.LIDT.CL.Sample.swapTy, left_inv := ⋯, right_inv := ⋯ }

theorem MIPRE.LIDT.CL.subtests_swap {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) : subtests hm x y a b = subtests hm y x b a

The subtests are symmetric in the players: each is written in both orientations, and agreement is symmetric.

theorem MIPRE.LIDT.CL.accepts_swap {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) : accepts hm x y a b = accepts hm y x b a

The decision predicate is symmetric in the players.

theorem MIPRE.LIDT.CL.clGame_μ_swap {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) : (clGame hm).μ x y = (clGame hm).μ y x

The question distribution is symmetric in the players: exchanging the two types is a bijection of the samples.

theorem MIPRE.LIDT.CL.clGame_D_swap {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) : (clGame hm).D x y a b = (clGame hm).D y x b a

The seeded CL test accepts the exchanged answers to the exchanged questions.

Soundness in a model, up to isomorphism and exchange

theorem MIPRE.LIDT.Simul.tuplePOVMAIn_pushStrat {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {F : Type} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (Φ : M.Iso M') (S : M.ProjStrat (CL.clGame hm)) (y : Point F m) (a : Fin r → F) : (tuplePOVMAIn hm (Φ.pushStrat S) y).op a = Φ.ΦA ((tuplePOVMAIn hm S y).op a)

The first player's point measurements of a pushed-forward strategy are pushed forward.

theorem MIPRE.LIDT.Simul.tuplePOVMBIn_pushStrat {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {F : Type} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (Φ : M.Iso M') (S : M.ProjStrat (CL.clGame hm)) (y : Point F m) (b : Fin r → F) : (tuplePOVMBIn hm (Φ.pushStrat S) y).op b = Φ.ΦB ((tuplePOVMBIn hm S y).op b)

The second player's point measurements of a pushed-forward strategy are pushed forward.

theorem MIPRE.LIDT.Simul.evalTuplePOVMIn_symm_pushA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {F : Type} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} (Φ : M.Iso M') (G : POVMIn (Fin r → LowIndDegPoly) 𝒜') (y : Point F m) (a : Fin r → F) : (evalTuplePOVMIn G y).op a = Φ.ΦA ((evalTuplePOVMIn (Φ.symm.pushA G) y).op a)

The evaluations of a measurement of the first player pulled back along the inverse.

theorem MIPRE.LIDT.Simul.evalTuplePOVMIn_symm_pushB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {F : Type} [Field F] [Fintype F] [DecidableEq F] {m d r : ℕ} (Φ : M.Iso M') (G : POVMIn (Fin r → LowIndDegPoly) ℬ') (y : Point F m) (b : Fin r → F) : (evalTuplePOVMIn G y).op b = Φ.ΦB ((evalTuplePOVMIn (Φ.symm.pushB G) y).op b)

The evaluations of a measurement of the second player pulled back along the inverse.

theorem MIPRE.LIDT.Simul.SoundIn.of_iso {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') (h : SoundIn M') : SoundIn M

Soundness passes along an isomorphism: a strategy of M is pushed forward to M' with its value, the measurements M''s soundness extracts are pulled back along the inverse, and the three inconsistencies are carried over.

theorem MIPRE.LIDT.Simul.SoundIn.iff_of_iso {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.Iso M') : SoundIn M ↔ SoundIn M'

Soundness is invariant under isomorphism.

theorem MIPRE.LIDT.Simul.SoundIn.swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (h : SoundIn M) : SoundIn M.swap

Soundness passes to the model with the players exchanged: the seeded CL test is symmetric in the players (CL.clGame_μ_swap, CL.clGame_D_swap), so a strategy of the exchanged model is one of the model with the same value (BipartiteModel.ProjStrat.value_swap), and the measurements extracted for it serve, exchanged, with the inconsistencies exchanged (BipartiteModel.inconsistency_swap).

Tensor-product models on any finite factors, and their extensions

theorem MIPRE.LIDT.Simul.soundIn_tensor_fintype {dA : Type u_7} {dB : Type u_8} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) : SoundIn (BipartiteModel.tensor ψ)

The seeded CL test is sound in the tensor-product model of a state on any finite factors: soundIn_tensor, along a numbering of the two factors (BipartiteModel.tensorReindexIso).

theorem MIPRE.LIDT.Simul.soundIn_expand_tensor {dA : Type u_7} {dB : Type u_8} {α : Type u_9} {β : Type u_10} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ψ : dA × dB → ℂ) (e : α × β → ℂ) : SoundIn ((BipartiteModel.tensor ψ).expand e)

The seeded CL test is sound in every extension of a tensor-product model: the extension is the tensor-product model of the expanded vector (BipartiteModel.tensorExpandIso).

Extensions of the model with the players exchanged

theorem MIPRE.LIDT.Simul.soundIn_swap_expand {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [StarProper 𝒜] [StarProper ℬ] (h : ∀ {α β : Type} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : Fintype β] [inst_3 : DecidableEq β] (e : α × β → ℂ), SoundIn (M.expand e)) {α β : Type} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) : SoundIn (M.swap.expand e)

Soundness in the extensions of a model gives soundness in the extensions of the model with the players exchanged: the extension of the exchanged model in e is the exchanged extension in e read backwards (BipartiteModel.swapExpandIso).

theorem MIPRE.LIDT.Simul.soundIn_swap_expand_of_norm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} [StarProper 𝒜] [StarProper ℬ] (h : ∀ {α β : Type} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : Fintype β] [inst_3 : DecidableEq β] (e : α × β → ℂ), ‖evec e‖ = 1 → SoundIn (M.expand e)) {α β : Type} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (he : ‖evec e‖ = 1) : SoundIn (M.swap.expand e)

soundIn_swap_expand for the extensions by unit vectors.