Explicit Chan–He size bounds for polynomially bounded integers

Adapted from Sizes.lean and the parameter definitions in PaperStatements.lean, at anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. This module extracts the concrete natural-number bounds. It does not import the source's asymptotic calculus, native machine or running-time claims.

Main definitions

• lenOf: the common output length 8 * mPar n (2n^κ)^2.
• numBound: a degree-seven logarithmic bound on the number of instances.
• workBound: a bound on candidate-prime/element pairs, not RAM instructions.

Main results

• threeSum_iff_exists_convolution: the finite reduction at polynomial magnitudes.
• length_instances_pow_le, abs_instances_pow_le, scanPairs_pow_le: explicit bounds.

References

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

def Cslib.Algorithms.ThreeSum.ChanHe.lenOf (κ n : ℕ) : ℕ

The common length of instances for inputs bounded by n^κ.

def Cslib.Algorithms.ThreeSum.ChanHe.numBound (κ n : ℕ) : ℕ

A degree-seven logarithmic upper bound on the number of instances, for n ≥ 2.

def Cslib.Algorithms.ThreeSum.ChanHe.workBound (κ n : ℕ) : ℕ

Bound on candidate-prime/element pairs scanned, excluding all other preprocessing work.

theorem Cslib.Algorithms.ThreeSum.ChanHe.labelBits_pow_le (n κ : ℕ) : labelBits (2 * n ^ κ) ≤ κ * (Nat.log 2 n + 1) + 3

labelBits (2 n^κ) ≤ κ(⌊log₂ n⌋ + 1) + 3.

theorem Cslib.Algorithms.ThreeSum.ChanHe.mPar_pow_le (n κ : ℕ) : mPar n (2 * n ^ κ) ≤ (5 * κ + 16) * (10 * κ + 40) * (n.sqrt + 1) * (Nat.log 2 n + 1) ^ 2

An explicit square-root times squared-logarithm bound on the searched primes. This elementary estimate is original to the adaptation; it is a size bound, not a time bound.

theorem Cslib.Algorithms.ThreeSum.ChanHe.lenOf_le (κ n : ℕ) (hn : 1 ≤ n) : lenOf κ n ≤ 32 * ((5 * κ + 16) * (10 * κ + 40)) ^ 2 * n * (Nat.log 2 n + 1) ^ 4

At polynomial magnitudes every convolution array has length at most n times a fourth-degree logarithm, with an explicit constant depending only on κ.

theorem Cslib.Algorithms.ThreeSum.ChanHe.one_le_lenOf (κ n : ℕ) : 1 ≤ lenOf κ n

The instances are not empty arrays.

Correctness, the number of instances, their entries, and the count for the searches

theorem Cslib.Algorithms.ThreeSum.ChanHe.length_instances_pow_le (n κ : ℕ) (hn : 2 ≤ n) (x : Fin n → ℤ) : (instances n (n ^ κ) x).length ≤ numBound κ n

The number of instances is at most numBound κ n.

theorem Cslib.Algorithms.ThreeSum.ChanHe.scanPairs_pow_le {κ n : ℕ} {x : Fin n → ℤ} (hn : 2 ≤ n) (hx : ∀ (i : Fin n), |x i| ≤ ↑n ^ κ) : scanPairs n (n ^ κ) x ≤ workBound κ n

The searches look at no more than workBound κ n pairs. This bounds the count scanPairs, which we define; it is not a running time.

theorem Cslib.Algorithms.ThreeSum.ChanHe.abs_instances_pow_le {κ n : ℕ} {x : Fin n → ℤ} (hn : 2 ≤ n) (hx : ∀ (i : Fin n), |x i| ≤ ↑n ^ κ) {y : ℕ → ℤ} (hy : y ∈ instances n (n ^ κ) x) (u : ℕ) : |y u| ≤ 120 * ↑n ^ κ + 40

The entries of the instances have absolute value at most 120 n^κ + 40.

theorem Cslib.Algorithms.ThreeSum.ChanHe.threeSum_iff_exists_convolution {κ n : ℕ} {x : Fin n → ℤ} (hn : 2 ≤ n) (hx : ∀ (i : Fin n), |x i| ≤ ↑n ^ κ) : HasSolution x ↔ ∃ y ∈ instances n (n ^ κ) x, Convolution (lenOf κ n) y

The full finite reduction at polynomial input magnitudes.