Choosing the modulus in the Chan–He reduction

The deterministic reduction from 3SUM to Convolution-3SUM after [ChanHe2020, Theorem 5.1] hashes the numbers by x ↦ x mod pq. It finds the two primes p and q by exhaustive search among the primes up to m = mPar n U. Both searches succeed and leave few elements badly hashed.

• An ordered pair of distinct elements of a set S collides modulo M if M divides their difference; coll S M counts these ordered pairs. An element that collides with another one is heavy. There are at most as many heavy elements as colliding pairs (card_heavy_le_coll). The count is determined by the sizes of the residue classes (coll_eq_sum); the proofs below do not need this, a program that computes the count does.
• A nonzero difference has at most Λ = labelBits U prime divisors. Summed over the candidates q in the set Q of primes, the pairs that collide modulo M₀ q number at most Λ times those that collide modulo M₀ (sum_coll_mul_le).
• Finite Markov and union bounds, as used in [CH20], show that some candidate is, for each of the three sets, at most three times as bad as the average (Finset.exists_forall_mul_card_le_mul_sum, exists_prime_coll_le). So both searches succeed (firstP_spec, secondP_spec), and the modulus pq leaves at most 9Λ²|S|²/|Q|² colliding pairs in each set S (modulus_spec).
• There are at least wPar n U primes up to mPar n U (wPar_le_card_primesLE, from the bound 2^m ≤ (m + 1) lcm(1, …, m) of Mathlib). With that many candidates a set S has at most |S|²/(2n) heavy elements (card_heavy_modulus_le, le_card_primesLE_mPar_sq).

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

Main results

• modulus_spec, card_heavy_modulus_le: successful searches and quadratic shrinking.

References

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

Colliding pairs and heavy elements

theorem Cslib.Algorithms.ThreeSum.ChanHe.natCast_dvd_sub_iff_emod_eq (M : ℕ) (x y : ℤ) : ↑M ∣ x - y ↔ x % ↑M = y % ↑M

Two integers are congruent modulo M iff they have the same remainder.

theorem Cslib.Algorithms.ThreeSum.ChanHe.card_heavy_le_coll (S : Finset ℤ) (M : ℕ) : (heavy S M).card ≤ coll S M

Each heavy element is the first component of a colliding pair.

theorem Cslib.Algorithms.ThreeSum.ChanHe.coll_le_sq (S : Finset ℤ) (M : ℕ) : coll S M ≤ S.card ^ 2

There are at most |S|² colliding ordered pairs.

theorem Cslib.Algorithms.ThreeSum.ChanHe.coll_eq_sum (S : Finset ℤ) (M : ℕ) : coll S M = ∑ x ∈ S, ((bucket S M (x % ↑M)).card - 1)

The collision count is determined by the sizes of the buckets: an element collides with the other members of its bucket.

theorem Cslib.Algorithms.ThreeSum.ChanHe.sum_coll_mul_le {Q : Finset ℕ} (hP : ∀ p ∈ Q, Nat.Prime p) {U : ℕ} {S : Finset ℤ} (hS : Bdd U S) (M₀ : ℕ) : ∑ q ∈ Q, coll S (M₀ * q) ≤ labelBits U * coll S M₀

Double counting. Summed over the candidates q ∈ Q, the pairs that collide modulo M₀ q number at most labelBits U times those that collide modulo M₀: such a pair collides modulo M₀, and q divides its difference. Coprimality of q and M₀ is not used, so the two primes of a modulus are allowed to coincide.

The two searches succeed

theorem Cslib.Algorithms.ThreeSum.ChanHe.firstP_spec {Q : Finset ℕ} {U : ℕ} {S₁ S₂ S₃ : Finset ℤ} (hQ : Q.Nonempty) (hP : ∀ p ∈ Q, Nat.Prime p) (h₁ : Bdd U S₁) (h₂ : Bdd U S₂) (h₃ : Bdd U S₃) : firstP Q (labelBits U) S₁ S₂ S₃ ∈ {p ∈ Q | coll S₁ p * Q.card ≤ 3 * labelBits U * S₁.card ^ 2 ∧ coll S₂ p * Q.card ≤ 3 * labelBits U * S₂.card ^ 2 ∧ coll S₃ p * Q.card ≤ 3 * labelBits U * S₃.card ^ 2}

The first search succeeds: firstP lies in Q and passes its three tests.

