theorem CommutingRepetition.Game.prod_law_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {ι : Type} [Fintype ι] [DecidableEq ι] (G : Game X Y A B) : ∑ xs : ι → X, ∑ ys : ι → Y, ∏ j : ι, G.questionWeight (xs j) (ys j) = 1

The product question law over any finite index set is normalized.

theorem CommutingRepetition.Game.answer_collapse {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (i : Fin n) (x : X) (y : Y) (c : (Fin n → A) → (Fin n → B) → ℝ) : (∑ a : A, ∑ b : B, G.payoff x y a b * ∑ as : Fin n → A, ∑ bs : Fin n → B, if as i = a then if bs i = b then c as bs else 0 else 0) = ∑ as : Fin n → A, ∑ bs : Fin n → B, G.payoff x y (as i) (bs i) * c as bs

Collapsing the one-shot answer pair against the coordinate-i indicator of the marginalized effects.

theorem CommutingRepetition.Game.presample_change_of_variables {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (i : Fin n) (G : Game X Y A B) (g : (Fin n → X) → (Fin n → Y) → ℝ) : ∑ rx : { j : Fin n // j ≠ i } → X, ∑ ry : { j : Fin n // j ≠ i } → Y, ∑ x : X, ∑ y : Y, (∏ j : { j : Fin n // j ≠ i }, G.questionWeight (rx j) (ry j)) * G.questionWeight x y * g ((Equiv.funSplitAt i X).symm (x, rx)) ((Equiv.funSplitAt i Y).symm (y, ry)) = ∑ w : Fin n → X, ∑ v : Fin n → Y, (∏ j : Fin n, G.questionWeight (w j) (v j)) * g w v

Presampling change of variables: sampling the off-i coordinates from the product law and the live pair from μ reproduces the full product law.

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.