Parallel repetition of normal form verifiers: the assembly

MIPRE.repetition ℓ : Repetition ℓ — blueprint thm:parallel-repetition, inhabited (planning/repetition-verifier.md, R4). The output verifier repVerifier V λ τ β packages the repeated sampler (MIPRE.Repeat.repSampler) and the repeated decider (MIPRE.Repeat.repDecider). Its game at index n, with answers of length at most T for any T past the length of an encoded k-tuple, is the k-fold direct repetition of 𝒱_n at the parse length B, up to two relabelings (valStar_repVerifier):

• the questions 𝔽₂^{k s} are the k-tuples of questions 𝔽₂^s (CL.blockEquiv), with the distribution matching because the repeated sampler's CL functions are direct sums (CL.clDist_famSum), and the decider reads the i-th block of a question where the repeated game reads the i-th coordinate (toBits_block);
• the answers of length at most T contain the encoded k-tuples of answers of length at most B (tupleEmbed), on which the repeated decider accepts exactly when every coordinate is accepted (repDecider_accepts_iff), and it accepts nothing else, so the extra answers do not change the value (quantumValue_extendAnswers) nor the PCC strategies (SyncStrategy.extend).

Completeness is then the tensor power (exists_perfectPCC_repeat_doubled), soundness is quantumValue_repeat_le_soundBound, and the complexity clause is the two running-time theorems repSampler_timeBound and repDecider_timeBound at W = Repetition.arg, the constants they provide chosen once (sampC, decC, …) for the polynomial bound.

The output verifier

noncomputable def MIPRE.repVerifier {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta : ℕ) : Verifier ℓ

The output of the procedure on 𝒱 at (λ, τ, β): the repeated sampler and decider.

Equations

• MIPRE.repVerifier V lam tau beta = { sampler := MIPRE.Repeat.repSampler V.sampler lam tau, decider := MIPRE.Repeat.repDecider V.sampler.prog V.decider.prog lam tau beta, accepts_length := ⋯ }

Games reindexed along an equivalence of the questions

def MIPRE.Game.reindex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {X' : Type u_5} {Y' : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype X'] [Fintype Y'] (G : Game X Y A B) (eX : X' ≃ X) (eY : Y' ≃ Y) : Game X' Y' A B

The game G played through equivalences of the question alphabets.

Equations

• G.reindex eX eY = { μ := fun (x : X') (y : Y') => G.μ (eX x) (eY y), μ_nonneg := ⋯, μ_sum_one := ⋯, D := fun (x : X') (y : Y') (a : A) (b : B) => G.D (eX x) (eY y) a b }

Blocks of a question

theorem MIPRE.toBits_block {k s : ℕ} (x : Fin (k * s) → CL.𝔽₂) (i : Fin k) : CL.toBits (CL.block finProdFinEquiv i x) = Cost.Data.chunk s (↑i) (CL.toBits x)

The i-th block of a question of 𝔽₂^{k s} is the i-th chunk of its bit string.

Encoded tuples of answers

theorem MIPRE.tuple_encode_injective {k : ℕ} {f g : Fin k → Cost.BitStr} (h : (Cost.Data.list (List.ofFn fun (i : Fin k) => Cost.encode (f i))).toBitsPost = (Cost.Data.list (List.ofFn fun (i : Fin k) => Cost.encode (g i))).toBitsPost) : f = g

Encoded k-tuples of bit strings are determined by their coordinates.

noncomputable def MIPRE.tupleEmbed (k B T : ℕ) (hT : k * (4 * B + 2) + 1 ≤ T) : (Fin k → Verifier.Answers B) ↪ Verifier.Answers T

The k-tuples of answers of length at most B, as answers of length at most T, for T past the length of an encoded tuple.

Equations

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

theorem MIPRE.tupleEmbed_val (k B T : ℕ) (hT : k * (4 * B + 2) + 1 ≤ T) (aa : Fin k → Verifier.Answers B) : ↑((tupleEmbed k B T hT) aa) = (Cost.Data.list (List.ofFn fun (i : Fin k) => Cost.encode ↑(aa i))).toBitsPost

The game of the output is the repeated game

noncomputable def MIPRE.questionsEquiv {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n : ℕ) : (repVerifier V lam tau beta).Questions n ≃ (Fin (Repetition.reps lam tau n) → V.Questions n)

The questions of the output at index n are k-tuples of questions of 𝒱_n.

Equations

• MIPRE.questionsEquiv V lam tau beta n = MIPRE.CL.blockEquiv finProdFinEquiv

noncomputable def MIPRE.midGame {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n : ℕ) : Game ((repVerifier V lam tau beta).Questions n) ((repVerifier V lam tau beta).Questions n) (Fin (Repetition.reps lam tau n) → Verifier.Answers (Repetition.parseBound lam beta n)) (Fin (Repetition.reps lam tau n) → Verifier.Answers (Repetition.parseBound lam beta n))

The repeated game, on the output's questions.

Equations

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

