Direct parallel repetition for entangled strategies

The uniform exponential parallel repetition theorem for finite-dimensional tensor-product strategies (blueprint thm:direct-repetition-q), in the vocabulary of this repository, transferred from the vendored module MIPRE/Background/Repetition/TenProofs/ (OpenAI, Ten advances in mathematics and theoretical computer science, 2026, Chapter 6): there is a universal c > 0 such that for every game G with nonempty answer alphabets and ε = 1 - val*(G) > 0, and every n ≥ 1, val*(G^{⊗n}) ≤ exp(-c·n·ε¹³/(ε + log(|A||B|))).

A game of this repository is literally a game of the vendored module (same question weights, same Bool predicate), and so is its direct repetition. The values differ in their strategy classes: MIPRE.quantumValue ranges over pure states and projective measurements on ℂ^dA ⊗ ℂ^dB, the vendored entangledValue over density matrices and POVMs on arbitrary finite-dimensional spaces. That they agree (purification and Naimark dilation) is quantumValue_eq_entangledValue (blueprint lem:povm-value-eq), the one statement here whose proof is still open.

def MIPRE.Repetition.toTP {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : QuantumParallelRepetition.Game X Y A B

A game of this repository as a game of the vendored module.

Equations

• MIPRE.Repetition.toTP G = { questionWeight := G.μ, weight_nonneg := ⋯, weight_normalized := ⋯, predicate := G.D }

theorem MIPRE.Repetition.toTP_repeat {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) : toTP (G.repeat n) = (toTP G).repeat n

The two direct repetitions are the same construction.

theorem MIPRE.Repetition.quantumValue_eq_entangledValue {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : quantumValue G = QuantumParallelRepetition.entangledValue (toTP G)

The quantum value of this repository (pure states, projective measurements) equals the entangled value of the vendored module (density matrices, POVMs): purification and Naimark dilation (blueprint lem:povm-value-eq).

theorem MIPRE.Repetition.quantumValue_repeat_le : ∃ (c : ℝ), 0 < c ∧ ∀ (X Y A B : Type) [inst : Fintype X] [inst_1 : Fintype Y] [inst_2 : Fintype A] [inst_3 : Fintype B] (G : Game X Y A B), Nonempty A → Nonempty B → 0 < 1 - quantumValue G → ∀ (n : ℕ), 0 < n → quantumValue (G.repeat n) ≤ Real.exp (-(c * ((1 - quantumValue G) ^ 13 / (1 - quantumValue G + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)

Uniform exponential parallel repetition for entangled strategies (blueprint thm:direct-repetition-q; OpenAI 2026, Chapter 6, via the vendored root QuantumParallelRepetition.distributionUniformExponential): there is a universal constant c > 0 such that for every game G with nonempty answer alphabets and ε = 1 - val*(G) > 0, and every n ≥ 1, val*(G^{⊗n}) ≤ exp(-c·n·ε¹³/(ε + log(|A||B|))).