One node and the three-set recursion in the Chan–He reduction

This file proves that the reduction for three sets, reduction n U, is correct and makes polylogarithmically many instances, following [ChanHe2020, Theorem 5.1]. A node of the recursion tree consists of three sets and a modulus M.

• One node. The elements that are alone in their residue class modulo M are called light. The first two arrays hold each light element of the first two sets at the index of its remainder. The third array holds -c, for each light element c of the third set, at the remainder of -c and once more M cells further on. All other cells hold padding. Padding is too large to take part in a solution, and a + b + c = 0 makes the remainders of a and b add up to that of -c, or to that plus M. So the Convolution-3SUM instance of the node has a solution iff the light elements of the three sets have a 3SUM solution (node_correct).
• The recursion. A 3SUM solution consists of three light elements, or one of its elements is heavy (hasSol_split). The three children of a node replace one set each by its heavy elements.
• The depth. A set that has been replaced j times has at most n / d_j elements, where d₀ = 1 and d_{j+1} = 2 d_j² (Replaced.heavy). Since d_j > n for j = height n (lt_dSeq_height), it is then empty (Replaced.eq_empty), so no node lies below the fuel n levels of the tree that are built. This gives nodes_correct, by induction on the number of levels, and reduction_correct, whose hypotheses on the three sets are collected in Admissible.
• The size. A ternary tree with fuel n levels has at most 3 ^ fuel n ≤ (2⌊log₂ n⌋ + 2)⁵ nodes (length_reduction_le). The entries of the arrays are bounded in abs_arrXY_le and abs_arrZ_le, and the count for the searches of one node in scan_node_le.

Directly adapted from Recursion.lean at the pinned anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5.

Main results

• reduction_correct, length_reduction_le: correct reduction and polylogarithmic node count.

References

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

Light elements and the cells of the arrays

def Cslib.Algorithms.ThreeSum.ChanHe.light (S : Finset ℤ) (M : ℕ) : Finset ℤ

The elements of S that are alone in their residue class modulo M. They play the role of the good elements of [CH20].

theorem Cslib.Algorithms.ThreeSum.ChanHe.light_subset (S : Finset ℤ) (M : ℕ) : light S M ⊆ S

Light elements are elements.

theorem Cslib.Algorithms.ThreeSum.ChanHe.heavy_subset (S : Finset ℤ) (M : ℕ) : heavy S M ⊆ S

Heavy elements are elements.

theorem Cslib.Algorithms.ThreeSum.ChanHe.abs_arrXY_le {S : Finset ℤ} {U : ℕ} (M : ℕ) (h : Bdd U S) (i : ℕ) : |arrXY S M U i| ≤ 2 * ↑U + 1

The entries of the array made from the first or the second set of a node have absolute value at most 2U + 1.

theorem Cslib.Algorithms.ThreeSum.ChanHe.abs_arrZ_le {S : Finset ℤ} {U : ℕ} (M : ℕ) (h : Bdd U S) (k : ℕ) : |arrZ S M U k| ≤ 2 * ↑U + 1

The entries of the third array of a node have absolute value at most 2U + 1.

One node

theorem Cslib.Algorithms.ThreeSum.ChanHe.node_correct {U M N : ℕ} (hM : 1 ≤ M) (hN : 2 * M ≤ N) {S₁ S₂ S₃ : Finset ℤ} (h₁ : Bdd U S₁) (h₂ : Bdd U S₂) (h₃ : Bdd U S₃) : HasConvolutionSolution N (arrXY S₁ M U) (arrXY S₂ M U) (arrZ S₃ M U) ↔ HasThreeSetSolution (light S₁ M) (light S₂ M) (light S₃ M)

Correctness of one node. Its Convolution-3SUM instance, read at any length N ≥ 2M, has a solution iff the light elements of the three sets have a 3SUM solution.

The sizes of the sets along the recursion

def Cslib.Algorithms.ThreeSum.ChanHe.dSeq (j : ℕ) : ℕ