theorem MIPRE.game_μ_eq {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n T : ℕ) (x y : (repVerifier V lam tau beta).Questions n) : ((repVerifier V lam tau beta).game n T).μ x y = (midGame V lam tau beta n).μ x y

The distribution of the output's game is that of the repeated game.

theorem MIPRE.game_D_tuple {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n T : ℕ) (hT : Repetition.reps lam tau n * (4 * Repetition.parseBound lam beta n + 2) + 1 ≤ T) (x y : (repVerifier V lam tau beta).Questions n) (aa bb : Fin (Repetition.reps lam tau n) → Verifier.Answers (Repetition.parseBound lam beta n)) : ((repVerifier V lam tau beta).game n T).D x y ((tupleEmbed (Repetition.reps lam tau n) (Repetition.parseBound lam beta n) T hT) aa) ((tupleEmbed (Repetition.reps lam tau n) (Repetition.parseBound lam beta n) T hT) bb) = (midGame V lam tau beta n).D x y aa bb

The output's decider on encoded tuples: every coordinate accepted.

theorem MIPRE.game_D_range {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n T : ℕ) (hT : Repetition.reps lam tau n * (4 * Repetition.parseBound lam beta n + 2) + 1 ≤ T) (x y : (repVerifier V lam tau beta).Questions n) (a b : Verifier.Answers T) (h : ((repVerifier V lam tau beta).game n T).D x y a b = true) : (∃ (aa : Fin (Repetition.reps lam tau n) → Verifier.Answers (Repetition.parseBound lam beta n)), (tupleEmbed (Repetition.reps lam tau n) (Repetition.parseBound lam beta n) T hT) aa = a) ∧ ∃ (bb : Fin (Repetition.reps lam tau n) → Verifier.Answers (Repetition.parseBound lam beta n)), (tupleEmbed (Repetition.reps lam tau n) (Repetition.parseBound lam beta n) T hT) bb = b

The output's decider accepts only encoded tuples.

theorem MIPRE.val_repVerifier {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n : ℕ) (ω : ValueModel) (T : ℕ) (hT : Repetition.reps lam tau n * (4 * Repetition.parseBound lam beta n + 2) + 1 ≤ T) : (repVerifier V lam tau beta).val ω n T = ω.val ((V.game n (Repetition.parseBound lam beta n)).repeat (Repetition.reps lam tau n))

The value of the output's game is that of the repeated game, in every value model, at any answer bound past the length of an encoded tuple: the two relabelings are transports every model has (ValueModel.extendAnswers, ValueModel.eq_of_equiv), so the bridge from the verifier to the game does not depend on the value.

theorem MIPRE.valStar_repVerifier {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n T : ℕ) (hT : Repetition.reps lam tau n * (4 * Repetition.parseBound lam beta n + 2) + 1 ≤ T) : (repVerifier V lam tau beta).valStar n T = quantumValue ((V.game n (Repetition.parseBound lam beta n)).repeat (Repetition.reps lam tau n))

The value of the output's game is that of the repeated game: val_repVerifier in the tensor-product model.

theorem MIPRE.hasPerfectPCC_repVerifier {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n T : ℕ) (hT : Repetition.reps lam tau n * (4 * Repetition.parseBound lam beta n + 2) + 1 ≤ T) (h : V.HasPerfectPCC n (Repetition.parseBound lam beta n)) : (repVerifier V lam tau beta).HasPerfectPCC n T

Completeness: a value-1 PCC strategy for 𝒱_n at the parse length gives one for the output's game, the tensor power relabeled and extended to the output's answers.

theorem MIPRE.val_repVerifier_le {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n : ℕ) {ω : ValueModel} {c : ℝ} (hω : Repetition.GameSoundIn ω c) (T : ℕ) (hT : Repetition.reps lam tau n * (4 * Repetition.parseBound lam beta n + 2) + 1 ≤ T) {ε : ℝ} (hε : 0 < ε) (h : V.val ω n (Repetition.parseBound lam beta n) ≤ 1 - ε) : (repVerifier V lam tau beta).val ω n T ≤ Repetition.soundBound c ε (Repetition.reps lam tau n) (Repetition.parseBound lam beta n)

Soundness in a value model: in a model with the direct repetition bound at the constant c (Repetition.GameSoundIn), ω(𝒱_n) ≤ 1 - ε at the parse length gives that bound for the output's game.

theorem MIPRE.valStar_repVerifier_le {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n T : ℕ) (hT : Repetition.reps lam tau n * (4 * Repetition.parseBound lam beta n + 2) + 1 ≤ T) {ε : ℝ} (hε : 0 < ε) (h : V.valStar n (Repetition.parseBound lam beta n) ≤ 1 - ε) : (repVerifier V lam tau beta).valStar n T ≤ Repetition.soundBound Repetition.repConst ε (Repetition.reps lam tau n) (Repetition.parseBound lam beta n)

Soundness: val*(𝒱_n) ≤ 1 - ε at the parse length gives the direct repetition bound for the output's game — val_repVerifier_le in the tensor-product model.

