Parallel repetition of normal form verifiers, as a hypothesis

Blueprint thm:parallel-repetition (paper parallel_amplification.tex, thm:repetition, in its direct rather than anchored form; ledger nodes 1.4, 1.4.3, 1.4.3.1), stated as the data the theorem provides: the structure Repetition ℓ. Its inhabitation is the theorem: the game-level direct repetition theorem thm:direct-repetition-q (MIPRE.Repetition.quantumValue_repeat_le, vendored) packaged at the level of verifiers — a sampler running k(n) independent copies of the input sampler, a decider parsing a self-delimiting k(n)-tuple of answers and running the input decider on every coordinate. Nothing here proves it. The composition MIPRE.GapCompression.ofPipeline consumes an instance at ℓ = 7.

The reading of the paper's statement in the vocabulary of MIPRE.Verifier:

• ComputeParrepVerifier takes (𝒱, ℓ, λ, τ); the number of repetitions is k(n) = (λn)^τ, read as 2^{τ(|λ| + |n|)} with |·| the bit length — the power of two just above (λn)^τ (Nat.size), which a program of the ambient model writes down by a walk over the bits of λ and n, where the paper's expression would need multiplication. The repeated decider parses each coordinate of an answer against a length 2^{β(|λ| + |n|)} — the paper's B_𝒟(n), read from the timeout-counter form of the decider there, and a further parameter β here — so the procedure is a polynomial-time function of the input programs and (λ, τ, β) (compute); the repeated sampler depends only on the input sampler and (λ, τ) (sampler).
• The complexity clause bounds the output at index n by a polynomial in k(n), the parse length, the input's budget at n, the input's description length, the raw parameters and the input's cost on the dimension query (Repetition.arg; the paper's poly(k(n), TIME_𝒮(n)) and poly(k(n), B_𝒟(n))), at a degree affine in the input's — the repeated decider runs the input decider through the universal machine, whose overhead is polynomial — and the answers it accepts by a polynomial in k(n) and the parse length alone.
• Completeness: a value-1 PCC strategy for 𝒱_n gives one for 𝒱^rep_n.
• Soundness: val*(𝒱_n) ≤ 1 - ε gives val*(𝒱^rep_n) ≤ exp(-c ε^13 k(n) / (B + 1)), with B = 2^{β(|λ| + |n|)} the parse length: thm:direct-repetition-q with log(|𝒜||ℬ|) ≤ 2(B + 1) for answer alphabets of strings of length at most B, the constant c absorbing the factor 3. The exponent 13 is the vendored theorem's.

Answer alphabets: 𝒱_n is read with answers of length at most the parse length, so that the repeated game is exactly the direct repetition of 𝒱_n at that alphabet, and 𝒱^rep_n with answers of length at most its own bound, beyond which its decider rejects.

@[reducible, inline]

abbrev MIPRE.Repetition.reps (lam tau n : ℕ) : ℕ

The number of repetitions k(n) = 2^{τ(|λ| + |n|)}, at least (λn + 1)^τ.

Equations

• MIPRE.Repetition.reps lam tau n = 2 ^ (tau * (lam.size + n.size))

@[reducible, inline]

abbrev MIPRE.Repetition.parseBound (lam beta n : ℕ) : ℕ

The length against which each coordinate of an answer is parsed: 2^{β(|λ| + |n|)}, at least (λn + 1)^β and at most (λn + 1)^{6β} for λ, n ≥ 1.

Equations

• MIPRE.Repetition.parseBound lam beta n = 2 ^ (beta * (lam.size + n.size))

@[reducible, inline]

abbrev MIPRE.Repetition.arg (lam tau beta n : ℕ) (R : Budget) (s : ℕ) : ℕ

The argument of the polynomial bounding the running times of the output at index n: the repetition count, the parse length, the input's budget and description length, the raw parameters λ, τ, β, n (the paper's poly(k(n), TIME_𝒮(n)) dominates them when τ ≥ 1; here they are added, since τ = 0 is allowed), and 10^{R.k}, the input's time on the dimension query — an input of fixed size 9, which the output asks on every input of its own, including the empty one, and whose cost at degree R.k no polynomial in the other quantities dominates.

Equations

• MIPRE.Repetition.arg lam tau beta n R s = MIPRE.Repetition.reps lam tau n + MIPRE.Repetition.parseBound lam beta n + R.S + R.d + R.D + R.B + s + lam + tau + beta + n + 10 ^ R.k

@[reducible, inline]

abbrev MIPRE.Repetition.ansArg (lam tau beta n : ℕ) : ℕ

The argument of the polynomial bounding the answers of the output at index n.

Equations

• MIPRE.Repetition.ansArg lam tau beta n = MIPRE.Repetition.reps lam tau n + MIPRE.Repetition.parseBound lam beta n

noncomputable def MIPRE.Repetition.soundBound (c ε : ℝ) (k B : ℕ) : ℝ

The soundness bound exp(-c ε^13 k / (B + 1)).

Equations

• MIPRE.Repetition.soundBound c ε k B = Real.exp (-(c * ε ^ 13 * ↑k / (↑B + 1)))

