Direct parallel repetition for commuting-operator strategies

The uniform direct parallel repetition theorem for commuting-operator strategies (blueprint thm:direct-repetition-co), in the vocabulary of this repository, transferred from the vendored development MIPRE/Background/Repetition/CommutingRepetition/ (Vidick, Uniform direct parallel repetition for two-player commuting-operator strategies, 2026): there is a universal c > 0 such that for every game G with nonempty alphabets and every n ≥ 1, valco(G^{⊗n}) ≤ exp(-c·n·ε⁷/(ε + log(|A||B|))) where ε = 1 - valco(G).

The transfer is a field-by-field identification: a MIPRE.Game is a game of the vendored development with {0,1}-valued payoff, MIPRE.CommutingOperatorStrategy is its CommutingStrategy at universe 0, the two suprema defining the value range over the same set of reals, and the two direct repetitions agree (a product of {0,1}-valued payoffs is the indicator of the conjunction).

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

A game of this repository as a game of the vendored development: the decision predicate becomes a {0,1}-valued payoff.

Equations

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

def MIPRE.Repetition.toCRStrategy {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) : CommutingRepetition.CommutingStrategy X Y A B

A commuting-operator strategy of this repository as one of the vendored development.

Equations

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

def MIPRE.Repetition.ofCRStrategy {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingRepetition.CommutingStrategy X Y A B) : CommutingOperatorStrategy X Y A B

A commuting-operator strategy of the vendored development as one of this repository.

Equations

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

theorem MIPRE.Repetition.win_toCRStrategy {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (S : CommutingOperatorStrategy X Y A B) : (toCR G).win (toCRStrategy S).correlation = CommutingOperatorStrategy.value G S

The value of a strategy is its winning probability in the vendored development.

theorem MIPRE.Repetition.commutingOperatorValue_eq_omegaCO {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : commutingOperatorValue G = (toCR G).omegaCO

The commuting-operator value of this repository is the commuting-operator value of the vendored development: the two suprema range over the same set of reals.

theorem MIPRE.Repetition.payoff_repeat {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (xs : Fin n → X) (ys : Fin n → Y) (as : Fin n → A) (bs : Fin n → B) : (toCR (G.repeat n)).payoff xs ys as bs = ((toCR G).repeat n).payoff xs ys as bs

The payoff of the repeated game of the vendored development is the indicator of the conjunction of the coordinate predicates.

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

The direct repetition of this repository, transported, has the value of the direct repetition of the vendored development.

theorem MIPRE.Repetition.commutingOperatorValue_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] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (G : Game X Y A B) (n : ℕ), 1 ≤ n → commutingOperatorValue (G.repeat n) ≤ Real.exp (-(c * ((1 - commutingOperatorValue G) ^ 7 / (1 - commutingOperatorValue G + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)

Uniform direct parallel repetition for commuting-operator strategies (blueprint thm:direct-repetition-co; Vidick 2026, Theorem 7.1, via the vendored root CommutingRepetition.uniform_parallel_repetition): there is a universal constant c > 0 such that for every game G with nonempty alphabets and every n ≥ 1, valco(G^{⊗n}) ≤ exp(-c·n·ε⁷/(ε + log(|A||B|))) with ε = 1 - valco(G) (when ε = log(|A||B|) = 0 the quotient is 0 / 0 = 0).