Reed Solomon multilinear Correlated Agreement Nat

theorem reedSolomon_multilinearCorrelatedAgreement_Nat [Nontrivial (ReedSolomon.code α k)]    {e : ℕ} (hk : k ≤ Fintype.card ι)    (he : e ≤ (Code.uniqueDecodingRadius (C := (ReedSolomon.code α k : Set (ι → A))))) :    ∀ (ϑ : ℕ), (hϑ_gt_0 : ϑ > 0) → δ_ε_multilinearCorrelatedAgreement_Nat (F := A) (A := A)      (ι := ι) (C := (ReedSolomon.code α k : Set (ι → A)))      (ϑ := ϑ) (e := e) (ε := Fintype.card ι) := by    set n := Fintype.card ι    intro ϑ hϑ_gt_0 u h_prob_tensor_gt    set C_RS: ModuleCode ι A A := ReedSolomon.code α k    have h_dist_RS := ReedSolomon.dist_eq_of_le (F := A) (α := α)      (n := k) (ι := ι) (h := hk)    have h_dist_CRS : ‖(C_RS : Set (ι → A))‖₀ = n - k + 1 := h_dist_RS    -- 1. Apply ReedSolomon_ProximityGapAffineLines_UniqueDecoding (BCIKS20 Thm 4.1)    have h_fincard_n : Fintype.card (ι) = n := by rfl    have h_affine_gap_base : e_ε_correlatedAgreementAffineLinesNat (F := A) (A := A) (ι := ι)      (C := C_RS) (e := e) (ε := n) := by      let res := ReedSolomon_ProximityGapAffineLines_UniqueDecoding (A := A)        (hk := by omega) (e := e) he      rw [h_fincard_n] at res      exact res    -- 2. Check condition ε ≥ e + 1 for Theorem 3.1    have h_eps_ge_e1 : n ≥ e + 1 := by      simp only [uniqueDecodingRadius] at he      simp_rw [h_dist_CRS] at he      simp only [add_tsub_cancel_right] at he      rw [ge_iff_le];      apply Nat.le_of_lt_succ;      have h_lt : e + 1 < (n - k) / 2 + 1 + 1 := by omega      have h_le : (n - k) / 2 + 1 ≤ n := by        exact Nat.sub_div_two_add_one_le n k hk      omega    -- 3. Apply Theorem 3.1 inductively (or just state it's needed for Thm 3.6)    have h_affine_gap_interleaved : ∀ m, (hm: m ≥ 1) →        letI : Nonempty (Fin m × (ι)) := by          apply nonempty_prod.mpr          constructor          · exact Fin.pos_iff_nonempty.mp hm          · omega        e_ε_correlatedAgreementAffineLinesNat          (F := A) (A := InterleavedSymbol A (Fin m)) (ι := ι) (C := C_RS ^⋈ (Fin m))          e (Fintype.card (ι)) := by      intro m hm      let res := affine_gaps_lifted_to_interleaved_codes (MC := C_RS)        (F := A) (A := A) (hε := h_eps_ge_e1) (e := e)        (m := m) (hProximityGapAffineLines := h_affine_gap_base) (he := he)      rw [h_fincard_n]      exact res    -- 4. Apply Theorem 3.6 (AER24)    let RS_tensor_gap := interleaved_affine_gaps_imply_tensor_gaps      (MC := C_RS) (h_interleaved_gaps := by      rw [h_fincard_n] at h_affine_gap_interleaved      exact h_affine_gap_interleaved) h_affine_gap_base    exact RS_tensor_gap ϑ hϑ_gt_0 u h_prob_tensor_gt