Complete finite Chan–He reduction from ordinary integer 3SUM

Adapted from Anthropic's FromNumbers.lean, lines 261–299 and 396–468, at formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. The generic distinct-position frontend and array packing are imported rather than duplicated. The construction uses only finite sets, deterministic prime searches and bounded recursion.

Main definitions

• instances: finite one-array convolution instances of the ordinary 3SUM input.
• scanPairs: the candidate-prime/element count, explicitly not a RAM running time.

Main results

• instances_correct: equivalence for every n ≥ 1 and every input bounded by U.
• length_instances_le: at most (2 * labelBits (2U)^2 + 2) * (2 * log₂ n + 2)^5 instances.
• abs_instances_le: every output entry has magnitude at most 120U + 40.

No native preprocessing, word-width threshold or charged-time claim follows from this module.

References

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

def Cslib.Algorithms.ThreeSum.ChanHe.Node.oneArray (ν : Node) (U : ℕ) : ℕ → ℤ

The one-array convolution instance of a recursion node.

def Cslib.Algorithms.ThreeSum.ChanHe.allNodes (n U : ℕ) (x : Fin n → ℤ) : List Node

All recursion nodes for the distinct-position frontend's three-set inputs.

def Cslib.Algorithms.ThreeSum.ChanHe.instances (n U : ℕ) (x : Fin n → ℤ) : List (ℕ → ℤ)

The list of one-array convolution instances, each read at length 8 * mPar n (2U)^2.

def Cslib.Algorithms.ThreeSum.ChanHe.scanPairs (n U : ℕ) (x : Fin n → ℤ) : ℕ

Candidate-prime/element pairs scanned by both searches at all nodes. This is a combinatorial count, not a charged running time. In particular it omits sieving, sorting/counting residues, search tests, heavy-element extraction, frontend and array writing. The mathematical coll definition itself enumerates ordered pairs.

theorem Cslib.Algorithms.ThreeSum.ChanHe.Node.conv_iff_convolution {U : ℕ} {ν : Node} (b₁ : Bdd U ν.S₁) (b₂ : Bdd U ν.S₂) (b₃ : Bdd U ν.S₃) (N : ℕ) : ν.Conv U N ↔ Convolution (4 * N) (ν.oneArray U)

The three-array instance of a node and its one-array instance have the same answer.

theorem Cslib.Algorithms.ThreeSum.ChanHe.Node.abs_oneArray_le {U : ℕ} {ν : Node} (b₁ : Bdd U ν.S₁) (b₂ : Bdd U ν.S₂) (b₃ : Bdd U ν.S₃) (u : ℕ) : |ν.oneArray U u| ≤ 60 * ↑U + 40

The entries of the one-array instance of a node have absolute value at most 60U + 40.

theorem Cslib.Algorithms.ThreeSum.ChanHe.reduction_correct_oneArray {n U : ℕ} (hn : 1 ≤ n) {T₁ T₂ T₃ : Finset ℤ} (h : Admissible n U T₁ T₂ T₃) : HasThreeSetSolution T₁ T₂ T₃ ↔ ∃ ν ∈ reduction n U T₁ T₂ T₃, Convolution (8 * mPar n U ^ 2) (ν.oneArray U)

reduction_correct with one-array instances, read at length 8 * mPar n U ^ 2.

theorem Cslib.Algorithms.ThreeSum.ChanHe.mem_allNodes_iff {n U : ℕ} {x : Fin n → ℤ} {ν : Node} : ν ∈ allNodes n U x ↔ ∃ (T₁ : Finset ℤ) (T₂ : Finset ℤ) (T₃ : Finset ℤ), IsInput U x T₁ T₂ T₃ ∧ ν ∈ reduction n (2 * U) T₁ T₂ T₃

Nodes are exactly the nodes produced by one of the frontend inputs.

theorem Cslib.Algorithms.ThreeSum.ChanHe.admissible_of_input {n U : ℕ} {x : Fin n → ℤ} (hn : 1 ≤ n) (hx : ∀ (i : Fin n), |x i| ≤ ↑U) {T₁ T₂ T₃ : Finset ℤ} (h : IsInput U x T₁ T₂ T₃) : Admissible n (2 * U) T₁ T₂ T₃

Frontend bounds meet the recursion's cardinality and magnitude hypotheses.

The whole reduction

theorem Cslib.Algorithms.ThreeSum.ChanHe.instances_correct (n U : ℕ) (hn : 1 ≤ n) (x : Fin n → ℤ) (hx : ∀ (i : Fin n), |x i| ≤ ↑U) : HasSolution x ↔ ∃ y ∈ instances n U x, Convolution (8 * mPar n (2 * U) ^ 2) y

Correctness of the whole reduction. Let x consist of n ≥ 1 integers of absolute value at most U. Then three entries of x at different positions sum to 0 iff one of the instances, read at length 8 * mPar n (2 * U) ^ 2, has a solution.

theorem Cslib.Algorithms.ThreeSum.ChanHe.length_instances_le (n U : ℕ) (x : Fin n → ℤ) : (instances n U x).length ≤ (2 * labelBits (2 * U) ^ 2 + 2) * (2 * Nat.log 2 n + 2) ^ 5

Number of instances: at most (2 (labelBits (2U))² + 2) (2⌊log₂ n⌋ + 2)⁵.

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

Entries of the instances: they have absolute value at most 120U + 40.

theorem Cslib.Algorithms.ThreeSum.ChanHe.scanPairs_le {n U : ℕ} (hn : 1 ≤ n) {x : Fin n → ℤ} (hx : ∀ (i : Fin n), |x i| ≤ ↑U) : scanPairs n U x ≤ (instances n U x).length * (2 * mPar n (2 * U) * (3 * n))

The searches look at no more than (number of nodes) · 2m · 3n pairs. This bounds the count scanPairs, which we define; it is not a running time.