# Threshold repetition for entangled games

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Threshold parallel repetition for finite-dimensional entangled games](../../preprints/Threshold-parallel-repetition-for-finite-dimensional-entangled-games-September-25-2026/paper.pdf)

## Scope

The formalization gives exponential threshold parallel repetition for every finite two-player game with arbitrary correlated questions. If its finite-dimensional entangled value is $v<1$, its answer sets are $A,B$, and $0<\delta<1-v$, then the probability of winning at least the fraction $v+\delta$ of $k$ repetitions is at most $\exp(-\kappa\delta^{13}k/(1+\log(|A||B|)))$ for one universal $\kappa>0$. The bound applies to every joint finite-dimensional strategy and to their supremum, without assuming attainment. The separate distribution-dependent cubic bound is outside this scope.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Threshold parallel repetition for entangled games | [EntangledGames.lean](../ComparatorChallenges/EntangledGames.lean) |