The Pauli basis test in a bipartite model

Phase 4 of planning/mipco-track.md. Introspection's soundness uses one fact about the Pauli basis test, its soundness thm:qld, and uses it only through its conclusion: a local isometry into the EPR register and an ancilla, the state carried near |EPR⟩ ⊗ |aux⟩, and each player's Pauli measurements carried near the honest ones. This file states that conclusion for a projective strategy in a bipartite model, as the property QLD.SoundIn ω M of the model, at the error qldErr of thm:qld:

• the ancilla is a bipartite model N on a Hilbert space of Type, with ordered, proper algebras (QLD.AncillaModel), in place of the ancilla spaces H_A, H_B and the state |aux⟩;
• the local isometries are one local isometry of models (BipartiteModel.LocalIsometry) from M into N with the EPR register Anc F m adjoined (BipartiteModel.reg), in place of V_A ⊗ V_B; the players' operators move by its homomorphisms, as X ↦ V_A X V_Aᴴ does;
• the errors are the distance of the transported state to the state of the register model, and each player's summed squared state norms of the transported Pauli measurements minus the honest projectors smulKron 1 (proj (weylOf W) h) (QLD.Extraction);
• the value model ω dominates the POVM strategies of the ancilla model (ValueModel.DominatesPOVM): the strategy introspection extracts lives there, and its value has to count in ω.

thm:qld is SoundIn in every model in which the seeded low individual degree test is sound, in every extension by a unit vector, and whose extensions the value model dominates (QLD.soundIn_of_lidt, MIPRE/Background/QLD/Soundness.lean, Phase 5 of the plan). Its tensor-product instance (QLD.soundIn_tensor) is the one the main theorem uses, through introspection. Its commuting-operator form (QLD.SoundCo: the test is sound in the model of every commuting-operator strategy, with ω_co) is the hypothesis on the Pauli basis test of MIPRE.mipco_eq_core_of_stages, and follows from the seeded test's (QLD.soundCo_of_lidt).

The constants of thm:qld in closed form (exists_qldErr_le) are a fact about the function qldErr alone, so the hypothesis at qldErr gives the introspection compiler's constants in any model.

The ancilla

structure MIPRE.QLD.AncillaModel : Type 1

An ancilla model: a bipartite model on a Hilbert space of Type, with ordered, proper algebras compatible with the scalars (StarModule ℂ, which register measurements need) and a unit state, packed with its algebras.

• 𝒞 : Type

  The algebra represented on the Hilbert space.

• 𝒜 : Type

  The first player's algebra.

• ℬ : Type

  The second player's algebra.

• instRing𝒞 : Ring self.𝒞
• instStarRing𝒞 : StarRing self.𝒞
• instAlgebra𝒞 : Algebra ℂ self.𝒞
• instRing𝒜 : Ring self.𝒜
• instStarRing𝒜 : StarRing self.𝒜
• instAlgebra𝒜 : Algebra ℂ self.𝒜
• instStarModule𝒜 : StarModule ℂ self.𝒜
• instPartialOrder𝒜 : PartialOrder self.𝒜
• instStarOrderedRing𝒜 : StarOrderedRing self.𝒜
• instStarProper𝒜 : StarProper self.𝒜
• instRingℬ : Ring self.ℬ
• instStarRingℬ : StarRing self.ℬ
• instAlgebraℬ : Algebra ℂ self.ℬ
• instStarModuleℬ : StarModule ℂ self.ℬ
• instPartialOrderℬ : PartialOrder self.ℬ
• instStarOrderedRingℬ : StarOrderedRing self.ℬ
• instStarProperℬ : StarProper self.ℬ
• N : BipartiteModel self.𝒞 self.𝒜 self.ℬ

  The model.

• unit : ‖self.N.ψ‖ = 1

  Its state is a unit vector.

@[reducible, inline]

abbrev MIPRE.QLD.AncillaModel.of {𝒞 𝒜 ℬ : Type} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (N : BipartiteModel 𝒞 𝒜 ℬ) (h : ‖N.ψ‖ = 1) : AncillaModel

A bipartite model as an ancilla model: a model on a Hilbert space of Type, with ordered, proper algebras compatible with the scalars, in a unit state.

