Convolution-3SUM reduces to Exact Triangle

This directly adapts Anthropic's pinned reduction, after the reduction cited there as [VassilevskaWilliamsWilliams2013, Theorem 4.3]. The theorem number is taken from that source. No machine, machine simulation, or subquadratic time bound is asserted here. The native graph-weight construction is developed separately.

An input has a solution when x i + x j = x (i + j) for some i + j < N; indices may repeat. Indices start at zero: for nonempty input, x 0 = 0 alone gives the solution i = j = 0. This differs from ordinary 3SUM, which requires three distinct positions. For N < t * t, construct 2 * t tripartite instances with t vertices per part. Invalid indices receive 2 * U + 1, preventing them from creating zero triangles when input magnitudes are at most U.

Main definitions

• Convolution: the one-array Convolution-3SUM predicate.
• pick: read a signed in-range index or use a filler.
• weightAB, weightBC, weightAC: the three matrices of instance s.

Main results

• convolution_iff: correctness of the explicit reduction for N < t * t.
• convolution_iff_sqrt: the choice t = Nat.sqrt N + 1.
• weights_abs_le: all generated weights have magnitude at most 2 * U + 1.

References

• V. Vassilevska Williams and R. Williams, Finding, minimizing, and counting weighted subgraphs

def Cslib.Algorithms.ThreeSum.Convolution (N : ℕ) (x : ℕ → ℤ) : Prop

One-array Convolution-3SUM, allowing repeated indices. Only the first N entries matter.

def Cslib.Algorithms.ThreeSum.pick (N : ℕ) (x : ℕ → ℤ) (fill z : ℤ) : ℤ

A signed index selects an input entry exactly when it lies in [0, N).

theorem Cslib.Algorithms.ThreeSum.pick_nat (N : ℕ) (x : ℕ → ℤ) (fill : ℤ) (i : ℕ) : pick N x fill ↑i = if i < N then x i else fill

A nonnegative index uses the usual natural-number bounds check.

theorem Cslib.Algorithms.ThreeSum.pick_sub (N : ℕ) (x : ℕ → ℤ) (fill : ℤ) (a b : ℕ) : pick N x fill (↑a - ↑b) = if b ≤ a ∧ a - b < N then x (a - b) else fill

Signed subtraction rejects negative indices before converting them to naturals.

def Cslib.Algorithms.ThreeSum.weightAB {t : ℕ} (N : ℕ) (x : ℕ → ℤ) (fill : ℤ) (a b : Fin t) : ℤ

The edge (a,b) represents the input index a*t+b.

def Cslib.Algorithms.ThreeSum.weightBC {t : ℕ} (N s : ℕ) (x : ℕ → ℤ) (fill : ℤ) (b c : Fin t) : ℤ

The edge (b,c) represents the signed index c*t+s-b.

def Cslib.Algorithms.ThreeSum.weightAC {t : ℕ} (N s : ℕ) (x : ℕ → ℤ) (fill : ℤ) (a c : Fin t) : ℤ

The edge (a,c) negates the entry at (a+c)*t+s, using positive filler if invalid.

theorem Cslib.Algorithms.ThreeSum.weightAB_eq_pick {t : ℕ} (N : ℕ) (x : ℕ → ℤ) (fill : ℤ) (a b : Fin t) : weightAB N x fill a b = pick N x fill ↑(↑a * t + ↑b)

Matrix AB is implemented by a guarded signed-index read.

theorem Cslib.Algorithms.ThreeSum.weightBC_eq_pick {t : ℕ} (N s : ℕ) (x : ℕ → ℤ) (fill : ℤ) (b c : Fin t) : weightBC N s x fill b c = pick N x fill (↑(↑c * t + s) - ↑↑b)

Matrix BC is implemented by a guarded signed-index read, with a possibly negative index.

theorem Cslib.Algorithms.ThreeSum.weightAC_eq_pick {t : ℕ} (N s : ℕ) (x : ℕ → ℤ) (fill : ℤ) (a c : Fin t) : weightAC N s x fill a c = -pick N x (-fill) ↑((↑a + ↑c) * t + s)

Matrix AC reads with negative filler before negating, retaining positive invalid weights.

theorem Cslib.Algorithms.ThreeSum.weights_abs_le {t N s : ℕ} {x : ℕ → ℤ} {U : ℤ} (hU : 0 ≤ U) (hx : ∀ (i : ℕ), i < N → |x i| ≤ U) (a b c : Fin t) : |weightAB N x (2 * U + 1) a b| ≤ 2 * U + 1 ∧ |weightBC N s x (2 * U + 1) b c| ≤ 2 * U + 1 ∧ |weightAC N s x (2 * U + 1) a c| ≤ 2 * U + 1

Every edge is either an input entry up to sign, or the filler.

theorem Cslib.Algorithms.ThreeSum.convolution_iff {t N : ℕ} {x : ℕ → ℤ} {U : ℤ} (hU : 0 ≤ U) (hNt : N < t * t) (hx : ∀ (i : ℕ), i < N → |x i| ≤ U) : Convolution N x ↔ ∃ (s : ℕ), s < 2 * t ∧ ExactTriangle.HasZeroTriangle (weightAB N x (2 * U + 1)) (weightBC N s x (2 * U + 1)) (weightAC N s x (2 * U + 1))

The explicit reduction is correct for every input size, including zero. There are 2*t instances and exactly t vertices in each of their three parts.

theorem Cslib.Algorithms.ThreeSum.convolution_iff_sqrt {N : ℕ} {x : ℕ → ℤ} {U : ℤ} (hU : 0 ≤ U) (hx : ∀ (i : ℕ), i < N → |x i| ≤ U) : Convolution N x ↔ ∃ (s : ℕ), s < 2 * (N.sqrt + 1) ∧ ExactTriangle.HasZeroTriangle (weightAB N x (2 * U + 1)) (weightBC N s x (2 * U + 1)) (weightAC N s x (2 * U + 1))

Taking t = ⌊√N⌋+1 gives 2*t instances with t vertices per part.