theorem Cslib.Algorithms.ThreeSum.ChanHe.secondP_spec {Q : Finset ℕ} {U : ℕ} {S₁ S₂ S₃ : Finset ℤ} (hQ : Q.Nonempty) (hP : ∀ p ∈ Q, Nat.Prime p) (h₁ : Bdd U S₁) (h₂ : Bdd U S₂) (h₃ : Bdd U S₃) (p : ℕ) : secondP Q (labelBits U) S₁ S₂ S₃ p ∈ {q ∈ Q | coll S₁ (p * q) * Q.card ≤ 3 * labelBits U * coll S₁ p ∧ coll S₂ (p * q) * Q.card ≤ 3 * labelBits U * coll S₂ p ∧ coll S₃ (p * q) * Q.card ≤ 3 * labelBits U * coll S₃ p}

The second search succeeds, for any first factor p.

theorem Cslib.Algorithms.ThreeSum.ChanHe.modulus_spec {Q : Finset ℕ} {U : ℕ} {S₁ S₂ S₃ : Finset ℤ} (hQ : Q.Nonempty) (hP : ∀ p ∈ Q, Nat.Prime p) (h₁ : Bdd U S₁) (h₂ : Bdd U S₂) (h₃ : Bdd U S₃) : firstP Q (labelBits U) S₁ S₂ S₃ ∈ Q ∧ secondP Q (labelBits U) S₁ S₂ S₃ (firstP Q (labelBits U) S₁ S₂ S₃) ∈ Q ∧ ∀ S ∈ [S₁, S₂, S₃], coll S (modulus Q (labelBits U) S₁ S₂ S₃) * Q.card ^ 2 ≤ 9 * labelBits U ^ 2 * S.card ^ 2

Both searches succeed, and the modulus leaves at most 9Λ²|S|²/|Q|² colliding pairs in each of the three sets. (A search that fails returns 1, which is not in Q.)

theorem Cslib.Algorithms.ThreeSum.ChanHe.modulus_bounds {Q : Finset ℕ} {U : ℕ} {S₁ S₂ S₃ : Finset ℤ} (hQ : Q.Nonempty) (hP : ∀ p ∈ Q, Nat.Prime p) {m : ℕ} (hm : ∀ p ∈ Q, p ≤ m) (h₁ : Bdd U S₁) (h₂ : Bdd U S₂) (h₃ : Bdd U S₃) : 1 ≤ modulus Q (labelBits U) S₁ S₂ S₃ ∧ modulus Q (labelBits U) S₁ S₂ S₃ ≤ m ^ 2

The modulus lies between 1 and m² when all primes in Q are at most m.

theorem Cslib.Algorithms.ThreeSum.ChanHe.nonempty_of_le_card_sq {Q : Finset ℕ} {U n : ℕ} (hbig : 18 * labelBits U ^ 2 * n ≤ Q.card ^ 2) (hn : 1 ≤ n) : Q.Nonempty

The hypothesis of card_heavy_modulus_le on the number of candidates implies that there is one.

theorem Cslib.Algorithms.ThreeSum.ChanHe.card_heavy_modulus_le {Q : Finset ℕ} {U : ℕ} {S₁ S₂ S₃ : Finset ℤ} (hP : ∀ p ∈ Q, Nat.Prime p) {n : ℕ} (hbig : 18 * labelBits U ^ 2 * n ≤ Q.card ^ 2) (hn : 1 ≤ n) (h₁ : Bdd U S₁) (h₂ : Bdd U S₂) (h₃ : Bdd U S₃) (S : Finset ℤ) : S ∈ [S₁, S₂, S₃] → 2 * n * (heavy S (modulus Q (labelBits U) S₁ S₂ S₃)).card ≤ S.card ^ 2

With at least √(18n) Λ primes to choose from, each of the three sets S has at most |S|²/(2n) heavy elements. This is why the sizes of the sets fall doubly exponentially along the recursion.

Enough primes

theorem Cslib.Algorithms.ThreeSum.ChanHe.wPar_le_card_primesLE (n U : ℕ) : wPar n U ≤ (mPar n U).primesLE.card

There are at least wPar n U primes up to mPar n U.

theorem Cslib.Algorithms.ThreeSum.ChanHe.le_card_primesLE_mPar_sq (n U : ℕ) : 18 * labelBits U ^ 2 * n ≤ (mPar n U).primesLE.card ^ 2

The primes up to mPar n U are enough for card_heavy_modulus_le.