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.

The Naimark dilation itself, and the Born-rule transport lemmas that go with it, used to be written out in this file; they now live in MIPRE/Foundations/Dilation.lean. They are generic matrix mathematics that reach none of the vendored trees, and a second consumer appeared (blueprint lem:ms-direct-anticomm, in MIPRE/LCS/, which may not import MIPRE/Background/) for which being behind this file's 71k-line vendored import made them unusable.

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.

From a tensor-product strategy to a strategy of the vendored kind

The embedding direction of lem:povm-value-eq: a pure state is a density matrix, a projective measurement is a POVM, and the two index conventions already agree (both sides put Alice's and Bob's systems in a Kronecker product over Fin dA × Fin dB).

theorem MIPRE.Repetition.posSemidef_of_selfAdjoint_idem {d : Type} [Fintype d] [DecidableEq d] {P : Matrix d d ℂ} (hs : star P = P) (hp : P * P = P) : P.PosSemidef

A self-adjoint idempotent matrix is positive semidefinite: it equals Pᴴ * P.

theorem MIPRE.Repetition.trace_vecMulVec_star_mul {d : Type} [Fintype d] (ψ : d → ℂ) (E : Matrix d d ℂ) : (Matrix.vecMulVec ψ (star ψ) * E).trace = star ψ ⬝ᵥ E.mulVec ψ

The Born rule for a pure state written as a rank-one density matrix: tr(|ψ⟩⟨ψ| E) = ⟨ψ| E |ψ⟩.

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

A tensor-product strategy of this repository, as a strategy of the vendored module: the state is the rank-one density matrix |ψ⟩⟨ψ|, and each projective measurement is a POVM.

Equations

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

theorem MIPRE.Repetition.ofTensorProductStrategy_winProbability {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) : (ofTensorProductStrategy S).winProbability = S.value

The embedding preserves the value.

theorem MIPRE.Repetition.quantumValue_le_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 embedding direction of lem:povm-value-eq: every tensor-product strategy is a strategy of the vendored kind with the same value, so the quantum value of this repository is at most the vendored entangled value.

theorem MIPRE.Repetition.exists_purification {d : Type} [Fintype d] [DecidableEq d] {ρ : Matrix d d ℂ} (hρ : ρ.PosSemidef) (htr : ρ.trace = 1) : ∃ (ψ : d × d → ℂ), star ψ ⬝ᵥ ψ = 1 ∧ ∀ (M : Matrix d d ℂ), star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1).mulVec ψ = (ρ * M).trace

Purification, the first of the two inputs to the dilation direction. A density matrix ρ on d is the reduced state of a unit vector on d × d: factoring ρ = K * Kᴴ, the vector ψ (i, r) = K i r satisfies ⟨ψ| M ⊗ 1 |ψ⟩ = tr(ρ M) for every M, the second factor being the reference system. Neither a matrix square root nor the spectral theorem is needed, only the factorization of a positive semidefinite matrix. (General-purpose: it belongs in MIPRE/Mathlib/ once the dilation direction lands.)

From arbitrary finite local spaces to Fin d

theorem MIPRE.Repetition.projective_value_le_quantumValue {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {HA HB : Type} [Fintype HA] [DecidableEq HA] [Fintype HB] [DecidableEq HB] {G : Game X Y A B} (ψ : HA × HB → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) (PA : ProjectiveMeasurement X A (Matrix HA HA ℂ)) (PB : ProjectiveMeasurement Y B (Matrix HB HB ℂ)) : ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, (G.μ x y * if G.D x y a b = true then 1 else 0) * (star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (PA.M x a) (PB.M y b)).mulVec ψ).re ≤ quantumValue G

A pure state together with two projective families on arbitrary finite local spaces already bounds val*(G) from below: reindexing the two spaces by Fintype.equivFin turns them into a TensorProductStrategy, and a bijective reindexing changes no outcome probability. This is what lets the dilation steps above work with the natural index types (Alice × A, (Bob × R) × B) and only convert to Fin d at the end.

theorem MIPRE.Repetition.exists_purification_bipartite {dA dB : Type} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ρ : Matrix (dA × dB) (dA × dB) ℂ} (hρ : ρ.PosSemidef) (htr : ρ.trace = 1) : ∃ (ψ : dA × dB × dA × dB → ℂ), star ψ ⬝ᵥ ψ = 1 ∧ ∀ (E : Matrix dA dA ℂ) (F : Matrix dB dB ℂ), star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) E (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) F 1)).mulVec ψ = (ρ * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) E F).trace

Purification with the reference system placed on Bob's side. A density matrix ρ on dA × dB is the reduced state of a pure state on dA × (dB × R) with R = dA × dB, against which Alice's operators act as E ⊗ 1 and Bob's as F ⊗ 1_R; so the purification keeps the bipartite structure, at the cost of enlarging Bob's space.

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

The dilation direction of lem:povm-value-eq: mixed states and POVMs do not help. Given a vendored strategy — a density matrix ρ on Alice × Bob and POVMs {E^x_a}, {F^y_b} — purify ρ into a pure state on Alice × (Bob × R), dilate each POVM family to a projective family on one extra register (exists_projective_dilation, whose compressing isometry is the same for every question), and reindex the two local spaces to Fin types (projective_value_le_quantumValue). No outcome probability changes along the way, so the winning probability is the value of a tensor-product strategy.

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). The embedding direction is proved; the dilation direction is entangledValue_le_quantumValue (issue #28).

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|))).