The constants of the running-time bounds

noncomputable def MIPRE.sampC : ℕ

The constants of repSampler_timeBound, chosen once.

Equations

• MIPRE.sampC = MIPRE.Repeat.repSampler_timeBound.choose

noncomputable def MIPRE.sampM : ℕ

Equations

• MIPRE.sampM = MIPRE.sampM._proof_1.choose

noncomputable def MIPRE.sampE : ℕ

Equations

• MIPRE.sampE = MIPRE.sampE._proof_1.choose

theorem MIPRE.sampC_spec {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) (R : Budget) (W : ℕ) (hW : Repeat.SampDom S lam tau n R W) (hS : S.TimeBoundAt n R.S R.k) : (Repeat.repSampler S lam tau).TimeBoundAt n (sampC * (W + 1) ^ sampM) (sampE * (R.k + 1))

noncomputable def MIPRE.decC : ℕ

The constants of repDecider_timeBound, chosen once.

Equations

• MIPRE.decC = MIPRE.Repeat.repDecider_timeBound.choose

noncomputable def MIPRE.decM : ℕ

Equations

• MIPRE.decM = MIPRE.decM._proof_1.choose

noncomputable def MIPRE.decE : ℕ

Equations

• MIPRE.decE = MIPRE.decE._proof_1.choose

theorem MIPRE.decC_spec {ℓ : ℕ} (S : CL.Sampler ℓ) (D : Decider) (lam tau beta n : ℕ) (R : Budget) (W : ℕ) (hW : Repeat.DecDom S D lam tau beta n R W) (hS : S.TimeBoundAt n R.S R.k) (hD : D.TimeBoundAt n R.D R.k) : (Repeat.repDecider S.prog D.prog lam tau beta).TimeBoundAt n (decC * (W + 1) ^ decM) (decE * (R.k + 1))

noncomputable def MIPRE.repBound : Polynomial ℕ

The polynomial bounding the running times and the dimension of the output.

Equations

• MIPRE.repBound = Polynomial.C (MIPRE.sampC + MIPRE.decC + 1) * (Polynomial.X + 1) ^ (max MIPRE.sampM MIPRE.decM + 2)

theorem MIPRE.repBound_eval (W : ℕ) : Polynomial.eval W repBound = (sampC + decC + 1) * (W + 1) ^ (max sampM decM + 2)

noncomputable def MIPRE.repAnsBound : Polynomial ℕ

The polynomial bounding the answers the output accepts, in k(n) + B(n).

Equations

• MIPRE.repAnsBound = Polynomial.C 5 * (Polynomial.X + 1) ^ 2

theorem MIPRE.repAnsBound_eval (A : ℕ) : Polynomial.eval A repAnsBound = 5 * (A + 1) ^ 2

theorem MIPRE.ans_ineq (k B : ℕ) : k * (4 * B + 2) + 1 ≤ 5 * (k + B + 1) ^ 2

theorem MIPRE.ansArg_bound (lam tau beta n : ℕ) : Repetition.reps lam tau n * (4 * Repetition.parseBound lam beta n + 2) + 1 ≤ Polynomial.eval (Repetition.ansArg lam tau beta n) repAnsBound

The encoded tuples fit in the answer bound.

The complexity clause

theorem MIPRE.within_repVerifier {ℓ : ℕ} (V : Verifier ℓ) (lam tau beta n : ℕ) (R : Budget) (hV : V.Within n R) : (repVerifier V lam tau beta).Within n { S := Polynomial.eval (Repetition.arg lam tau beta n R V.size) repBound, d := Polynomial.eval (Repetition.arg lam tau beta n R V.size) repBound, D := Polynomial.eval (Repetition.arg lam tau beta n R V.size) repBound, k := max sampE decE * (R.k + 1), B := Polynomial.eval (Repetition.ansArg lam tau beta n) repAnsBound }

The complexity clause: within repBound at Repetition.arg, at degree max sampE decE (R.k + 1), with answers within repAnsBound at k(n) + B(n).

The theorem

noncomputable def MIPRE.repetition (ℓ : ℕ) : Repetition ℓ

Parallel repetition of normal form verifiers (blueprint thm:parallel-repetition), inhabited: the repeated sampler and decider, their programs as polynomial-time functions of the inputs through the s-m-n map, the complexity clause within_repVerifier, completeness hasPerfectPCC_repVerifier and soundness valStar_repVerifier_le.

Equations

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

theorem MIPRE.repetition_withConst_soundIn {ℓ : ℕ} {ω : ValueModel} {c : ℝ} (hω : Repetition.GameSoundIn ω c) (c' : ℝ) (hc' : 0 < c') (hle : c' ≤ Repetition.repConst) (hc : c' ≤ c) : ((repetition ℓ).withConst c' hc' hle).SoundIn ω

Parallel repetition is sound in every value model with the direct repetition bound at a constant at least the procedure's, whatever that constant was lowered to (Repetition.withConst): the procedure's soundness clause read in ω (Repetition.SoundIn).