The games of a verifier: congruence, answer padding, perfect PCC strategies

Bookkeeping for Verifier.game n T needed by the instantiation of the compressibility criterion (blueprint rem:compression-abstract), in any value model ω (ValueModel) — the tensor-product value val* and the commuting-operator value ω_co are its two instances — all consequences of the transport properties a model carries:

• Same sampler, comparable deciders. Two verifiers with the same sampler whose deciders accept the same tuples at index n have the same value and the same perfect PCC strategies there (val_congr, hasPerfectPCC_congr); accepting more raises the value (val_le_of_accepts_imp).
• Answer padding. Enlarging the answer-length bound T can only raise the value (val_le_of_le) and preserves perfect PCC strategies (hasPerfectPCC_of_le); when the decider rejects every answer longer than T, it does not change the value at all (val_eq_of_rejects). This is what lets the game of a verifier be compared across the answer bounds N ^ λ and poly(n, λ) of GapCompression and the bound a class of descriptions is defined with.
• A perfect PCC strategy gives val* = 1 (valStar_eq_one_of_hasPerfectPCC), through syncValue_le_quantumValue on the doubled game and quantumValue_doubledGame, hence value 1 in every model (val_eq_one_of_hasPerfectPCC), the model dominating val*.

Verifier.val ω n T is the value of 𝒱_n in the model; Verifier.valStar is its tensor-product instance, definitionally, and the valStar_* lemmas below are the generic ones at ValueModel.tensor. Verifier.HasPerfectPCC is a PCC strategy of value 1 on the doubled game (Verifier.doubledGame, Foundations/GapCompression.lean), so none of the lemmas here asks the decider to be synchronous at n. The file ends with GapCompression.Sound ω, the soundness clause of gap compression read in the model: soundness is Sound ValueModel.tensor, and the commuting-operator case is the hypothesis of the conditional MIP^co = coRE.

def MIPRE.Verifier.Answers.castLE {T T' : ℕ} (h : T ≤ T') : Answers T ↪ Answers T'

The embedding of the answers of length at most T into those of length at most T'.

Equations

