Core Chan–He hashing and recursion data

Direct adaptation of PaperStatements.lean, lines 1242–1365, from anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. These are finite mathematical constructions, not a native RAM implementation.

Main definitions

• coll, heavy: collision counts and elements sharing a residue class.
• firstP, secondP, modulus: deterministic minimum-prime searches.
• arrXY, arrZ: light-element convolution arrays with signed padding.
• nodes, reduction: a finite ternary recursion tree at explicit parameters.

References

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

Collisions and heavy elements

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

The number of ordered pairs of distinct elements of S that are congruent modulo M.

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

The elements of S that share their residue modulo M with another element of S. They play the role of the bad elements of [CH20]. The elements alone in their residue class modulo M are called light below; they play the role of the good elements of [CH20].

The arrays of one node

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

The elements of S with remainder r modulo M.

def Cslib.Algorithms.ThreeSum.ChanHe.arr (S : Finset ℤ) (M : ℕ) (pad : ℤ) (i : ℕ) : ℤ

The array of the light elements of S. Cell i holds the element of the bucket of i if that bucket has exactly one element, and the padding value pad otherwise.

def Cslib.Algorithms.ThreeSum.ChanHe.pad (U : ℕ) : ℤ

The padding value 2U + 1. It is too large to take part in a solution among numbers of absolute value at most U.

def Cslib.Algorithms.ThreeSum.ChanHe.arrXY (S : Finset ℤ) (M U : ℕ) : ℕ → ℤ

The array made from the first or the second set of a node.

def Cslib.Algorithms.ThreeSum.ChanHe.arrZ (S : Finset ℤ) (M U k : ℕ) : ℤ

The third array of a node. A light element c of S is written as -c into the two cells r and r + M, where r is the remainder of -c. All other cells, and all cells from 2M on, hold -pad U.

The choice of the modulus

def Cslib.Algorithms.ThreeSum.ChanHe.minOrOne (T : Finset ℕ) : ℕ

The least element of a finite set of natural numbers, and 1 if the set is empty.

def Cslib.Algorithms.ThreeSum.ChanHe.firstP (Q : Finset ℕ) (Λ : ℕ) (S₁ S₂ S₃ : Finset ℤ) : ℕ

The first prime: the least p in Q modulo which each of the three sets has at most 3Λ|S|²/|Q| colliding pairs. Here and below, Q is the set of candidate primes, and Λ bounds how many of them divide a nonzero difference of two elements. reduction takes the primes up to mPar n U for Q, and labelBits U for Λ.

def Cslib.Algorithms.ThreeSum.ChanHe.secondP (Q : Finset ℕ) (Λ : ℕ) (S₁ S₂ S₃ : Finset ℤ) (p : ℕ) : ℕ

The second prime, given the first: the least q in Q such that, in each of the three sets, at most the fraction 3Λ/|Q| of the pairs that collide modulo p still collide modulo pq.

def Cslib.Algorithms.ThreeSum.ChanHe.modulus (Q : Finset ℕ) (Λ : ℕ) (S₁ S₂ S₃ : Finset ℤ) : ℕ

The modulus of a node: the product of the two primes.

The recursion tree

structure Cslib.Algorithms.ThreeSum.ChanHe.Node : Type

A node of the recursion tree: three sets and the modulus chosen for them.

• S₁ : Finset ℤ

  The first set.

• S₂ : Finset ℤ

  The second set.

• S₃ : Finset ℤ

  The third set.

• M : ℕ

  The modulus.

def Cslib.Algorithms.ThreeSum.ChanHe.instDecidableEqNode.decEq (x✝ x✝¹ : Node) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.ThreeSum.ChanHe.instDecidableEqNode : DecidableEq Node

def Cslib.Algorithms.ThreeSum.ChanHe.nodes (Q : Finset ℕ) (Λ : ℕ) : ℕ → Finset ℤ → Finset ℤ → Finset ℤ → List Node

The nodes on the first f levels of the recursion tree with root (S₁, S₂, S₃); for f = 0 there are none. A triple with an empty set is not a node and has no children. Any other triple is a node, and each of its three children replaces one of the sets by its heavy elements.

The parameters

def Cslib.Algorithms.ThreeSum.ChanHe.height (n : ℕ) : ℕ

⌈log₂(⌊log₂ n⌋ + 2)⌉. In the recursion tree of reduction n U, for three sets of at most n ≥ 1 elements each, all of absolute value at most U (the hypotheses of the library's lemma ChanHe.reduction_correct), a set is empty after this many replacements by its heavy elements.

def Cslib.Algorithms.ThreeSum.ChanHe.fuel (n : ℕ) : ℕ

The number of levels of the recursion tree that are built. Under the hypotheses named at height, each of the three sets of a node has been replaced at most height n - 1 times, because it is not empty. So a node has at most 3 (height n - 1) nodes above it.

def Cslib.Algorithms.ThreeSum.ChanHe.wPar (n U : ℕ) : ℕ

The number of primes that we want to choose from.

def Cslib.Algorithms.ThreeSum.ChanHe.mPar (n U : ℕ) : ℕ

The bound m on the primes. There are at least wPar n U primes up to m (the library's lemma ChanHe.wPar_le_card_primesLE).

The reduction for three sets

def Cslib.Algorithms.ThreeSum.ChanHe.reduction (n U : ℕ) (S₁ S₂ S₃ : Finset ℤ) : List Node

The reduction for three sets. Here n is an upper bound on the sizes of the three sets and U on the absolute values of their elements; both stay fixed through the recursion. The result is a list of nodes. The Convolution-3SUM instance of a node ν consists of the arrays arrXY ν.S₁ ν.M U, arrXY ν.S₂ ν.M U and arrZ ν.S₃ ν.M U, read at any length N ≥ 2 * mPar n U ^ 2.

def Cslib.Algorithms.ThreeSum.ChanHe.Node.Conv (ν : Node) (U N : ℕ) : Prop

The three-array convolution instance attached to a recursion node.