Finite introspection soundness from valid-answer Pauli extraction

This is the extraction interface used in the paper: an unsquared state distance and measurement errors summed only over valid full-register answers. Every other raw answer, and the isometric image complement, is accounted for by the proof. The local isometries and their estimates are inputs; existence of those data is the separate Pauli soundness theorem.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the strategy lives in any model M, the local isometries are one local isometry of models into the register model Ξ.reg (ι → F) of a normalized auxiliary model Ξ, and the value is that of any value model dominating the POVM strategies of Ξ. This is the shape of the conclusion of the Pauli basis test in a model (QLD.Extraction).

noncomputable def MIPRE.Introspection.validSoundnessCoefficient (r : ℕ) (edges : ℝ) : ℝ

Equations

• MIPRE.Introspection.validSoundnessCoefficient r edges = 6 * MIPRE.Introspection.extractedSoundnessCoefficient r edges

theorem MIPRE.Introspection.validSoundnessCoefficient_one_le (r : ℕ) {edges : ℝ} (he : 0 ≤ edges) : 1 ≤ validSoundnessCoefficient r edges

theorem MIPRE.Introspection.exists_validSoundness_errorProfile (r : ℕ) {edges a b : ℝ} (hE : 0 ≤ edges) (ha : 0 ≤ a) (hb0 : 0 < b) (hb1 : b ≤ 1) : ∃ (a' : ℝ) (b' : ℝ), 1 ≤ a' ∧ 0 < b' ∧ b' ≤ 1 ∧ ∀ (x ε : ℝ), 1 ≤ x → 0 ≤ ε → validSoundnessCoefficient r edges * iteratedRoot (6 * r + 2) (errorProfile a b x ε) ≤ errorProfile a' b' x ε

The valid-answer interface retains the paper's two-term power profile, with constants uniform in the source and register dimensions.

theorem MIPRE.Introspection.TypedEstimates.quantumValue_ge_of_valid_isometric_images {F ι A : Type} {PauliType : Type u_1} {PauliAnswer : Type u_2} {κ : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [Nonempty A] [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Fintype κ] [DecidableEq κ] {ℓ : ℕ} {𝒞 𝒜 ℬ : Type u} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {𝒞₀ : Type u_4} {𝒜₀ : Type u_5} {ℬ₀ : Type u_6} [Ring 𝒞₀] [StarRing 𝒞₀] [Algebra ℂ 𝒞₀] [Ring 𝒜₀] [StarRing 𝒜₀] [Algebra ℂ 𝒜₀] [Ring ℬ₀] [StarRing ℬ₀] [Algebra ℂ ℬ₀] [PartialOrder 𝒜₀] [StarOrderedRing 𝒜₀] [PartialOrder ℬ₀] [StarOrderedRing ℬ₀] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (projectPauli : PauliAnswer → ι → F) (validPauli : (ι → F) → PauliAnswer) (hvalid : ∀ (x : ι → F), projectPauli (validPauli x) = x) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (ω : ValueModel) (G : Game (ι → F) (ι → F) A A) (hμ : ∀ (x y : ι → F), G.μ x y = CL.clDist (L false).eval (L true).eval x y) (hD : G.D = D) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (hω : ω.DominatesPOVM Ξ) (M : BipartiteModel 𝒞₀ 𝒜₀ ℬ₀) (hM : ‖M.ψ‖ = 1) (Φ : M.LocalIsometry (Ξ.reg (ι → F))) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) 𝒜₀) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ₀) (hMA : ∀ (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MA q).op) (hMB : ∀ (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MB q).op) (qX qZ : κ → ZMod 2) (hqX : ∀ (z : κ → ZMod 2), (P X).eval z = qX) (hqZ : ∀ (z : κ → ZMod 2), (P Z).eval z = qZ) {t : ℝ} (ht : 0 ≤ t) (hstate : ‖Φ.W M.ψ - (Ξ.reg (ι → F)).ψ‖ ≤ t) (hfail : 1 - M.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ t) (hX : ∑ x : ι → F, (Ξ.reg (ι → F)).stateSqNorm (Φ.ΦA ((MA (QuestionType.pauli X, qX)).op (ParsedAnswer.pauli (validPauli x))) - smulKron 1 (Honest.pauliXReadout (some x))) ≤ t) (hZ : ∑ z : ι → F, (Ξ.reg (ι → F)).swap.stateSqNorm (Φ.ΦB ((MB (QuestionType.pauli Z, qZ)).op (ParsedAnswer.pauli (validPauli z))) - smulKron 1 (readout some (some z))) ≤ t) : 1 - validSoundnessCoefficient ℓ ↑(TypeGraph.edges E X Z ℓ).card * iteratedRoot (6 * ℓ + 2) t ≤ ω.val G

Complete finite-game soundness from the valid-answer, unsquared-distance form of Pauli extraction. No zero-malformed-mass assumption is required.