theorem CommutingRepetition.Game.repeat_omegaCO_le {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 : ℕ) (hn : 1 ≤ n) : (G.repeat n).omegaCO ≤ G.omegaCO

Marginal monotonicity (node 1.6.1; 07_main_theorem.tex, eq marginal-monotonicity): ω^co(G^{⊗n}) ≤ ω^co(G) for every n ≥ 1. Stated for arbitrary [0,1] payoffs — a disclosed safe-direction strengthening of the manuscript's predicate-context display (DIFFERENCES.md D11). Proof: presample the other n − 1 question pairs with shared randomness (the seed mixture of Game/Mixture.lean), play the chosen coordinate i, and marginalize the answers; the product payoff is bounded by the coordinate-i payoff since all factors lie in [0,1].

theorem CommutingRepetition.Game.abs_win_sub_win_le {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G₁ G₂ : Game X Y A B} {δ : ℝ} (hδ : 0 ≤ δ) (hμ : G₁.questionWeight = G₂.questionWeight) (hV : ∀ (x : X) (y : Y) (a : A) (b : B), |G₁.payoff x y a b - G₂.payoff x y a b| ≤ δ) {p : Correlation X Y A B} (hp : ∀ (x : X) (y : Y) (a : A) (b : B), 0 ≤ p x y a b) (hsum : ∀ (x : X) (y : Y), ∑ a : A, ∑ b : B, p x y a b ≤ 1) : |G₁.win p - G₂.win p| ≤ δ

Payoff perturbation for the winning functional (node 1.6.3; 07_main_theorem.tex, eq payoff-rational-approximation, first inequality): two games with the same question law and δ-close payoff tables give winning probabilities within δ, for any subnormalized nonnegative correlation. (hδ is needed for degenerate empty alphabets, where the payoff hypothesis is vacuous and both wins are zero.)

theorem CommutingRepetition.Game.abs_omegaCO_sub_omegaCO_le {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] {G₁ G₂ : Game X Y A B} {δ : ℝ} (hδ : 0 ≤ δ) (hμ : G₁.questionWeight = G₂.questionWeight) (hV : ∀ (x : X) (y : Y) (a : A) (b : B), |G₁.payoff x y a b - G₂.payoff x y a b| ≤ δ) : |G₁.omegaCO - G₂.omegaCO| ≤ δ

Payoff perturbation for the commuting value (node 1.6.3): δ-close payoff tables give δ-close values. ["The same bounds hold after taking commuting suprema", 07_main_theorem.tex]

theorem CommutingRepetition.Game.abs_repeat_omegaCO_sub_le {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] {G₁ G₂ : Game X Y A B} {δ : ℝ} (hδ : 0 ≤ δ) (hμ : G₁.questionWeight = G₂.questionWeight) (hV : ∀ (x : X) (y : Y) (a : A) (b : B), |G₁.payoff x y a b - G₂.payoff x y a b| ≤ δ) (n : ℕ) : |(G₁.repeat n).omegaCO - (G₂.repeat n).omegaCO| ≤ ↑n * δ

Repeated-game payoff perturbation (node 1.6.3; 07_main_theorem.tex, eq payoff-rational-approximation, second inequality, "telescoping the product"): δ-close payoff tables give n·δ-close repeated values.