Finite-game introspection soundness from primitive Pauli estimates

The only operator estimates assumed here are the extracted Alice-X and Bob-Z guarantees. Actual game success supplies all hiding estimates and Alice-Z consistency. Both adaptive inductions and terminal extraction are then constructed. The explicit power bound covers every nonnegative input error, including errors outside the smallness threshold of the induction.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the extracted register state is the register model Ξ.reg (ι → F) of a normalized auxiliary model Ξ, and the value is that of any value model ω dominating the POVM strategies of Ξ. The strategy terminal extraction builds lives in the model the two iterations return, which reduces to Ξ (BipartiteModel.POVMReduces), so ω dominates it too.

def MIPRE.Introspection.primitiveBudgetCoefficient (r : ℕ) (edges : ℝ) : ℝ

A common budget for game failure, both Z estimates, and both hiding estimates, depending only on the fixed depth and type-graph size.

Equations

• MIPRE.Introspection.primitiveBudgetCoefficient r edges = 3 + 8 * edges + 2 * MIPRE.Introspection.TypedEstimates.hidingPauliBudget r edges 1 1

theorem MIPRE.Introspection.primitiveBudgetCoefficient_bounds (r : ℕ) {edges : ℝ} (hE : 0 ≤ edges) : 1 ≤ primitiveBudgetCoefficient r edges ∧ 4 * edges + 2 ≤ primitiveBudgetCoefficient r edges ∧ TypedEstimates.hidingPauliBudget r edges 1 1 ≤ primitiveBudgetCoefficient r edges ∧ 4 * edges + 2 * TypedEstimates.hidingPauliBudget r edges 1 1 ≤ primitiveBudgetCoefficient r edges

theorem MIPRE.Introspection.hidingPauliBudget_common (r : ℕ) (edges t : ℝ) : TypedEstimates.hidingPauliBudget r (edges * t) t t = TypedEstimates.hidingPauliBudget r edges 1 1 * t

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

This coefficient includes terminal edge loss and the trivial large-error regime, so no smallness premise remains in the soundness conclusion.

Equations

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

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

theorem MIPRE.Introspection.primitiveSoundness_power_bounds (r : ℕ) {edges t : ℝ} (hE : 0 ≤ edges) (ht : 0 ≤ t) : have p := adaptiveSoundnessCoefficient r edges (2 * r) * iteratedRoot (3 * (2 * r)) (primitiveBudgetCoefficient r edges * t); p ≤ primitiveSoundnessCoefficient r edges * iteratedRoot (6 * r) t ∧ edges * p ≤ primitiveSoundnessCoefficient r edges * iteratedRoot (6 * r) t

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

The finite-game soundness loss has the paper's two-term error profile, with constants uniform in the source game and the register dimension.

theorem MIPRE.Introspection.TypedEstimates.quantumValue_ge_of_primitive_pauli {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 Ξ) (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) (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ t) (hX : ∑ x : Option (ι → F), (Ξ.reg (ι → F)).stateSqNorm ((POVMIn.map (pauliProjection projectPauli) (MA (QuestionType.pauli X, qX))).op x - smulKron 1 (Honest.pauliXReadout x)) ≤ t) (hZ : introBobZError projectPauli Z qZ Ξ MB ≤ t) : 1 - primitiveSoundnessCoefficient ℓ ↑(TypeGraph.edges E X Z ℓ).card * iteratedRoot (6 * ℓ) t ≤ ω.val G

Complete finite-game soundness on an extracted register model, in every value model dominating its POVM strategies. No hiding, prefix invariant, future measurement, or small-error hypothesis is assumed.

theorem MIPRE.Introspection.TypedEstimates.quantumValue_ge_of_primitive_profile {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 Ξ) (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) {a b x ε : ℝ} (ha : 0 ≤ a) (hx : 1 ≤ x) (hε : 0 ≤ ε) (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ errorProfile a b x ε) (hX : ∑ z : Option (ι → F), (Ξ.reg (ι → F)).stateSqNorm ((POVMIn.map (pauliProjection projectPauli) (MA (QuestionType.pauli X, qX))).op z - smulKron 1 (Honest.pauliXReadout z)) ≤ errorProfile a b x ε) (hZ : introBobZError projectPauli Z qZ Ξ MB ≤ errorProfile a b x ε) : 1 - errorProfile (powerCoefficient (primitiveSoundnessCoefficient ℓ ↑(TypeGraph.edges E X Z ℓ).card) a (rootExponent (6 * ℓ))) (b * rootExponent (6 * ℓ)) x ε ≤ ω.val G

The composed soundness theorem in the original two-term profile. Its exponent and coefficient depend only on depth, graph size, and the primitive QLD profile constants.