Soundness before replacing the extracted state

The primitive measurement guarantees may hold on the actual extracted state, which is only approximately an EPR register tensored with an auxiliary state. Both the game value and the two complete Pauli families are transferred here, with no answer-cardinality factor. The resulting original-game bound has one additional square root and covers all errors.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the extracted state is a unit vector φ of the register model Ξ.reg (ι → F), near its state, and the strategy and its guarantees live in the register model with that state (BipartiteModel.withState).

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

The coefficient after transferring the extracted state and measurements.

Equations

• MIPRE.Introspection.extractedSoundnessCoefficient r edges = 20 * MIPRE.Introspection.primitiveSoundnessCoefficient r edges

theorem MIPRE.Introspection.extractedSoundnessCoefficient_one_le (r : ℕ) {edges : ℝ} (hE : 0 ≤ edges) : 1 ≤ extractedSoundnessCoefficient r edges

theorem MIPRE.Introspection.extractedSoundness_power_bound (r : ℕ) {edges t : ℝ} (hE : 0 ≤ edges) : primitiveSoundnessCoefficient r edges * iteratedRoot (6 * r) (20 * √t) ≤ extractedSoundnessCoefficient r edges * iteratedRoot (6 * r + 1) t

One additional square root pays for the initial state transfer.

theorem MIPRE.Introspection.exists_extractedSoundness_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 ≤ ε → extractedSoundnessCoefficient r edges * iteratedRoot (6 * r + 1) (errorProfile a b x ε) ≤ errorProfile a' b' x ε

Uniform constants for the profile after state transfer and both inductions.

theorem MIPRE.Introspection.TypedEstimates.quantumValue_ge_of_extracted_state {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 ℬ] (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) (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 Ξ) (φ : (Ξ.reg (ι → F)).H) (hφ : ‖φ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) (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 : ‖φ - (Ξ.reg (ι → F)).ψ‖ ^ 2 ≤ t) (hfail : 1 - ((Ξ.reg (ι → F)).withState φ).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ t) (hX : ∑ x : Option (ι → F), ((Ξ.reg (ι → F)).withState φ).stateSqNorm ((POVMIn.map (pauliProjection projectPauli) (MA (QuestionType.pauli X, qX))).op x - smulKron 1 (Honest.pauliXReadout x)) ≤ t) (hZ : ∑ z : Option (ι → F), ((Ξ.reg (ι → F)).withState φ).swap.stateSqNorm ((POVMIn.map (pauliProjection projectPauli) (MB (QuestionType.pauli Z, qZ))).op z - smulKron 1 (readout some z)) ≤ t) : 1 - extractedSoundnessCoefficient ℓ ↑(TypeGraph.edges E X Z ℓ).card * iteratedRoot (6 * ℓ + 1) t ≤ ω.val G

Original-game soundness from an actual extracted state and its primitive X/Z guarantees. The ideal register-state estimates are conclusions of this proof, rather than hypotheses on the output of QLD extraction.