Parallel repetition of normal form verifiers in the commuting-operator model

The soundness clause of thm:parallel-repetition read in ω_co (item "repetition" of Phase 2 of planning/mipco-track.md). Nothing about the verifier is new: the output's game is the repeated game in every value model (MIPRE.val_repVerifier), so soundness in a model is the game-level repetition bound in that model (MIPRE.val_repVerifier_le). What this file adds is that bound for ω_co, from the vendored uniform theorem MIPRE.Repetition.commutingOperatorValue_repeat_le (thm:direct-repetition-co):

• valco(G^{⊗k}) ≤ exp(-c ε'^7 k / (ε' + log(|𝒜||ℬ|))) with ε' = 1 - valco(G) ≥ ε; the exponent 7 is better than the tensor theorem's 13, and ε^13 ≤ ε'^7 because ε ≤ ε' ≤ 1, so the arithmetic of the tensor bound applies unchanged (Repetition.exp_le_soundBound), with its own constant repConstCo (gameSoundIn_commuting).
• One procedure must serve both models, and the structure Repetition has one constant, which the compression uses to choose the number of repetitions. So the commuting-operator reading is repetitionCo, the same procedure at the smaller of the two constants (Repetition.withConst), sound in both models (repetitionCo_soundIn_commuting; the tensor clause is its field). The main theorem keeps repetition itself, whose constant does not mention the commuting-operator theorem, so MIP* = RE does not depend on it.

noncomputable def MIPRE.Repetition.repConstCo₀ : ℝ

The universal constant of thm:direct-repetition-co.

Equations

• MIPRE.Repetition.repConstCo₀ = MIPRE.Repetition.commutingOperatorValue_repeat_le.choose

theorem MIPRE.Repetition.repConstCo₀_pos : 0 < repConstCo₀

theorem MIPRE.Repetition.commutingOperatorValue_repeat_le_spec (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) : commutingOperatorValue (G.repeat n) ≤ Real.exp (-(repConstCo₀ * ((1 - commutingOperatorValue G) ^ 7 / (1 - commutingOperatorValue G + Real.log (↑(Fintype.card A) * ↑(Fintype.card B))))) * ↑n)

noncomputable def MIPRE.Repetition.repConstCo : ℝ

The constant of the commuting-operator repetition bound for answers of bounded length: c / (1 + 2 log 3).

Equations

• MIPRE.Repetition.repConstCo = MIPRE.Repetition.repConstCo₀ / (1 + 2 * Real.log 3)

theorem MIPRE.Repetition.repConstCo_pos : 0 < repConstCo

theorem MIPRE.Repetition.commutingOperatorValue_repeat_le_soundBound {X : Type} [Fintype X] [Nonempty X] {B : ℕ} (G : Game X X (Verifier.Answers B) (Verifier.Answers B)) {ε : ℝ} (hε : 0 < ε) (hG : commutingOperatorValue G ≤ 1 - ε) {k : ℕ} (hk : 0 < k) : commutingOperatorValue (G.repeat k) ≤ soundBound repConstCo ε k B

Game-level soundness of direct repetition for commuting-operator strategies, in the form of Repetition.soundness: for a game with answers of length at most B, valco(G) ≤ 1 - ε gives valco(G^{⊗k}) ≤ exp(-c' ε^13 k / (B + 1)).

theorem MIPRE.Repetition.gameSoundIn_commuting : GameSoundIn ValueModel.commuting repConstCo

The commuting-operator model has the direct repetition bound at repConstCo.

noncomputable def MIPRE.Repetition.repConstBoth : ℝ

The constant of the procedure read in both models: the smaller of repConst and repConstCo.

Equations

• MIPRE.Repetition.repConstBoth = min MIPRE.Repetition.repConst MIPRE.Repetition.repConstCo

theorem MIPRE.Repetition.repConstBoth_pos : 0 < repConstBoth

noncomputable def MIPRE.repetitionCo (ℓ : ℕ) : Repetition ℓ

Parallel repetition of normal form verifiers for both values: repetition ℓ at the constant Repetition.repConstBoth, the smaller of the two repetition constants. It is the same procedure — sampler, decider, complexity clause and completeness are those of repetition ℓ — and its soundness clause holds in both models.

Equations

• MIPRE.repetitionCo ℓ = (MIPRE.repetition ℓ).withConst MIPRE.Repetition.repConstBoth MIPRE.Repetition.repConstBoth_pos ⋯

theorem MIPRE.repetitionCo_soundIn_commuting (ℓ : ℕ) : (repetitionCo ℓ).SoundIn ValueModel.commuting

Parallel repetition is sound in the commuting-operator model (blueprint thm:parallel-repetition-co): the procedure's soundness clause read in ω_co, from the vendored commuting-operator repetition theorem through the value-independent bridge from the verifier to the repeated game.