The sequence d₀ = 1, d_{j+1} = 2 d_j² of [CH20], in closed form.

theorem Cslib.Algorithms.ThreeSum.ChanHe.height_pos (n : ℕ) : 1 ≤ height n

height n is at least 1, so the subtraction in fuel does not truncate.

structure Cslib.Algorithms.ThreeSum.ChanHe.Replaced (n U j : ℕ) (T : Finset ℤ) : Prop

What is known about a set T that has been replaced j times by its heavy elements: its elements have absolute value at most U, and there are at most n / d_j of them.

• bdd : Bdd U T

  The elements have absolute value at most U.

• card : T.card * dSeq j ≤ n

  There are at most n / d_j elements.

theorem Cslib.Algorithms.ThreeSum.ChanHe.Replaced.zero {n U : ℕ} {T : Finset ℤ} (hb : Bdd U T) (hc : T.card ≤ n) : Replaced n U 0 T

At the root no set has been replaced.

theorem Cslib.Algorithms.ThreeSum.ChanHe.Replaced.heavy {n U j : ℕ} {T : Finset ℤ} (h : Replaced n U j T) (hn : 1 ≤ n) {M : ℕ} (hM : 2 * n * (ChanHe.heavy T M).card ≤ T.card ^ 2) : Replaced n U (j + 1) (ChanHe.heavy T M)

One more replacement: if at most |T|²/(2n) elements of T are heavy, then these are at most n / d_{j+1}.

theorem Cslib.Algorithms.ThreeSum.ChanHe.Replaced.eq_empty {n U j : ℕ} {T : Finset ℤ} (h : Replaced n U j T) (hj : height n ≤ j) : T = ∅

After height n replacements a set is empty.

The recursion tree

theorem Cslib.Algorithms.ThreeSum.ChanHe.hasSol_split (S₁ S₂ S₃ : Finset ℤ) (M : ℕ) : HasThreeSetSolution S₁ S₂ S₃ ↔ HasThreeSetSolution (light S₁ M) (light S₂ M) (light S₃ M) ∨ (HasThreeSetSolution (heavy S₁ M) S₂ S₃ ∨ HasThreeSetSolution S₁ (heavy S₂ M) S₃) ∨ HasThreeSetSolution S₁ S₂ (heavy S₃ M)

A solution consists of three light elements, or it contains a heavy one. The brackets are those of the list of the children in nodes.

theorem Cslib.Algorithms.ThreeSum.ChanHe.length_nodes_le (Q : Finset ℕ) (Λ f : ℕ) (S₁ S₂ S₃ : Finset ℤ) : 2 * (nodes Q Λ f S₁ S₂ S₃).length + 1 ≤ 3 ^ f

The first f levels of the tree have at most (3^f - 1)/2 nodes.

theorem Cslib.Algorithms.ThreeSum.ChanHe.nodes_subset (Q : Finset ℕ) (Λ f : ℕ) (S₁ S₂ S₃ : Finset ℤ) (ν : Node) : ν ∈ nodes Q Λ f S₁ S₂ S₃ → ν.S₁ ⊆ S₁ ∧ ν.S₂ ⊆ S₂ ∧ ν.S₃ ⊆ S₃

The sets of a node are subsets of the sets at the root.

structure Cslib.Algorithms.ThreeSum.ChanHe.Candidates (n U m : ℕ) (Q : Finset ℕ) : Prop

The hypotheses on the set Q of candidates for the two searches: primes, all at most m, and enough of them for card_heavy_modulus_le.

• prime (p : ℕ) : p ∈ Q → Nat.Prime p

  The candidates are primes.

• le (p : ℕ) : p ∈ Q → p ≤ m

  The candidates are at most m.

• card : 18 * labelBits U ^ 2 * n ≤ Q.card ^ 2

  There are at least √(18n) Λ candidates.

