Same-state soundness of finite-game detyping, in a bipartite model

The detyping restriction of MIPRE/Foundations/CL/DetypingSoundness.lean (the finite-game core of lem:detyping-verifiers) uses nothing of a tensor-product strategy but its conditional failures, their nonnegativity and the averaging identity of a sampled game. It is restated here for POVM families in a bipartite model (Phase 2 of planning/mipco-track.md): the families of a strategy for the detyped game, read at the fixed graph views, are a strategy for the typed game in the same model, and it fails at most 16^{|T|} times as often (CL.Detyping.restrict_povmValue_ge). Its readings in the two values — CL.Detyping.quantumValue_typedGame_ge and CL.Detyping.commutingOperatorValue_typedGame_ge — bound the typed game's value below by the detyped game's, through a supremum (one_sub_mul_one_sub_iSup_le).

theorem MIPRE.one_sub_mul_one_sub_iSup_le {ι : Sort u_1} (v : ι → ℝ) {c Q : ℝ} (hc : 1 ≤ c) (hQ : 0 ≤ Q) (h : ∀ (i : ι), 1 - c * (1 - v i) ≤ Q) : 1 - c * (1 - ⨆ (i : ι), v i) ≤ Q

An affine transfer of values survives the supremum. If every value v i gives 1 - c (1 - v i) ≤ Q, with c ≥ 1 and Q ≥ 0, then so does their supremum.

theorem MIPRE.SampledGame.one_sub_povmValue {S : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype S] [Fintype X] [Fintype Y] [Nonempty S] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (qA : S → X) (qB : S → Y) (D : X → Y → A → B → Bool) {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) : 1 - M.povmValue (game qA qB D) MA MB = (∑ s : S, M.condFail (game qA qB D) MA MB (qA s) (qB s)) / ↑(Fintype.card S)

The failure probability of a strategy in a model is the uniform average of its conditional failures — one_sub_value for POVM families in a bipartite model.

theorem MIPRE.CL.Detyping.restrict_condFail_eq {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_6} {B : Type u_7} [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) (MA : (Coord T ι → ZMod 2) → POVMIn A 𝒜) (MB : (Coord T ι → ZMod 2) → POVMIn B ℬ) (x y : Question T ι) (h : E x.1 y.1) : M.condFail (typedGame E hne P D) (fun (x : Question T ι) => MA (question E false x)) (fun (y : Question T ι) => MB (question E true y)) x y = M.condFail (game E P D) MA MB (question E false x) (question E true y)

Conditional failure agrees on every edge: the restricted families, at a typed question pair on an edge, fail exactly as the original ones at the embedded questions.

theorem MIPRE.CL.Detyping.typed_failure_povm {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_6} {B : Type u_7} [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) (MA : Question T ι → POVMIn A 𝒜) (MB : Question T ι → POVMIn B ℬ) : 1 - M.povmValue (typedGame E hne P D) MA MB = (∑ uv ∈ Graph.edges E, ∑ v : ι → ZMod 2, M.condFail (typedGame E hne P D) MA MB (uv.1, (P false uv.1).eval v) (uv.2, (P true uv.2).eval v)) / (↑(Graph.edges E).card * ↑(Fintype.card (ι → ZMod 2)))

The typed failure is the uniform edge-and-content average of the conditional failures.

theorem MIPRE.CL.Detyping.failure_povm {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_6} {B : Type u_7} [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) (MA : (Coord T ι → ZMod 2) → POVMIn A 𝒜) (MB : (Coord T ι → ZMod 2) → POVMIn B ℬ) : 1 - M.povmValue (game E P D) MA MB = (∑ g : Graph.Coord T → ZMod 2, ∑ v : ι → ZMod 2, M.condFail (game E P D) MA MB ((presentation E false (P false)).eval (Sum.elim g v)) ((presentation E true (P true)).eval (Sum.elim g v))) / (16 ^ Fintype.card T * ↑(Fintype.card (ι → ZMod 2)))

