theorem CommutingRepetition.constant_choice {C c ε ℓ : ℝ} (hC : 1 ≤ C) (hc0 : 0 < c) (hc : c ≤ min (1 / 8) (min (1 / (8192 * C ^ 6)) (1 / 19200))) (hε0 : 0 < ε) (hε1 : ε ≤ 1) (hℓ : 0 ≤ ℓ) : c * ε ^ 7 / (ε + ℓ) ≤ c * ε ^ 6 ∧ c * ε ^ 7 / (ε + ℓ) ≤ ε / 8 ∧ 0 < ε / (4 * C) ∧ ε / (4 * C) ≤ 1

Constant choice (node 1.5.1; 07_main_theorem.tex, eqs universal-c-choice, gamma-xi-choice, gamma-greedy-condition): for C ≥ 1, c ≤ min{1/8, 1/(8192 C⁶), 1/19200}, 0 < ε ≤ 1, ℓ ≥ 0, the choices γ = c ε⁷/(ε + ℓ) and ξ = ε/(4C) satisfy the downstream hypotheses: γ ≤ c ε⁶ ≤ ε/8 and 0 < ξ ≤ 1.

theorem CommutingRepetition.counterexample_extraction {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (G : Game X Y A B) (n : ℕ) {γ : ℝ} (hsup : Real.exp (-(γ * ↑n)) < (G.repeat n).omegaCO) : ∃ (Trep : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)), Real.exp (-(γ * ↑n)) < (G.repeat n).win Trep.correlation

Counterexample extraction (node 1.5.2; 07_main_theorem.tex, eq alleged-repeated-counterexample and following): if the repeated value exceeds e^{−γn}, the strict tracial reduction at H = G^{⊗n}, λ = e^{−γn} yields an exact tracially embeddable repeated strategy with success still above e^{−γn}. No attainment is used.

theorem CommutingRepetition.eta_delta_bounds {c ε ℓ η Δ : ℝ} (hc0 : 0 < c) (hc : c ≤ 1 / 8) (hε0 : 0 < ε) (hε1 : ε ≤ 1) (hℓ : 0 ≤ ℓ) (hη : η ≤ 8 * (c * ε ^ 7 / (ε + ℓ)) * ((ε + ℓ) / ε)) (hΔ : Δ ≤ 16 * η) : η ≤ 8 * c * ε ^ 6 ∧ 8 * c * ε ^ 6 ≤ 1 ∧ Δ ≤ 128 * c * ε ^ 6

Pre-rounding parameter arithmetic (node 1.5.3; 07_main_theorem.tex, eq main-q-eta-delta): with γ = c ε⁷/(ε + ℓ) and c ≤ 1/8, the pre-rounding outputs satisfy η ≤ 8cε⁶ ≤ 1 and Δ ≤ 128cε⁶.

theorem CommutingRepetition.contradiction_arithmetic {C c ε η Δ w : ℝ} (hC : 1 ≤ C) (hc0 : 0 < c) (hc : c ≤ min (1 / 8) (min (1 / (8192 * C ^ 6)) (1 / 19200))) (hε0 : 0 < ε) (hε1 : ε ≤ 1) (hη0 : 0 ≤ η) (hη : η ≤ 8 * c * ε ^ 6) (hΔ0 : 0 ≤ Δ) (hΔ : Δ ≤ 128 * c * ε ^ 6) (hw : 1 - ε / 4 - C / 2 * (Δ ^ (1 / 6) + ε / (4 * C)) - 5 * √(3 * η / 2) ≤ w) : 1 - 3 * ε / 4 ≤ w

Arithmetic contradiction (node 1.5.4; 07_main_theorem.tex, eqs explicit-one-shot-lower-bound, strict-one-shot-contradiction): inserting η ≤ 8cε⁶, Δ ≤ 128cε⁶, ξ = ε/(4C) into the one-shot payoff bound w ≥ 1 − ε/4 − (C/2)(Δ^{1/6} + ξ) − 5√(3η/2) forces w ≥ 1 − 3ε/4: the three displayed losses are at most ε/4, ε/8, ε/8 by the constraints (128c)^{1/6} ≤ 1/(2C), (C/2)ξ = ε/8, 5√(12c) ≤ 1/8.

theorem CommutingRepetition.predicate_case : ∃ (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), G.IsPredicate → ∀ (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)

The predicate case (node 1.5; 07_main_theorem.tex sec 7.3): the uniform repetition bound for games whose payoff is a predicate. If ω^co(G^{⊗n}) > e^{−γn} then nodes 1.1, 1.2, 1.3, 1.4 produce a legal one-shot strategy with win_G ≥ 1 − 3ε/4 > 1 − ε = ω^co(G), contradicting the definition of the supremum (attainment of neither value is needed).