Source-game soundness from the restricted QLD strategy

The extraction inputs refer to the actual restricted QLD strategy, with scalar completion of malformed answers. The full-register answers retain their original operators, so the checked finite-game soundness theorem applies without a malformed-mass hypothesis.

The isometry codomains and ideal projectors here use binary coordinates under Weyl.binEquiv b. Thus the witness interface explicitly records the coordinate convention expected after the field-to-binary Pauli equivalence.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the strategy is a projective strategy of any model M, and the extraction is the conclusion of the Pauli basis test in a model (QLD.Extraction) read at the genuine full-register answers in binary coordinates: an ancilla model N and a local isometry of M into N with the binary register adjoined. The value is that of any value model dominating the POVM strategies of N.

noncomputable def MIPRE.Introspection.RestrictedSoundness.validAnswer {F : Type} [Field F] [Algebra (ZMod 2) F] {m t d : ℕ} (b : Module.Basis (Fin t) (ZMod 2) F) (x : BinaryComplete.Seed m t) : QLD.Answer F m d

Interpret a full binary register answer as the genuine QLD Pauli answer.

Equations

• MIPRE.Introspection.RestrictedSoundness.validAnswer b x = MIPRE.QLD.Answer.pauliAns ((MIPRE.Weyl.binEquiv b).symm x)

theorem MIPRE.Introspection.RestrictedSoundness.project_validAnswer {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t d : ℕ} [NeZero m] (b : Module.Basis (Fin t) (ZMod 2) F) (x : BinaryComplete.Seed m t) : BinaryComplete.project b (validAnswer b x) = x

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

The conclusion of the Pauli basis test for an actual QLD strategy, in binary coordinates: an ancilla model and a local isometry into it with the binary register adjoined, the state within δ of the register state, and the valid-answer X and Z effects within δ of the honest readouts in summed squared state norm.

• N : QLD.AncillaModel

  The ancilla model.

• Φ : M.LocalIsometry (self.N.N.reg (BinaryComplete.Seed m t))

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

• state_error : ‖self.Φ.W M.ψ - (self.N.N.reg (BinaryComplete.Seed m t)).ψ‖ ≤ δ
• X_error : ∑ x : BinaryComplete.Seed m t, (self.N.N.reg (BinaryComplete.Seed m t)).stateSqNorm (self.Φ.ΦA ((R.PA (QLD.Question.pauli QLD.Bas.X)).op (validAnswer b x)) - smulKron 1 (Honest.pauliXReadout (some x))) ≤ δ
• Z_error : ∑ z : BinaryComplete.Seed m t, (self.N.N.reg (BinaryComplete.Seed m t)).swap.stateSqNorm (self.Φ.ΦB ((R.PB (QLD.Question.pauli QLD.Bas.Z)).op (validAnswer b z)) - smulKron 1 (readout some (some z))) ≤ δ

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.RestrictedSoundness.restriction {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t d ℓ : ℕ} [NeZero m] {A : Type} [Fintype A] {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun (ZMod 2) (BinaryComplete.Coord m t) ℓ) (D : BinaryComplete.Seed m t → BinaryComplete.Seed m t → A → A → Bool) {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (PauliRestriction.fullGame hm b L (BinaryComplete.project b) D)) : M.ProjStrat (QLD.qldGame hm)

The extraction theorem is applied to this precise QLD strategy.

Equations

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

theorem MIPRE.Introspection.RestrictedSoundness.quantumValue_ge_of_extraction {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t d ℓ : ℕ} [NeZero m] {A : Type} [Fintype A] [Nonempty A] {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun (ZMod 2) (BinaryComplete.Coord m t) ℓ) (D : BinaryComplete.Seed m t → BinaryComplete.Seed m t → A → A → Bool) {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (PauliRestriction.fullGame hm b L (BinaryComplete.project b) D)) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (ω : ValueModel) {ε δ : ℝ} (hδ : 0 ≤ δ) (hfail : 1 - S.value ≤ ε) (E : Extraction M hm b (restriction hm b L D S) δ) (hω : ω.DominatesPOVM E.N.N) : 1 - validSoundnessCoefficient ℓ ↑(TypeGraph.edges QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) ℓ).card * iteratedRoot (6 * ℓ + 2) (max ε δ) ≤ ω.val (Honest.sourceGame L D)

Concrete valid-answer extraction estimates imply source-game soundness, in every value model dominating the ancilla model. The common error is the maximum of full-game failure and extraction error.