Stir rbr soundness

theorem stir_rbr_soundness    [SampleableType F] {s : ℕ}    {P : Params ι F}    [h_nonempty : ∀ i : Fin (M + 1), Nonempty (ι i)]    {hParams : ParamConditions ι P} {Dist : Distances M}    {Codes : CodeParams ι P Dist}    (hδ₀ : Dist.δ 0 < (1 - Bstar (rate (code (P.φ 0) P.deg))))    (hδᵢ : ∀ {j : Fin (M + 1)}, j ≠ 0 →        Dist.δ j < (1 - rate (code (P.φ j) (degree ι P j))          - 1 / Fintype.card (ι j) : ℝ) ∧        Dist.δ j < (1 - Bstar (rate (code (P.φ j) (degree ι P j)))))    (ε_fold : ℝ≥0) (ε_out : Fin M → ℝ≥0) (ε_shift : Fin M → ℝ≥0) (ε_fin : ℝ≥0) :    ∃ n : ℕ,    -- There exists an `n`-message vector IOPP,    ∃ vPSpec : ProtocolSpec.VectorSpec n,    -- such that there are `2 * M + 2` challenges from the verifier to the prover,    Fintype.card (vPSpec.ChallengeIdx) = 2 * M + 2 ∧    -- ∃ vector IOPP π with the aforementioned `vPSpec`, and for    -- `Statement = Unit, Witness = Unit, OracleStatement(ι₀, F)` such that    ∃ π : VectorIOP Unit (OracleStatement (ι 0) F) Unit vPSpec F,    let ε_rbr : vPSpec.ChallengeIdx → ℝ≥0 :=      fun _ => ({ε_fold} ∪ {ε_fin} ∪ univ.image ε_out ∪ univ.image ε_shift).max' (by simp)    (IsSecureWithGap (stirRelation (degree ι P 0) (P.φ 0) 0)                    (stirRelation (degree ι P 0) (P.φ 0) (Dist.δ 0))                    ε_rbr π) ∧    -- `ε_fold ≤ errStar(degree₀/foldingParam₀, ρ₀, δ₀, repeatParam₀)`      ε_fold ≤ proximityError F (P.deg / P.foldingParam 0) (rate (code (P.φ 0) P.deg))                 (Dist.δ 0) (P.repeatParam 0)      ∧      -- Note here that `j : Fin M`, so we need to cast into `Fin (M + 1)` for indexing of      -- `Dist.δ` and `P.repeatParam`. To get `j`, we use `.castSucc`, whereas to get `j + 1`,      -- we use `.succ`.      -- Because of the difference in indexing between the paper and the code, we essentially have      -- `j = i - 1` compared to the paper.      -- `ε_out_{j+1} ≤ l_{j+1}²/2 * (degree_{j+1}/ |F| - |ι_{j+1}|)^s`      ∀ {j : Fin M} (hⱼ : j.val ≠ 0),        ε_out j ≤ ((Dist.l j.succ : ℝ) ^ 2 / 2) *          ((degree ι P j.succ : ℝ) / (Fintype.card F - Fintype.card (ι j.succ))) ^ s        ∧        -- `ε_shift_{j+1} ≤ (1 - δ_j)^repeatParam_j`        -- `+ errStar(degree_{j+1}, ρ_{j+1}, δ_{j+1}, repeatParam_j + s)`        -- `+ errStar(degree_{j+1}/foldingParam_{j+1}, ρ_{j+1}, δ_{j+1}, repeatParam_{j+1})`        ε_shift j ≤          (1 - Dist.δ j.castSucc) ^ (P.repeatParam j.castSucc)  +          -- proximityError(degreeⱼ, ρ(codeⱼ), δⱼ, repeatParam_j + s), where codeⱼ = code φⱼ degreeⱼ           proximityError F (degree ι P j.succ) (rate (code (P.φ j.succ) (degree ι P j.succ)))            (Dist.δ j.succ) (P.repeatParam j.castSucc) + s +          -- proximityError(degreeⱼ / foldingParamⱼ, ρ(codeⱼ), δⱼ, repeatParamⱼ)           proximityError F ((degree ι P j.succ) / P.foldingParam j.succ)            (rate (code (P.φ j.succ) (degree ι P j.succ)))            (Dist.δ j.succ) (P.repeatParam j.succ)        ∧        -- `ε_fin ≤ (1 - δ_M)^repeatParam_M`        ε_fin ≤ (1 - Dist.δ (Fin.last M)) ^ (P.repeatParam (Fin.last M))  :=