Proximity Gaps in Interleaved Codes

This file formalizes the main results from the paper "Proximity Gaps in Interleaved Codes" by Diamond and Gruen (DG25).

Main Definitions

The core results from DG25 are the following:

1. affine_gaps_lifted_to_interleaved_codes: Theorem 3.1 (DG25): If a linear code C has proximity gaps for affine lines (up to unique decoding radius), then its interleavings C^m also do.
2. interleaved_affine_gaps_imply_tensor_gaps: Theorem 3.6 (AER24): If all interleavings C^m have proximity gaps for affine lines, then C exhibits tensor-style proximity gaps.
3. reedSolomon_multilinearCorrelatedAgreement_Nat, reedSolomon_multilinearCorrelatedAgreement: Corollary 3.7 (DG25): Reed-Solomon codes exhibit tensor-style proximity gaps (up to unique decoding radius).

This formalization assumes the availability of Theorem 2.2 (Ben+23 / BCIKS20 Thm 4.1) stating that Reed-Solomon codes have proximity gaps for affine lines up to the unique decoding radius.

TODOs

• Conjecture 4.3 proposes ε=n might hold for general linear codes.

References

• [DG25] Benjamin E. Diamond and Angus Gruen. “Proximity Gaps in Interleaved Codes”. In: IACR Communications in Cryptology 1.4 (Jan. 13, 2025). issn: 3006-5496. doi: 10.62056/a0ljbkrz.

• [AER24] Guillermo Angeris, Alex Evans, and Gyumin Roh. A Note on Ligero and Logarithmic Randomness. Cryptology ePrint Archive, Paper 2024/1399. 2024. url: https://eprint.iacr.org/2024/1399.

def affineLineEvaluation {ι : Type l} {A : Type w} [AddCommMonoid A] {F : Type v} [Ring F] [Module F A] (u₀ u₁ : Code.Word A ι) (r : F) : Code.Word A ι

Evaluation of an affine line across u₀ and u₁ at a point r

def e_ε_correlatedAgreementAffineLinesNat {A : Type w} [DecidableEq A] [AddCommMonoid A] {F : Type} [Ring F] [Fintype F] {ι : Type u_1} [Fintype ι] [Nonempty ι] [DecidableEq ι] [Module F A] (C : Set (ι → A)) (e ε : ℕ) : Prop

theorem dist_affineCombination_le_dist_interleaved₂ {ι : Type l} [Fintype ι] {A : Type w} [DecidableEq A] [AddCommMonoid A] {F : Type} [Ring F] [Module F A] (u₀ u₁ v₀ v₁ : Code.Word A ι) (r : F) : Δ₀(affineLineEvaluation u₀ u₁ r, affineLineEvaluation v₀ v₁ r) ≤ Δ₀(u₀⋈₂u₁, v₀⋈₂v₁)

Lemma: Distance of Affine Combination is Bounded by Interleaved Distance

def δ_ε_multilinearCorrelatedAgreement_Nat {A : Type w} [DecidableEq A] [AddCommMonoid A] {F : Type} [Fintype F] [CommRing F] {ι : Type u_1} [Fintype ι] [Nonempty ι] [DecidableEq ι] [Module F A] (C : Set (ι → A)) (ϑ e ε : ℕ) : Prop

def multilinearCombine_affineLineEvaluation {ι : Type l} {A : Type w} [AddCommMonoid A] {F : Type} [CommRing F] [Module F A] {ϑ : ℕ} (U₀ U₁ : Code.WordStack A (Fin (2 ^ ϑ)) ι) (r : Fin ϑ → F) (r_affine_combine : F) : Code.Word A ι

def splitHalfRowWiseInterleavedWords {ι : Type l} {A : Type w} {ϑ : ℕ} (u : Code.WordStack A (Fin (2 ^ (ϑ + 1))) ι) : Code.WordStack A (Fin (2 ^ ϑ)) ι × Code.WordStack A (Fin (2 ^ ϑ)) ι

def mergeHalfRowWiseInterleavedWords {ι : Type l} {A : Type w} {ϑ : ℕ} (u₀ u₁ : Code.WordStack A (Fin (2 ^ ϑ)) ι) : Code.WordStack A (Fin (2 ^ (ϑ + 1))) ι

theorem eq_splitHalf_iff_merge_eq {ι : Type l} {A : Type w} {ϑ : ℕ} (u : Code.WordStack A (Fin (2 ^ (ϑ + 1))) ι) (u₀ u₁ : Code.WordStack A (Fin (2 ^ ϑ)) ι) : u₀ = (splitHalfRowWiseInterleavedWords u).1 ∧ u₁ = (splitHalfRowWiseInterleavedWords u).2 ↔ mergeHalfRowWiseInterleavedWords u₀ u₁ = u

theorem CA_split_rowwise_implies_CA {ι : Type l} [Fintype ι] {A : Type w} [DecidableEq A] (C : Set (Code.Word A ι)) {ϑ : ℕ} (u : Code.WordStack A (Fin (2 ^ (ϑ + 1))) ι) (e : ℕ) : have U₀ := (splitHalfRowWiseInterleavedWords u).1; have U₁ := (splitHalfRowWiseInterleavedWords u).2; Code.jointProximityNat₂ (Code.CodeInterleavable.interleaveCode C (Fin (2 ^ ϑ))) (⋈|U₀) (⋈|U₁) e → Code.jointProximityNat C u e

NOTE: This could be generalized to 2 * N instead of 2 ^ (ϑ + 1). Also, this can be proved for ↔ instead of →.

theorem multilinearCombine_recursive_form {ι : Type l} {A : Type w} [AddCommMonoid A] {F : Type} [CommRing F] [Module F A] {ϑ : ℕ} (u : Code.WordStack A (Fin (2 ^ (ϑ + 1))) ι) (r : Fin (ϑ + 1) → F) : have U₀ := (splitHalfRowWiseInterleavedWords u).1; have U₁ := (splitHalfRowWiseInterleavedWords u).2; have r_init := Fin.init r; multilinearCombine u r = multilinearCombine (affineLineEvaluation U₀ U₁ (r (Fin.last ϑ))) r_init

[⊗_{i=0}^{ϑ-1}(1-r_i, r_i)] · [ - u₀ -; ...; - u_{2^ϑ-1} - ] - [⊗_{i=0}^{ϑ-2}(1-r_i, r_i)] · ([(1-r_{ϑ-1}) · U₀] + [r_{ϑ-1} · U₁])

theorem multilinearCombine₁_eq_affineLineEvaluation {ι : Type l} {A : Type w} [AddCommMonoid A] {F : Type} [CommRing F] [Module F A] (u : Fin 2 → Code.Word A ι) (r : Fin 1 → F) : multilinearCombine u r = affineLineEvaluation (u 0) (u 1) (r 0)