• MIPRE.Verifier.Answers.castLE h = { toFun := fun (a : MIPRE.Verifier.Answers T) => ⟨↑a, ⋯⟩, inj' := ⋯ }

@[simp]

theorem MIPRE.Verifier.Answers.castLE_val {T T' : ℕ} (h : T ≤ T') (a : Answers T) : ↑((castLE h) a) = ↑a

instance MIPRE.Verifier.instNonemptyAnswers (T : ℕ) : Nonempty (Answers T)

theorem MIPRE.Verifier.game_D {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (x y : V.Questions n) (a b : Answers T) : (V.game n T).D x y a b = true ↔ V.decider.Accepts n (CL.toBits x) (CL.toBits y) ↑a ↑b

The value of 𝒱_n in a model

noncomputable def MIPRE.Verifier.val {ℓ : ℕ} (V : Verifier ℓ) (ω : ValueModel) (n T : ℕ) : ℝ

The value of 𝒱_n in the model ω, with answers of length at most T.

Equations

• V.val ω n T = ω.val (V.game n T)

@[simp]

theorem MIPRE.Verifier.val_tensor {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) : V.val ValueModel.tensor n T = V.valStar n T

@[simp]

theorem MIPRE.Verifier.val_commuting {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) : V.val ValueModel.commuting n T = commutingOperatorValue (V.game n T)

theorem MIPRE.Verifier.valStar_le_val {ℓ : ℕ} (V : Verifier ℓ) (ω : ValueModel) (n T : ℕ) : V.valStar n T ≤ V.val ω n T

Every model dominates val*.

theorem MIPRE.Verifier.val_le_one {ℓ : ℕ} (V : Verifier ℓ) (ω : ValueModel) (n T : ℕ) : V.val ω n T ≤ 1

Same sampler, comparable deciders

theorem MIPRE.Verifier.val_le_of_accepts_imp {ℓ : ℕ} (ω : ValueModel) {V W : Verifier ℓ} {n T : ℕ} (hS : W.sampler = V.sampler) (h : ∀ (x y a b : Cost.BitStr), V.decider.Accepts n x y a b → W.decider.Accepts n x y a b) : V.val ω n T ≤ W.val ω n T

With the same sampler, a decider accepting more at index n gives a larger value.

theorem MIPRE.Verifier.val_congr {ℓ : ℕ} (ω : ValueModel) {V W : Verifier ℓ} {n T : ℕ} (hS : W.sampler = V.sampler) (h : ∀ (x y a b : Cost.BitStr), V.decider.Accepts n x y a b ↔ W.decider.Accepts n x y a b) : V.val ω n T = W.val ω n T

With the same sampler, deciders accepting the same tuples at index n give the same value.

theorem MIPRE.Verifier.valStar_congr {ℓ : ℕ} {V W : Verifier ℓ} {n T : ℕ} (hS : W.sampler = V.sampler) (h : ∀ (x y a b : Cost.BitStr), V.decider.Accepts n x y a b ↔ W.decider.Accepts n x y a b) : V.valStar n T = W.valStar n T

theorem MIPRE.Verifier.hasPerfectPCC_of_accepts_iff {ℓ : ℕ} {V W : Verifier ℓ} {n T : ℕ} (hS : W.sampler = V.sampler) (h : ∀ (x y a b : Cost.BitStr), V.decider.Accepts n x y a b ↔ W.decider.Accepts n x y a b) (hV : V.HasPerfectPCC n T) : W.HasPerfectPCC n T

With the same sampler, deciders accepting the same tuples at index n have the same perfect PCC strategies.

theorem MIPRE.Verifier.hasPerfectPCC_congr {ℓ : ℕ} {V W : Verifier ℓ} {n T : ℕ} (hS : W.sampler = V.sampler) (h : ∀ (x y a b : Cost.BitStr), V.decider.Accepts n x y a b ↔ W.decider.Accepts n x y a b) : V.HasPerfectPCC n T ↔ W.HasPerfectPCC n T

Answer padding

theorem MIPRE.Verifier.val_le_of_le {ℓ : ℕ} (V : Verifier ℓ) (ω : ValueModel) {n T T' : ℕ} (hT : T ≤ T') : V.val ω n T ≤ V.val ω n T'

Enlarging the answer-length bound can only raise the value.

def MIPRE.Verifier.RejectsLong {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) : Prop

The decider rejects every answer longer than T at index n. The property a compressed decider has beyond its time bound (GapCompression.output_rejects_long), and the third clause of membership in the classes of the halting reduction (Verifier.InClassA, InClassB): it is what lets the answer bound a class is read with be raised without moving the value (val_eq_of_rejects), which the soundness direction of the compressor's obligation needs. The paper's V^halt has it by construction, Step 6 of its decider F being an explicit length check; the classes here range over arbitrary strings and have to ask for it.

Equations

• V.RejectsLong n T = ∀ (x y a b : MIPRE.Cost.BitStr), T < List.length a ∨ T < List.length b → ¬V.decider.Accepts n x y a b

theorem MIPRE.Verifier.val_eq_of_rejects {ℓ : ℕ} (V : Verifier ℓ) (ω : ValueModel) {n T T' : ℕ} (hT : T ≤ T') (hrej : V.RejectsLong n T) : V.val ω n T' = V.val ω n T

When the decider rejects every answer longer than T at index n, enlarging the answer-length bound does not change the value.

theorem MIPRE.Verifier.valStar_eq_of_rejects {ℓ : ℕ} (V : Verifier ℓ) {n T T' : ℕ} (hT : T ≤ T') (hrej : V.RejectsLong n T) : V.valStar n T' = V.valStar n T

theorem MIPRE.Verifier.val_eq_zero_of_rejects_all {ℓ : ℕ} (V : Verifier ℓ) (ω : ValueModel) {n T : ℕ} (hrej : ∀ (x y a b : Cost.BitStr), ¬V.decider.Accepts n x y a b) : V.val ω n T = 0

A decider that accepts nothing at index n gives value 0.

theorem MIPRE.Verifier.hasPerfectPCC_of_le {ℓ : ℕ} (V : Verifier ℓ) {n T T' : ℕ} (hT : T ≤ T') (h : V.HasPerfectPCC n T) : V.HasPerfectPCC n T'

Enlarging the answer-length bound preserves perfect PCC strategies.

Perfect PCC strategies and the value

theorem MIPRE.Verifier.valStar_eq_one_of_hasPerfectPCC {ℓ : ℕ} (V : Verifier ℓ) {n T : ℕ} (h : V.HasPerfectPCC n T) : V.valStar n T = 1

A perfect PCC strategy gives quantum value 1.

theorem MIPRE.Verifier.val_eq_one_of_hasPerfectPCC {ℓ : ℕ} (V : Verifier ℓ) (ω : ValueModel) {n T : ℕ} (h : V.HasPerfectPCC n T) : V.val ω n T = 1

A perfect PCC strategy gives value 1 in every model: the model dominates val*.

The doubled game

theorem MIPRE.Verifier.val_doubledGame {ℓ : ℕ} (V : Verifier ℓ) (ω : ValueModel) (n T : ℕ) : ω.val (V.doubledGame n T).toGame = V.val ω n T

The doubled game has the value it doubles, in every model.

def MIPRE.GapCompression.Sound (G : GapCompression) (ω : ValueModel) : Prop

Soundness of gap compression in a value model (blueprint def:compression-co-sound): for a λ-bounded input and n ≥ C₀, a value at most 1/2 of 𝒱_{2^n} in the model gives a value at most 1/2 of 𝒱^compr_n, at the answer bounds of GapCompression.soundness. That field is Sound ValueModel.tensor (GapCompression.sound_tensor); Sound ValueModel.commuting is the model-co case of the soundness clause of Lin's gap compression theorem (Lin25, thm:gappedcompression) and the one hypothesis of the conditional MIP^co = coRE (planning/mipco-track.md).

Equations

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

theorem MIPRE.GapCompression.sound_tensor (G : GapCompression) : G.Sound ValueModel.tensor

The soundness clause of gap compression is soundness in the tensor-product model.