theorem CommutingRepetition.rational_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), (∀ (x : X) (y : Y) (a : A) (b : B), ∃ (r : ℚ), G.payoff x y a b = ↑r) → ∀ (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 rational-payoff case (node 1.6.2; 07_main_theorem.tex sec 7.4): the uniform repetition bound for games with rational payoff tables in [0,1], for some universal constant. (The manuscript's constant-sharing with the predicate case is not encoded by this second ∃ c — the same weaker-but-true packaging as DIFFERENCES.md D2; the predicate case's constant does work, since the private-coin argument keeps every estimate's constants unchanged.) The referee declares acceptance per coordinate with a fresh private coin of bias V(aᵢ, bᵢ | xᵢ, yᵢ); the coins are never revealed, so no effect, sampler, or label may depend on them, and the predicate machinery runs with the core indicator replaced by the weight w_D ∈ [0,1] (eq private-coin-core-weight), the accepted-word budget by the weighted entropy inequality w·H₁(a) ≤ H₁(w·a) plus log-sum (eq weighted-accepted-word-entropy), and the history budget by data processing from the private-coin space.