Prove2Me

Entangled value is computed by a game on Fin alphabets

Proved
QuantumParallelRepetition.entangledValue_eq_fin

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

parallel-repetitionquantum-informationquantum-parallel-repetition

Every finite game has the same entangled value as a game whose alphabets are standard finite types:

ω∗(G)=ω∗(G′),G′:Game Fin ∣X∣ Fin ∣Y∣ Fin ∣A∣ Fin ∣B∣.\omega^*(G) = \omega^*\big(G'\big), \qquad G' : \mathrm{Game}\ \mathrm{Fin}\,|X|\ \mathrm{Fin}\,|Y|\ \mathrm{Fin}\,|A|\ \mathrm{Fin}\,|B|.

This is the universe-lowering step. A game over arbitrary finite alphabets lives in whatever universe those alphabets inhabit, while Fin n always lives in Type. Any statement about entangled values proved for games in Type therefore transfers to games over arbitrary finite alphabets.

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.entangledValue_eq_fin (G : Game X Y A B) :
    entangledValue G
      = entangledValue (G.relabel (Fintype.equivFin X) (Fintype.equivFin Y)
          (Fintype.equivFin A) (Fintype.equivFin B)) := 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