Auxiliary estimates for the concrete typed introspection game

The uniform ordered-edge law supplies the selection probability. The parsed sampling predicate supplies the accepted-answer relation, including malformed constructors, so its estimate has no abstract subtest or probability premise. The Pauli predicate is passed the actual question contents; constructing that predicate, and compiling the byte parser, remain separate obligations.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md).

theorem MIPRE.Introspection.TypedEstimates.aux_agreement_estimate {PauliType : Type u_1} {κ : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] [Fintype B] [Fintype C] [DecidableEq C] {ℓ : ℕ} {𝒞 : Type u_9} {𝒜 : Type u_10} {ℬ : Type u_11} [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) (D : CL.Detyping.Question (QuestionType PauliType ℓ) κ → CL.Detyping.Question (QuestionType PauliType ℓ) κ → A → B → Bool) (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (hΨ : ‖Ψ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn A 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn B ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue (TypedPresentation.game E X Z ℓ P D) MA MB ≤ ε) (t u : AuxType ℓ) (w w' : Bool) (hedge : TypeGraph.Adj E X Z (Sum.inr (t, w)) (Sum.inr (u, w'))) (f : A → C) (g : B → C) (hcheck : ∀ (a : A) (b : B), D (Sum.inr (t, w), 0) (Sum.inr (u, w'), 0) a b = true → f a = g b) : ∑ z : C, Ψ.xSqNorm ((POVMIn.map f (MA (Sum.inr (t, w), 0))).op z) ((POVMIn.map g (MB (Sum.inr (u, w'), 0))).op z) ≤ 2 * ↑(TypeGraph.edges E X Z ℓ).card * ε

On any auxiliary edge, the coarsened cross-party distance costs exactly twice the ordered-edge count times the game's failure.

noncomputable def MIPRE.Introspection.TypedEstimates.questionCheck {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} {ℓ : ℕ} [Field F] [Fintype ι] [DecidableEq ι] (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (q r : CL.Detyping.Question (QuestionType PauliType ℓ) κ) : ParsedAnswer (ι → F) A PauliAnswer → ParsedAnswer (ι → F) A PauliAnswer → Bool

Lift the parsed checks to actual typed questions. Only the Pauli test reads their contents; the auxiliary tests depend on the type labels and answers.

Equations

• MIPRE.Introspection.TypedEstimates.questionCheck L X Z projectPauli D DP q r = MIPRE.Introspection.TypedPredicate.check L X Z projectPauli D (fun (p s : PauliType) => DP p s q.2 r.2) q.1 r.1

noncomputable def MIPRE.Introspection.TypedEstimates.parsedGame {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} [Field F] [Fintype F] [Fintype ι] [DecidableEq ι] [Fintype PauliAnswer] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) : Game (CL.Detyping.Question (QuestionType PauliType ℓ) κ) (CL.Detyping.Question (QuestionType PauliType ℓ) κ) (ParsedAnswer (ι → F) A PauliAnswer) (ParsedAnswer (ι → F) A PauliAnswer)

The concrete typed game with the parsed introspection decision predicate.

Equations

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

def MIPRE.Introspection.TypedEstimates.introspectPrefix {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} {ℓ : ℕ} [Field F] [Fintype ι] [DecidableEq ι] (L : CL.CLFun F ι ℓ) (k : ℕ) : ParsedAnswer (ι → F) A PauliAnswer → Option ((ι → F) × A)

Coarsen an introspection answer, retaining a distinct outcome for malformed answers.

Equations

• MIPRE.Introspection.TypedEstimates.introspectPrefix L k (MIPRE.Introspection.ParsedAnswer.pair y a) = some (L.outputPrefix k y, a)
• MIPRE.Introspection.TypedEstimates.introspectPrefix L k x✝ = none

def MIPRE.Introspection.TypedEstimates.samplePrefix {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} {ℓ : ℕ} [Field F] [Fintype ι] [DecidableEq ι] (L : CL.CLFun F ι ℓ) (k : ℕ) : ParsedAnswer (ι → F) A PauliAnswer → Option ((ι → F) × A)

