theorem CommutingRepetition.uniform_parallel_repetition : ∃ (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 → (G.repeat n).omegaCO ≤ Real.exp (-(c * ((1 - G.omegaCO) ^ 7 / (1 - G.omegaCO + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)

Uniform direct parallel repetition for commuting-operator strategies (07_main_theorem.tex, Theorem 7.1): there is a universal c > 0 such that for every finite game G with payoffs in [0,1] and every n ≥ 1, ω^co(G^{⊗n}) ≤ exp(−c·n·ε⁷/(ε + log(|A||B|))) where ε = 1 − ω^co(G).

theorem CommutingRepetition.uniform_parallel_repetition_pow13 : ∃ (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 → (G.repeat n).omegaCO ≤ Real.exp (-(c * ((1 - G.omegaCO) ^ 13 / (1 - G.omegaCO + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)

Power-thirteen corollary (07_main_theorem.tex, Corollary 7.2): some universal constant gives the ε¹³ bound. The paper's "with the same universal constant" is not encoded by this second ∃ c (a deliberate weaker-but-true rendering recorded in DIFFERENCES.md); the main theorem's constant does work, since ε⁷ ≥ ε¹³ on [0,1].