Oracularization in a value model

The value transfers of oracularization at a normal form verifier — Verifier.valStar_ge_of_typed, and through it Oracularization.typed_soundness and Oracularization.detyped_soundness — use three facts about val* beyond the fields of ValueModel: the game-level soundness of oracularization, the transfer from the typed game to the oracularization by a question-dependent reading of the answers, and the detyping restriction. ValueModel.OracularSound is those three facts, for a value model; the tensor-product and the commuting-operator model have them (ValueModel.tensor_oracularSound, ValueModel.commuting_oracularSound), both from the model-level statements (SeededGame.povmValue_sound_ge, BipartiteModel.povmValue_le_postprocess, CL.Detyping.restrict_povmValue_ge) read in the model of each strategy. The transfers are then written once, in Verifier.val ω (Verifier.val_ge_of_typed, ValueModel.OracularSound.typedGame_ge_ambient, and in Pipeline/Oracularization.lean Oracularization.typed_soundness_val and Oracularization.detyped_soundness_val).

structure MIPRE.ValueModel.OracularSound (ω : ValueModel) : Prop

Oracularization is sound in the value model (def:oracular-sound-in): the three facts the value transfers of oracularization use.

• le_postprocess: reading the answers through maps that may depend on the question, on the same questions and distribution, raises the value when every accepted tuple stays accepted;
• oracular: the game-level soundness of oracularization, ω(oracular) > 1 - ε giving ω ≥ 1 - 24√ε for the input game;
• detype: the finite-game detyping restriction, the typed game's value at least 1 - 16^{|T|}(1 - ω) of the detyped game's.

• le_postprocess {X Y A B A' B' : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A'] [DecidableEq B'] (G : Game X Y A B) (G' : Game X Y A' B') (rA : X → A → A') (rB : Y → B → B') : (∀ (x : X) (y : Y), G'.μ x y = G.μ x y) → (∀ (x : X) (y : Y) (a : A) (b : B), G.D x y a b = true → G'.D x y (rA x a) (rB y b) = true) → ω.val G ≤ ω.val G'
• oracular {V A : Type} [Fintype V] [DecidableEq V] [Nonempty V] [Fintype A] [DecidableEq A] [Inhabited A] (S : SeededGame V A) {ε : ℝ} : 0 < ε → 1 - ε < ω.val S.oracular.toGame → 1 - 24 * √ε ≤ ω.val S.toGame
• detype {T ι A B : Type} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] : (∀ (u v : T), E u v → E v u) → ∀ (hne : (CL.Graph.edges E).Nonempty) (P : Bool → T → CL.CLFun (ZMod 2) ι ℓ), (∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) → 0 < ℓ → ∀ (D : CL.Detyping.Question T ι → CL.Detyping.Question T ι → A → B → Bool), 1 - 16 ^ Fintype.card T * (1 - ω.val (CL.Detyping.game E P D)) ≤ ω.val (CL.Detyping.typedGame E hne P D)

theorem MIPRE.ValueModel.tensor_oracularSound : tensor.OracularSound

Oracularization is sound in the tensor-product model.

theorem MIPRE.ValueModel.commuting_oracularSound : commuting.OracularSound

Oracularization is sound in the commuting-operator model (thm:oracularization-in-model).

theorem MIPRE.ValueModel.OracularSound.typedGame_ge_ambient {ω : ValueModel} (hω : ω.OracularSound) {T : Type} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : CL.TypedSampler ℓ T) (D : CL.Detyping.TypedDecider T) (C : CL.Detyping.CutoffProgram) (hE : ∀ (u v : T), E u v → E v u) (hne : (CL.Graph.edges E).Nonempty) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) : 1 - 16 ^ Fintype.card T * (1 - ω.val ((CL.Detyping.DeciderProgram.verifier E S D C hℓ hD).game n (C.outer n))) ≤ ω.val (CL.Detyping.typedGame E hne (CL.Detyping.DeciderProgram.sourceFamily S n) (CL.Detyping.DeciderProgram.typedPredicate S D C n))

The detyping restriction at the compiled verifier, in a value model: the typed game's value is at least 1 - 16^{|T|}(1 - ω) of the compiled verifier's game at the outer cut, which is the finite detyped game up to the numbering of its coordinates (ValueModel.eq_of_equiv).

theorem MIPRE.SeededGame.val_typedGame_le {ω : ValueModel} (hω : ω.OracularSound) {ι : Type} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type} [Fintype A] [DecidableEq A] (L : Player → CL.CLFun CL.𝔽₂ ι (ℓ + 1)) (D : (ι → CL.𝔽₂) → (ι → CL.𝔽₂) → A → A → Bool) {A' : Type} [Fintype A'] (D' : CL.Detyping.Question Role ι → CL.Detyping.Question Role ι → A' → A' → Bool) (rA : CL.Detyping.Question Role ι → A' → OAns A) (hD : ∀ (p q : CL.Detyping.Question Role ι) (a b : A'), D' p q a b = true → (ofCL L D).oaccepts p q (rA p a) (rA q b) = true) : ω.val (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily L) D') ≤ ω.val (ofCL L D).oracular.toGame

The typed oracularized game has no larger value than the oracularization, in a value model where oracularization is sound: a typed predicate whose acceptance implies the oracularized predicate after a question-dependent reading of the answers, on the same distribution (typedGame_mu). quantumValue_typedGame_le is its tensor-product case.

theorem MIPRE.Verifier.val_ge_of_typed {ℓ : ℕ} (V : Verifier (ℓ + 1)) {ω : ValueModel} (hω : ω.OracularSound) (n B : ℕ) {A' : Type} [Fintype A'] (D' : CL.Detyping.Question Role (Fin (V.sampler.dim n)) → CL.Detyping.Question Role (Fin (V.sampler.dim n)) → A' → A' → Bool) (rA : CL.Detyping.Question Role (Fin (V.sampler.dim n)) → A' → OAns (Answers B)) (hD : ∀ (p q : CL.Detyping.Question Role (Fin (V.sampler.dim n))) (a b : A'), D' p q a b = true → (V.seeded n B).oaccepts p q (rA p a) (rA q b) = true) {ε : ℝ} (hε : 0 < ε) (h : 1 - ε < ω.val (CL.Detyping.typedGame roleGraph roleGraph_nonempty (fun (x : Bool) => roleFamily (V.sampler.cl n)) D')) : 1 - 24 * √ε ≤ V.val ω n B

Soundness of the typed oracularized game, in a value model where oracularization is sound: for a typed predicate whose acceptance implies the oracularized predicate after a reading of the answers, ω of the typed game above 1 - ε puts ω(𝒱_n) at least 1 - 24√ε. valStar_ge_of_typed is its tensor-product case.