Soundness of repeated tailored verifiers

The soundness half of paper II's thm:repetition (II:11103) in the direct form of the plan (planning/aldous-lyons-track.md, Phase 2): the repeated verifier's game accepts, through the coordinates of its answers, only what the direct repetition of 𝒱_n's bipartite game accepts (MIPRE.Tailored.TailoredVerifier.RepSpec.accepts_of_accepts), so its value is at most that game's (MIPRE.quantumValue_le_of_coarse), which the vendored direct repetition theorem bounds (MIPRE.Repetition.quantumValue_repeat_le_soundBound). The answers of 𝒱_n's bipartite game have length at most 2B when the input's lengths are at most B, and the factor 2 is absorbed into the constant: soundBound c ε k (2B) ≤ soundBound (c / 2) ε k B.

theorem MIPRE.Repetition.soundBound_mono {c ε : ℝ} (hc : 0 ≤ c) (hε : 0 ≤ ε) (k : ℕ) {B B' : ℕ} (hB : B ≤ B') : soundBound c ε k B ≤ soundBound c ε k B'

The soundness bound grows with the answer length.

theorem MIPRE.Repetition.soundBound_two_mul {c ε : ℝ} (hc : 0 ≤ c) (hε : 0 ≤ ε) (k B : ℕ) : soundBound c ε k (2 * B) ≤ soundBound (c / 2) ε k B

Doubling the answer length halves the constant.

theorem MIPRE.Tailored.TailoredVerifier.maxLen_le_of_lenBound {ℓ : ℕ} {V : TailoredVerifier ℓ} {n B : ℕ} (hB : LenBound V.len n B) : (V.tgame n).maxLen ≤ 2 * B

The answers of 𝒱_n's bipartite game have length at most 2B when the answer-length calculator's outputs are at most B.

theorem MIPRE.Tailored.TailoredVerifier.RepSpec.valStar_le_repeat {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam tau : ℕ} {L P : Decider} {n : ℕ} (h : V.RepSpec lam tau L P n) : (V.repTV lam tau L P).valStar n ≤ quantumValue ((V.tgame n).toGame.repeat (K lam tau n))

The repeated verifier's value is at most that of the direct repetition of 𝒱_n.

theorem MIPRE.Tailored.TailoredVerifier.RepSpec.valStar_le {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam tau : ℕ} {L P : Decider} {n : ℕ} (h : V.RepSpec lam tau L P n) {B : ℕ} {ε : ℝ} (hε : 0 < ε) (hB : LenBound V.len n B) (hV : V.valStar n ≤ 1 - ε) : (V.repTV lam tau L P).valStar n ≤ Repetition.soundBound (Repetition.repConst / 2) ε (K lam tau n) B

Soundness of the repeated verifier: for an input whose lengths are at most B, val*(𝒱_n) ≤ 1 - ε gives val*(𝒱^rep_n) ≤ exp(-(c/2) ε^13 k(n) / (B + 1)), with c the constant of the direct repetition theorem for answers of bounded length.