Packing three convolution arrays into one

Adapted from Anthropic's PaperStatements.lean and FromNumbers.lean, at formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. Three-array convolution uses Definition 2.2 of [CH20]. The four-way packing is an additional elementary step in that formalization, not part of the Chan–He proof.

Main definitions

• HasConvolutionSolution: three arrays with zero-based indices and i + j < N.
• oneArray: four-way interleaving with magnitude tags.

Main results

• oneArray_correct: equivalence with the existing one-array Convolution predicate.
• abs_oneArray_le: packed magnitudes are at most 30W + 10.

References

• T. M. Chan and Q. He, Reducing 3SUM to Convolution-3SUM

def Cslib.Algorithms.ThreeSum.HasConvolutionSolution (N : ℕ) (X Y Z : ℕ → ℤ) : Prop

Three-array convolution, with zero-based indices and the requirement i + j < N.

Three arrays in one

def Cslib.Algorithms.ThreeSum.oneArray (W : ℕ) (X Y Z : ℕ → ℤ) (u : ℕ) : ℤ

Three arrays in one. With G = 3W + 1, where W bounds the entries of the three arrays, cell 4i + 1 holds X i + G, cell 4i + 2 holds Y i + 3G, cell 4i + 3 holds Z i + 4G, and cell 4i holds 10G. In an equation y_u + y_v = y_{u+v} the multiples of G have to cancel, and they do so only when u and v have the remainders 1 and 2 modulo 4.

Three arrays in one

theorem Cslib.Algorithms.ThreeSum.oneArray_correct {N W : ℕ} {X Y Z : ℕ → ℤ} (hX : ∀ (i : ℕ), i < N → |X i| ≤ ↑W) (hY : ∀ (i : ℕ), i < N → |Y i| ≤ ↑W) (hZ : ∀ (i : ℕ), i < N → |Z i| ≤ ↑W) : HasConvolutionSolution N X Y Z ↔ Convolution (4 * N) (oneArray W X Y Z)

Three arrays to one, of four times the length. Here W bounds the entries below N.

theorem Cslib.Algorithms.ThreeSum.abs_oneArray_le {N W : ℕ} {X Y Z : ℕ → ℤ} (hX : ∀ (i : ℕ), i < N → |X i| ≤ ↑W) (hY : ∀ (i : ℕ), i < N → |Y i| ≤ ↑W) (hZ : ∀ (i : ℕ), i < N → |Z i| ≤ ↑W) {u : ℕ} (hu : u < 4 * N) : |oneArray W X Y Z u| ≤ 30 * ↑W + 10

The entries of the one array have absolute value at most 30W + 10.