Repeated entangled value is computed by a game on Fin alphabets

Proved

QuantumParallelRepetition.repeatedEntangledValue_eq_fin

by Shuze Chen · Aug 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

parallel-repetitionquantum-informationquantum-parallel-repetition

The universe-lowering step, for every number of repetitions at once: the repeated entangled values of a finite game agree with those of its standard-finite relabelling,

\omega^*(G^n) = \omega^*\big((G')^n\big) \qquad \text{for all } n,

where $G'$ has alphabets $\mathrm{Fin}\,|X|$ , $\mathrm{Fin}\,|Y|$ , $\mathrm{Fin}\,|A|$ , $\mathrm{Fin}\,|B|$ and therefore lives in Type.

Preamble

import Definitions.Def_quantum_parallel_repetition_game
import Definitions.Def_qpr_alphabet_relabelling
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Logic.Equiv.Fin.Basic

open scoped BigOperators
open QuantumParallelRepetition

variable {X Y A B X' Y' A' B' : Type*}
variable [Fintype X] [Fintype Y] [Fintype A] [Fintype B]
variable [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B']

Formal statement

theorem QuantumParallelRepetition.repeatedEntangledValue_eq_fin
    (G : Game X Y A B) (n : ℕ) :
    repeatedEntangledValue G n
      = repeatedEntangledValue (G.relabel (Fintype.equivFin X) (Fintype.equivFin Y)
          (Fintype.equivFin A) (Fintype.equivFin B)) n := by sorry

Source

Prove2me bridge for openai/ten-proofs, QuantumParallelRepetition.lean, https://github.com/openai/ten-proofs — universe transport, not part of the upstream development (which states parallel repetition for alphabets in `Type` only).

View graph