The detyped failure is the uniform average over its independent graph and content seeds.

theorem MIPRE.CL.Detyping.restrict_failure_eq_povm {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_6} {B : Type u_7} [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → B → Bool) (MA : (Coord T ι → ZMod 2) → POVMIn A 𝒜) (MB : (Coord T ι → ZMod 2) → POVMIn B ℬ) : (1 - M.povmValue (typedGame E hne P D) (fun (x : Question T ι) => MA (question E false x)) fun (y : Question T ι) => MB (question E true y)) = (∑ g ∈ Graph.validSeeds E, ∑ v : ι → ZMod 2, M.condFail (game E P D) MA MB ((presentation E false (P false)).eval (Sum.elim g v)) ((presentation E true (P true)).eval (Sum.elim g v))) / (↑(Graph.validSeeds E).card * ↑(Fintype.card (ι → ZMod 2)))

The restricted families' failure is the detyped failure conditioned on valid graph seeds.

theorem MIPRE.CL.Detyping.restrict_failure_le_povm {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [StarOrderedRing 𝒜] [StarOrderedRing ℬ] {A : Type u_6} {B : Type u_7} [Fintype A] [Fintype B] {ℓ : ℕ} (hψ : ‖M.ψ‖ = 1) (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → B → Bool) (MA : (Coord T ι → ZMod 2) → POVMIn A 𝒜) (MB : (Coord T ι → ZMod 2) → POVMIn B ℬ) : (1 - M.povmValue (typedGame E hne P D) (fun (x : Question T ι) => MA (question E false x)) fun (y : Question T ι) => MB (question E true y)) ≤ 16 ^ Fintype.card T * (1 - M.povmValue (game E P D) MA MB)

The finite-game detyping reduction, in a bipartite model, with the source's soundness factor 16^{|T|}.

theorem MIPRE.CL.Detyping.restrict_povmValue_ge {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [StarOrderedRing 𝒜] [StarOrderedRing ℬ] {A : Type u_6} {B : Type u_7} [Fintype A] [Fintype B] {ℓ : ℕ} (hψ : ‖M.ψ‖ = 1) (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → B → Bool) (MA : (Coord T ι → ZMod 2) → POVMIn A 𝒜) (MB : (Coord T ι → ZMod 2) → POVMIn B ℬ) {ε : ℝ} (hS : 1 - ε ≤ M.povmValue (game E P D) MA MB) : 1 - 16 ^ Fintype.card T * ε ≤ M.povmValue (typedGame E hne P D) (fun (x : Question T ι) => MA (question E false x)) fun (y : Question T ι) => MB (question E true y)

Same-state soundness of detyping, in a bipartite model (lem:transports-model): families of value at least 1 - ε for the detyped game, read at the fixed graph views, have value at least 1 - 16^{|T|} ε for the typed game, in the same model.

The two values

theorem MIPRE.CL.Detyping.quantumValue_typedGame_ge {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {A : Type u_6} {B : Type u_7} [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → B → Bool) : 1 - 16 ^ Fintype.card T * (1 - quantumValue (game E P D)) ≤ quantumValue (typedGame E hne P D)

Detyping in quantum values: the typed game's val* is at least 1 - 16^{|T|}(1 - val*) of the detyped game's.

theorem MIPRE.CL.Detyping.commutingOperatorValue_typedGame_ge {T ι A B : Type} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → B → Bool) : 1 - 16 ^ Fintype.card T * (1 - commutingOperatorValue (game E P D)) ≤ commutingOperatorValue (typedGame E hne P D)

Detyping in commuting-operator values: the typed game's ω_co is at least 1 - 16^{|T|}(1 - ω_co) of the detyped game's. A commuting-operator strategy for the detyped game is restricted in its own model (restrict_povmValue_ge), and the restriction is a commuting-operator strategy (BipartiteModel.povmValue_le_commutingOperatorValue).