theorem Cslib.Algorithms.ThreeSum.ChanHe.nodes_correct {n U N m : ℕ} (hn : 1 ≤ n) {Q : Finset ℕ} (hQ : Candidates n U m Q) (hN : 2 * m ^ 2 ≤ N) (f : ℕ) {T₁ T₂ T₃ : Finset ℤ} {j₁ j₂ j₃ : ℕ} (r₁ : Replaced n U j₁ T₁) (r₂ : Replaced n U j₂ T₂) (r₃ : Replaced n U j₃ T₃) (hf : 3 * height n - 2 ≤ f + j₁ + j₂ + j₃) : HasThreeSetSolution T₁ T₂ T₃ ↔ ∃ ν ∈ nodes Q (labelBits U) f T₁ T₂ T₃, ν.Conv U N

The induction behind reduction_correct. If the i-th set has been replaced j_i times, then f levels of the tree are enough as soon as f + j₁ + j₂ + j₃ ≥ 3 (height n) - 2.

The reduction for three sets

structure Cslib.Algorithms.ThreeSum.ChanHe.Admissible (n U : ℕ) (S₁ S₂ S₃ : Finset ℤ) : Prop

The hypotheses on an input of reduction n U: each of the three sets has at most n elements, all of absolute value at most U.

• card₁ : S₁.card ≤ n

  The first set has at most n elements.

• card₂ : S₂.card ≤ n

  The second set has at most n elements.

• card₃ : S₃.card ≤ n

  The third set has at most n elements.

• bdd₁ : Bdd U S₁

  The elements of the first set have absolute value at most U.

• bdd₂ : Bdd U S₂

  The elements of the second set have absolute value at most U.

• bdd₃ : Bdd U S₃

  The elements of the third set have absolute value at most U.

theorem Cslib.Algorithms.ThreeSum.ChanHe.Admissible.of_mem {n U : ℕ} {S₁ S₂ S₃ : Finset ℤ} (h : Admissible n U S₁ S₂ S₃) {ν : Node} (hν : ν ∈ reduction n U S₁ S₂ S₃) : Admissible n U ν.S₁ ν.S₂ ν.S₃

The sets of a node satisfy the hypotheses that the sets at the root satisfy.

theorem Cslib.Algorithms.ThreeSum.ChanHe.reduction_correct {n U N : ℕ} (hn : 1 ≤ n) (hN : 2 * mPar n U ^ 2 ≤ N) {S₁ S₂ S₃ : Finset ℤ} (h : Admissible n U S₁ S₂ S₃) : HasThreeSetSolution S₁ S₂ S₃ ↔ ∃ ν ∈ reduction n U S₁ S₂ S₃, ν.Conv U N

Correctness of the reduction for three sets. Let the three sets have at most n ≥ 1 elements each, all of absolute value at most U, and let N ≥ 2 * mPar n U ^ 2. Then 3SUM has a solution iff the Convolution-3SUM instance of some node has one at length N.

theorem Cslib.Algorithms.ThreeSum.ChanHe.three_pow_fuel_le (n : ℕ) : 3 ^ fuel n ≤ (2 * Nat.log 2 n + 2) ^ 5

A ternary tree with fuel n levels has polylogarithmically many nodes.

theorem Cslib.Algorithms.ThreeSum.ChanHe.length_reduction_le (n U : ℕ) (S₁ S₂ S₃ : Finset ℤ) : (reduction n U S₁ S₂ S₃).length ≤ (2 * Nat.log 2 n + 2) ^ 5

The reduction makes at most (2⌊log₂ n⌋ + 2)⁵ nodes, and each node is one instance.

theorem Cslib.Algorithms.ThreeSum.ChanHe.scan_node_le {n U : ℕ} {ν : Node} (h : Admissible n U ν.S₁ ν.S₂ ν.S₃) : 2 * (mPar n U).primesLE.card * (ν.S₁.card + ν.S₂.card + ν.S₃.card) ≤ 2 * mPar n U * (3 * n)

The two searches of a node go through at most m = mPar n U primes each, and its three sets have at most 3n elements in all. This bounds a number of pairs (candidate prime, element), not a running time.