Removing padding from arbitrary source-game strategies

Canonical zero-extension of questions pulls every padded strategy back, in its own model, with exactly its value. The unused seed coordinates average out uniformly; this is not restricted to perfect strategies or PCC strategies.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): a projective strategy (BipartiteModel.ProjStrat) of the padded source game in a model, asked the zero-extension of each original question (ProjStrat.restrict), is a projective strategy of the original source game in the same model, of the same value (restrictStrategy, restrictStrategy_value, exists_projStrat_value_ge); the state and the dimensions of the matrix statement are the model itself. The value comparisons quantumValue_le and quantumValue_depthFamily_le hold in every value model approached by the projective strategies of the models it dominates (ValueModel.ProjApprox), which val* and ω_co are (ValueModel.tensor_projApprox, ValueModel.commuting_projApprox); the matrix statements are their instances at ValueModel.tensor.

def MIPRE.ValueModel.ProjApprox (ω : ValueModel) : Prop

The value model is approached by the projective strategies of the models it dominates: below the value of a game, and above 0, lies the value of a projective strategy for it in a bipartite model, on a Hilbert space of Type, that ω dominates. With ValueModel.Dominates, ω.val G is then the supremum of the values of these strategies, so two games whose projective strategies compare model by model have comparable values (SourcePadding.quantumValue_le). val* has it through the tensor-product models of tensor-product strategies (tensor_projApprox), ω_co through the models of commuting-operator strategies (commuting_projApprox).

Equations

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

theorem MIPRE.ValueModel.tensor_projApprox : tensor.ProjApprox

val* is approached by the projective strategies of the models it dominates: a tensor-product strategy near the supremum is a projective strategy of its tensor-product model, of the same value (TensorProductStrategy.toModel), and val* dominates that model (tensor_dominates).

theorem MIPRE.ValueModel.commuting_projApprox : commuting.ProjApprox

ω_co is approached by the projective strategies of the models it dominates: those of the models of commuting-operator strategies (exists_projStrat_lt_commutingOperatorValue), which ω_co dominates (commuting_dominates).

noncomputable def MIPRE.Introspection.SourcePadding.seedSplit {F : Type u_1} {I : Type u_2} {J : Type u_3} [Fintype I] [DecidableEq J] (e : I ↪ J) : (J → F) ≃ (I → F) × ({ j : J // j ∉ Set.range ⇑e } → F)

Equations

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

theorem MIPRE.Introspection.SourcePadding.average_pull {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ↪ J) (f : (I → F) → ℝ) : (∑ x : J → F, f (CL.pull e x)) / ↑(Fintype.card (J → F)) = (∑ y : I → F, f y) / ↑(Fintype.card (I → F))

Restricting a uniform seed to an injected set of coordinates is uniform.

noncomputable def MIPRE.Introspection.SourcePadding.restrictStrategy {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} [Field F] [Fintype F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {Ψ : BipartiteModel 𝒞 𝒜 ℬ} (S : Ψ.ProjStrat (Honest.sourceGame (family e L) (decider e D))) : Ψ.ProjStrat (Honest.sourceGame L D)

Ask the padded strategy the canonical extension of the original question, in the same model.

Equations

• MIPRE.Introspection.SourcePadding.restrictStrategy e L D S = S.restrict (MIPRE.Introspection.Honest.sourceGame L D) (MIPRE.CL.push e) (MIPRE.CL.push e)

theorem MIPRE.Introspection.SourcePadding.restrictStrategy_succAt {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ψ : BipartiteModel 𝒞 𝒜 ℬ} (S : Ψ.ProjStrat (Honest.sourceGame (family e L) (decider e D))) (x y : I → F) : Ψ.condWin (Honest.sourceGame L D) (restrictStrategy e L D S).PA (restrictStrategy e L D S).PB x y = Ψ.condWin (Honest.sourceGame (family e L) (decider e D)) S.PA S.PB (CL.push e x) (CL.push e y)

At an original question pair, the restricted strategy wins exactly as the padded strategy does at the extended pair: the padded decider reads the original questions back.

theorem MIPRE.Introspection.SourcePadding.restrictStrategy_value {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ψ : BipartiteModel 𝒞 𝒜 ℬ} (S : Ψ.ProjStrat (Honest.sourceGame (family e L) (decider e D))) : (restrictStrategy e L D S).value = S.value

Restriction keeps the value: the padded seed's unused coordinates average out (average_pull).

theorem MIPRE.Introspection.SourcePadding.exists_projStrat_value_ge {F : Type u_1} {I : Type u_2} {J : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ψ : BipartiteModel 𝒞 𝒜 ℬ} (S : Ψ.ProjStrat (Honest.sourceGame (family e L) (decider e D))) : ∃ (R : Ψ.ProjStrat (Honest.sourceGame L D)), S.value ≤ R.value

Every padded strategy restricts without loss, in its own model: the model form of quantumValue_le.

theorem MIPRE.Introspection.SourcePadding.quantumValue_le {F I J A : Type} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) {ω : ValueModel} (hω : ω.ProjApprox) : ω.val (Honest.sourceGame (family e L) (decider e D)) ≤ ω.val (Honest.sourceGame L D)

Soundness can return from the padded source game to the original game without losing any value, in every value model approached by the projective strategies of the models it dominates: each of those strategies restricts, in its model, to one of the original game of the same value (restrictStrategy_value).

theorem MIPRE.Introspection.SourcePadding.quantumValue_depthFamily_le {F I J A : Type} [Field F] [Fintype F] [DecidableEq F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (D : (I → F) → (I → F) → A → A → Bool) {ω : ValueModel} (hω : ω.ProjApprox) (hℓ : 0 < ℓ) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) : ω.val (Honest.sourceGame (depthFamily e L) (decider e D)) ≤ ω.val (Honest.sourceGame L D)

Filling the spectator coordinates inside the existing first factor also has no soundness cost, since its entire source game is identical.