Coarsen a sampling answer by evaluating the original CL prefix on its sampled seed.

Equations

• MIPRE.Introspection.TypedEstimates.samplePrefix L k (MIPRE.Introspection.ParsedAnswer.pair y a) = some ((MIPRE.CL.CLFun.truncate k L).eval y, a)
• MIPRE.Introspection.TypedEstimates.samplePrefix L k x✝ = none

theorem MIPRE.Introspection.TypedEstimates.sampling_prefix_estimate {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_9} {𝒜 : Type u_10} {ℬ : Type u_11} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype PauliAnswer] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (hΨ : ‖Ψ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (k : ℕ) : ∑ z : Option ((ι → F) × A), Ψ.xSqNorm ((POVMIn.map (introspectPrefix (L w) k) (MA (QuestionType.introspect w, 0))).op z) ((POVMIn.map (samplePrefix (L w) k) (MB (QuestionType.sample w, 0))).op z) ≤ 2 * ↑(TypeGraph.edges E X Z ℓ).card * ε

Every prefix of the actual parsed sampling test has cross-party error at most 2 |E| ε, summed over the complete alphabet, including the malformed-answer outcome.

def MIPRE.Introspection.TypedEstimates.hidingReadout {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} {ℓ : ℕ} [Field F] [Fintype ι] [DecidableEq ι] (L : CL.CLFun F ι ℓ) : ParsedAnswer (ι → F) A PauliAnswer → Option ((ι → F) × (ι → F))

The last hiding answer, retaining exactly the data tested against Read.

Equations

• MIPRE.Introspection.TypedEstimates.hidingReadout L (MIPRE.Introspection.ParsedAnswer.hide y yp x_1) = some (L.outputPrefix (ℓ - 1) y, yp)
• MIPRE.Introspection.TypedEstimates.hidingReadout L x✝ = none

def MIPRE.Introspection.TypedEstimates.readingReadout {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} {ℓ : ℕ} [Field F] [Fintype ι] [DecidableEq ι] (L : CL.CLFun F ι ℓ) : ParsedAnswer (ι → F) A PauliAnswer → Option ((ι → F) × (ι → F))

The same tested data from a Read answer.

Equations

• MIPRE.Introspection.TypedEstimates.readingReadout L (MIPRE.Introspection.ParsedAnswer.read y yp a) = some (L.outputPrefix (ℓ - 1) y, yp)
• MIPRE.Introspection.TypedEstimates.readingReadout L x✝ = none

theorem MIPRE.Introspection.TypedEstimates.hiding_read_estimate {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_9} {𝒜 : Type u_10} {ℬ : Type u_11} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype PauliAnswer] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (hΨ : ‖Ψ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (k : Fin ℓ) (hk : ↑k + 1 = ℓ) : ∑ z : Option ((ι → F) × (ι → F)), Ψ.xSqNorm ((POVMIn.map (hidingReadout (L w)) (MA (QuestionType.hide w k, 0))).op z) ((POVMIn.map (readingReadout (L w)) (MB (QuestionType.read w, 0))).op z) ≤ 2 * ↑(TypeGraph.edges E X Z ℓ).card * ε

The concrete last-hiding/Read test bounds the tested coarse measurements, without a separate accepted-answer or selection-probability assumption.

theorem MIPRE.Introspection.TypedEstimates.hiding_read_same_side_estimate {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_9} {𝒜 : Type u_10} {ℬ : Type u_11} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype PauliAnswer] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (hΨ : ‖Ψ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (k : Fin ℓ) (hk : ↑k + 1 = ℓ) : ∑ z : Option ((ι → F) × (ι → F)), Ψ.stateSqNorm ((POVMIn.map (hidingReadout (L w)) (MA (QuestionType.hide w k, 0))).op z - (POVMIn.map (readingReadout (L w)) (MA (QuestionType.read w, 0))).op z) ≤ 8 * ↑(TypeGraph.edges E X Z ℓ).card * ε

The terminal hiding test and Read consistency loop give a same-party estimate with loss 8 |E| ε, after coarse-graining the actual accepted-answer relations.