theorem MIPRE.Repetition.soundBound_anti {c c' ε : ℝ} (hc : c ≤ c') (hε : 0 ≤ ε) (k B : ℕ) : soundBound c' ε k B ≤ soundBound c ε k B

The soundness bound is antitone in the constant.

structure MIPRE.Repetition (ℓ : ℕ) : Type

Parallel repetition of normal form verifiers (blueprint thm:parallel-repetition) for ℓ-level inputs: the data of the procedure ComputeParrepVerifier together with the guarantees of the theorem. An instance of this structure is the theorem.

• c : ℝ

  The constant of the soundness exponent.

• c_pos : 0 < self.c
• bound : Polynomial ℕ

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

• ansBound : Polynomial ℕ

  The polynomial bounding the length of the answers the output accepts, in k(n) and the parse length.

• deg : ℕ

  The degree multiplier of the output's running times.

• sampler : CL.Sampler ℓ → ℕ → ℕ → CL.Sampler ℓ

  The repeated sampler, a function of the input sampler and (λ, τ).

• samplerProg : Cost.PolyTimeFun (Cost.Prog × ℕ × ℕ) Cost.Prog

  Its program, computable from the input sampler's program and (λ, τ) in polynomial time.

• samplerProg_eq (S : CL.Sampler ℓ) (lam tau : ℕ) : self.samplerProg.toFun (S.prog, lam, tau) = (self.sampler S lam tau).prog
• compute : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × ℕ × ℕ × ℕ) Cost.Prog

  ComputeParrepVerifier: the repeated decider, from the input programs and (λ, τ, β), in polynomial time.

• output : Verifier ℓ → ℕ → ℕ → ℕ → Verifier ℓ

  The output on a normal form input, at parameters (λ, τ, β).

• output_sampler (V : Verifier ℓ) (lam tau beta : ℕ) : (self.output V lam tau beta).sampler = self.sampler V.sampler lam tau
• output_decider (V : Verifier ℓ) (lam tau beta : ℕ) : (self.output V lam tau beta).decider.prog = self.compute.toFun ((V.sampler.prog, V.decider.prog), lam, tau, beta)
• within (V : Verifier ℓ) (lam tau beta n : ℕ) (R : Budget) : V.Within n R → (self.output V lam tau beta).Within n { S := Polynomial.eval (arg lam tau beta n R V.size) self.bound, d := Polynomial.eval (arg lam tau beta n R V.size) self.bound, D := Polynomial.eval (arg lam tau beta n R V.size) self.bound, k := self.deg * (R.k + 1), B := Polynomial.eval (ansArg lam tau beta n) self.ansBound }

  The complexity clause: within a polynomial of k(n), the parse length, the input's budget and the input's description length, at degree deg (k + 1), and answers within a polynomial of k(n) and the parse length.

• completeness (V : Verifier ℓ) (lam tau beta n : ℕ) : V.HasPerfectPCC n (parseBound lam beta n) → (self.output V lam tau beta).HasPerfectPCC n (Polynomial.eval (ansArg lam tau beta n) self.ansBound)

  Completeness.

• soundness (V : Verifier ℓ) (lam tau beta n : ℕ) (ε : ℝ) : 0 < ε → ε ≤ 1 → V.valStar n (parseBound lam beta n) ≤ 1 - ε → (self.output V lam tau beta).valStar n (Polynomial.eval (ansArg lam tau beta n) self.ansBound) ≤ soundBound self.c ε (reps lam tau n) (parseBound lam beta n)

  Soundness. val*(𝒱_n) ≤ 1 - ε gives val*(𝒱^rep_n) ≤ exp(-c ε^13 k(n) / (B + 1)).

def MIPRE.Repetition.SoundIn {ℓ : ℕ} (R : Repetition ℓ) (ω : ValueModel) : Prop

The soundness clause of parallel repetition in a value model: the field soundness with the value val* replaced by the model's. The field is the tensor-product case (Repetition.soundIn_tensor); the commuting-operator case is what Phase 2 of planning/mipco-track.md proves, from the vendored commutingOperatorValue_repeat_le.

Equations

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

theorem MIPRE.Repetition.soundIn_tensor {ℓ : ℕ} (R : Repetition ℓ) : R.SoundIn ValueModel.tensor

The soundness clause of parallel repetition is soundness in the tensor-product model.

def MIPRE.Repetition.withConst {ℓ : ℕ} (R : Repetition ℓ) (c : ℝ) (hc : 0 < c) (hle : c ≤ R.c) : Repetition ℓ

The same procedure with a smaller soundness constant. Every clause survives: soundness because the bound is antitone in the constant (Repetition.soundBound_anti). This is how one procedure serves two value models whose repetition theorems have different constants: the exponent τ of the compression is chosen against the smaller one.

Equations

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

theorem MIPRE.Repetition.SoundIn.withConst {ℓ : ℕ} {R : Repetition ℓ} {ω : ValueModel} (h : R.SoundIn ω) (c : ℝ) (hc : 0 < c) (hle : c ≤ R.c) : (R.withConst c hc hle).SoundIn ω

Lowering the constant keeps soundness in every value model.