theorem proximity_gap {F : Type} [Field F] [Fintype F] [DecidableEq F] {ι : Type} [Fintype ι] [Nonempty ι] {φ : ι ↪ F} {degree m : ℕ} {δ : NNReal} {f : Fin m → ι → F} {GenFun : F → Fin m → F} (h : ↑δ < 1 - Bstar ↑(ρ ReedSolomon.code φ degree) → ∀ {f : Fin m → ι → F}, ↑(do let r ← PMF.uniformOfFintype F pure (↑δᵣ(fun (x : ι) => ∑ j : Fin m, GenFun r j * f j x, ↑(ReedSolomon.code φ degree)) ≤ ↑δ)) True > ENNReal.ofReal (err' F degree (↑(ρ ReedSolomon.code φ degree)) (↑δ) m)) : ∃ (S : Finset ι), ↑S.card ≥ (1 - δ) * ↑(Fintype.card ι) ∧ ∃ u ∈ ReedSolomon.code φ degree, ∀ (i : Fin m), ∀ x ∈ S, f i x = u x

Theorem 4.1[BCIKS20] from STIR[ACFY24] Let C = RS[F, ι, degree] be a ReedSolomon code with rate degree / |ι| and let Bstar(ρ) = √ρ. For all δ ∈ (0, 1 - Bstar(ρ)), f₁,...,fₘ : ι → F, if Pr_{r ← F} [ δᵣ(rⱼ * fⱼ, C) ≤ δ] > err'(degree, ρ, δ, m) then ∃ S ⊆ ι, |S| ≥ (1-δ) * |ι| and ∀ i : m, ∃ u : C, u(S)=fᵢ(S)