Equations

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

The conclusion of the Pauli basis test in a model

structure MIPRE.QLD.Extraction {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (M : BipartiteModel 𝒞 𝒜 ℬ) (hm : m ∣ Fintype.card F) (S : M.ProjStrat (qldGame hm)) (δ : ℝ) : Type (max (max (max 1 u_2) u_3) u_4)

The conclusion of the Pauli basis test for a projective strategy S in the model M, at error δ: an ancilla model N and a local isometry of M into N with the EPR register Anc F m adjoined, carrying the state of M within δ of the state of the register model, and carrying each player's coarse (Pauli, W) measurement within δ of the honest projectors on the player's register, in summed squared state norm.

• N : AncillaModel

  The ancilla model.

• Φ : M.LocalIsometry (self.N.N.reg (Anc F m))

  The local isometry into the ancilla model with the EPR register adjoined.

• state_error : ‖self.Φ.W M.ψ - (self.N.N.reg (Anc F m)).ψ‖ ≤ δ

  The transported state is near |EPR⟩ ⊗ ψ_N.

• alice_error (W : Bas) : ∑ h : Anc F m, (self.N.N.reg (Anc F m)).stateSqNorm (self.Φ.ΦA ((POVMIn.map rdPauliVec (S.PA (Question.pauli W))).op h) - smulKron 1 (Weyl.proj (weylOf W) h)) ≤ δ

  The first player's transported Pauli measurements are near the honest ones.

• bob_error (W : Bas) : ∑ h : Anc F m, (self.N.N.reg (Anc F m)).swap.stateSqNorm (self.Φ.ΦB ((POVMIn.map rdPauliVec (S.PB (Question.pauli W))).op h) - smulKron 1 (Weyl.proj (weylOf W) h)) ≤ δ

  The second player's transported Pauli measurements are near the honest ones.

def MIPRE.QLD.Extraction.mono {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {M : BipartiteModel 𝒞 𝒜 ℬ} {hm : m ∣ Fintype.card F} {S : M.ProjStrat (qldGame hm)} {δ δ' : ℝ} (E : Extraction M hm S δ) (h : δ ≤ δ') : Extraction M hm S δ'

Increasing the error bound keeps the extraction.

Equations

• E.mono h = { N := E.N, Φ := E.Φ, state_error := ⋯, alice_error := ⋯, bob_error := ⋯ }

Soundness in a model

def MIPRE.QLD.SoundIn {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (ω : ValueModel) (M : BipartiteModel 𝒞 𝒜 ℬ) : Prop

The Pauli basis test is sound in the bipartite model M (def:qld-sound-in), with the value model ω: for every admissible (q, m, d), a projective strategy in M failing the test with probability at most ε has an extraction at error qldErr ε m d q whose ancilla model ω dominates.

Equations

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

The commuting-operator model

def MIPRE.QLD.SoundCo : Prop

The Pauli basis test is sound in the commuting-operator model (def:qld-sound-in): in the model of every commuting-operator strategy, with ω_co. It is the hypothesis on the Pauli basis test of MIPRE.mipco_eq_core_of_stages, and follows from the soundness of the seeded test in the commuting-operator model (QLD.soundCo_of_lidt, Phase 5 of planning/mipco-track.md).

Equations

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

Values approached in models where the test is sound

def MIPRE.QLD.ApproxSoundIn (ω : ValueModel) : Prop

The value model is approached by projective strategies in models where the Pauli basis test is sound: below the value of a game, and above 0, lies the value of a projective strategy for it in a bipartite model on a Hilbert space of Type in which the test is sound with ω. Introspection applies the test inside the model of such a strategy. val* has it through the tensor-product models of tensor-product strategies (approxSoundIn_tensor, in MIPRE/Background/QLD/Soundness.lean), and ω_co whenever the test is sound in the model of every commuting-operator strategy (approxSoundIn_commuting).

Equations

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

theorem MIPRE.QLD.approxSoundIn_commuting (h : SoundCo) : ApproxSoundIn ValueModel.commuting

ω_co is approached in the models of commuting-operator strategies (exists_projStrat_lt_commutingOperatorValue), where the test is sound if it is sound in every such model.