Distinct-position 3SUM as a finite list of three-set problems

Adapted from Anthropic's FromNumbers.lean, at formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. The three-set predicate and magnitude bound come from its Definitions.lean (Definition 2.1 of [CH20]); the label, splitting and multiplicity definitions come from PaperStatements.lean.

These elementary frontend steps are additions in that formalization, not the prime-modulus and heavy-element recursion of [ChanHe2020, Theorem 5.1]. They preserve multiplicities at distinct positions. No native preprocessing or charged running-time bound is proved here.

Main definitions

• HasThreeSetSolution: zero-sum elements selected from three finite sets.
• Bdd: an absolute-value bound on a finite set of integers.
• labelBits: a sufficient number of binary label digits.
• IsInput, inputs: the frontend relation and its finite executable enumeration.

Main results

• threeSum_iff_exists_mem_inputs: distinct-position correctness for the finite list.
• length_inputs: exactly 2 * labelBits (2U)^2 + 2 entries, counting repetitions.
• IsInput.bounds: the cardinality and magnitude bounds on each entry.

References

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

def Cslib.Algorithms.ThreeSum.HasThreeSetSolution (S₁ S₂ S₃ : Finset ℤ) : Prop

3SUM on three sets (Definition 2.1 of [CH20]), without requiring equal sizes.

def Cslib.Algorithms.ThreeSum.Bdd (U : ℕ) (S : Finset ℤ) : Prop

Every element of S has magnitude at most U.

theorem Cslib.Algorithms.ThreeSum.Bdd.mono {U : ℕ} {S T : Finset ℤ} (h : Bdd U S) (hT : T ⊆ S) : Bdd U T

Passing to a subset preserves the magnitude bound.

theorem Cslib.Algorithms.ThreeSum.HasThreeSetSolution.mono {S₁ S₂ S₃ T₁ T₂ T₃ : Finset ℤ} (h : HasThreeSetSolution S₁ S₂ S₃) (h₁ : S₁ ⊆ T₁) (h₂ : S₂ ⊆ T₂) (h₃ : S₃ ⊆ T₃) : HasThreeSetSolution T₁ T₂ T₃

A three-set solution remains a solution when each set grows.

def Cslib.Algorithms.ThreeSum.labelBits (U : ℕ) : ℕ

The number of bits sufficient for all labels in [0, 2U].

def Cslib.Algorithms.ThreeSum.lab (U : ℕ) (x : ℤ) : ℕ

The label of an element of [-U, U]: its value shifted into [0, 2U].

def Cslib.Algorithms.ThreeSum.splitA (U β : ℕ) (v : Bool) (S : Finset ℤ) : Finset ℤ

The elements of S whose label has the binary digit v at position β.

def Cslib.Algorithms.ThreeSum.splitB (U β β' : ℕ) (v w : Bool) (S : Finset ℤ) : Finset ℤ

The elements of S whose label has the other digit, !v, at position β, and the digit w at position β'. For fixed β, β' and v the three sets splitA U β v S, splitB U β β' v false S and splitB U β β' v true S are pairwise disjoint.

def Cslib.Algorithms.ThreeSum.twiceSet {n : ℕ} (x : Fin n → ℤ) : Finset ℤ

The numbers 2a, for the values a ≠ 0 that occur at two positions or more.

def Cslib.Algorithms.ThreeSum.zeroSet {n : ℕ} (x : Fin n → ℤ) : Finset ℤ

The set {0} if 0 occurs at three positions or more, and the empty set otherwise. This is the one place where the reduction decides a case by itself: 0 occurs at three positions exactly when 0, 0, 0 is a solution.

theorem Cslib.Algorithms.ThreeSum.distinct_iff_split {U : ℕ} {S : Finset ℤ} (h : Bdd U S) : (∃ a ∈ S, ∃ b ∈ S, ∃ c ∈ S, a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ a + b + c = 0) ↔ ∃ β < labelBits U, ∃ β' < labelBits U, ∃ (v : Bool), HasThreeSetSolution (splitA U β v S) (splitB U β β' v false S) (splitB U β β' v true S)

A set has three distinct elements with sum 0 iff one of the 2 (labelBits U)² three-set inputs, obtained by splitting it by two binary digits, has a solution.

Positions instead of values: solutions that repeat a value

def Cslib.Algorithms.ThreeSum.Degenerate {n : ℕ} (x : Fin n → ℤ) : Prop

There is a solution that repeats a value: a, a, -2a with a ≠ 0, or 0, 0, 0, at different positions.

theorem Cslib.Algorithms.ThreeSum.threeSum_iff_distinct_or_degenerate {n : ℕ} (x : Fin n → ℤ) : HasSolution x ↔ (∃ a ∈ Finset.image x Finset.univ, ∃ b ∈ Finset.image x Finset.univ, ∃ c ∈ Finset.image x Finset.univ, a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ a + b + c = 0) ∨ Degenerate x

Three different positions with sum 0: either the three values are distinct, or the solution repeats a value.

theorem Cslib.Algorithms.ThreeSum.degenerate_iff {n : ℕ} (x : Fin n → ℤ) : Degenerate x ↔ HasThreeSetSolution (twiceSet x) {0} (Finset.image x Finset.univ) ∨ HasThreeSetSolution (zeroSet x) {0} {0}

There is a solution that repeats a value iff one of two three-set inputs has a solution. The first input leaves the search for -2a to the reduction. The second already contains the answer for 0, 0, 0; see zeroSet.

theorem Cslib.Algorithms.ThreeSum.bdd_twiceSet {n U : ℕ} {x : Fin n → ℤ} (hx : ∀ (i : Fin n), |x i| ≤ ↑U) : Bdd (2 * U) (twiceSet x)

The elements of twiceSet x are bounded by 2U.

theorem Cslib.Algorithms.ThreeSum.bdd_zero (U : ℕ) : Bdd U {0}

The set {0} is bounded by anything.

theorem Cslib.Algorithms.ThreeSum.bdd_zeroSet {n : ℕ} (U : ℕ) (x : Fin n → ℤ) : Bdd U (zeroSet x)

The set zeroSet x is bounded by anything.

theorem Cslib.Algorithms.ThreeSum.card_twiceSet_le {n : ℕ} (x : Fin n → ℤ) : (twiceSet x).card ≤ n

twiceSet x has at most n elements.

theorem Cslib.Algorithms.ThreeSum.card_zeroSet_le {n : ℕ} (x : Fin n → ℤ) : (zeroSet x).card ≤ 1

zeroSet x has at most one element.

inductive Cslib.Algorithms.ThreeSum.IsInput {n : ℕ} (U : ℕ) (x : Fin n → ℤ) : Finset ℤ → Finset ℤ → Finset ℤ → Prop

The three-set inputs of the frontend.

• split {n U : ℕ} {x : Fin n → ℤ} {β β' : ℕ} (hβ : β < labelBits (2 * U)) (hβ' : β' < labelBits (2 * U)) (v : Bool) : IsInput U x (splitA (2 * U) β v (Finset.image x Finset.univ)) (splitB (2 * U) β β' v false (Finset.image x Finset.univ)) (splitB (2 * U) β β' v true (Finset.image x Finset.univ))

  The set of values, split by two binary digits: for the solutions with three distinct values.

• twice {n U : ℕ} {x : Fin n → ℤ} : IsInput U x (twiceSet x) {0} (Finset.image x Finset.univ)

  For the solutions a, a, -2a.

• zero {n U : ℕ} {x : Fin n → ℤ} : IsInput U x (zeroSet x) {0} {0}

  For the solution 0, 0, 0.

theorem Cslib.Algorithms.ThreeSum.threeSum_iff_exists_input {n U : ℕ} {x : Fin n → ℤ} (hx : ∀ (i : Fin n), |x i| ≤ ↑U) : HasSolution x ↔ ∃ (T₁ : Finset ℤ) (T₂ : Finset ℤ) (T₃ : Finset ℤ), IsInput U x T₁ T₂ T₃ ∧ HasThreeSetSolution T₁ T₂ T₃

Three entries of x at different positions sum to 0 iff one of the three-set inputs has a solution.

theorem Cslib.Algorithms.ThreeSum.IsInput.bounds {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₃) : T₁.card ≤ n ∧ T₂.card ≤ n ∧ T₃.card ≤ n ∧ Bdd (2 * U) T₁ ∧ Bdd (2 * U) T₂ ∧ Bdd (2 * U) T₃

Each frontend input consists of sets of at most n elements, bounded in magnitude by 2U. The hypothesis 1 ≤ n accounts for the singleton {0} used by the repeated-value cases.

def Cslib.Algorithms.ThreeSum.inputs {n : ℕ} (U : ℕ) (x : Fin n → ℤ) : List (Finset ℤ × Finset ℤ × Finset ℤ)

Enumerate all binary-digit splits and the two repeated-value inputs.

theorem Cslib.Algorithms.ThreeSum.mem_inputs_iff {n U : ℕ} {x : Fin n → ℤ} {T₁ T₂ T₃ : Finset ℤ} : (T₁, T₂, T₃) ∈ inputs U x ↔ IsInput U x T₁ T₂ T₃

Membership in the executable list is exactly the frontend input relation.

theorem Cslib.Algorithms.ThreeSum.length_inputs {n : ℕ} (U : ℕ) (x : Fin n → ℤ) : (inputs U x).length = 2 * labelBits (2 * U) ^ 2 + 2

The frontend enumerates exactly 2 (labelBits (2U))² + 2 inputs, counting repetitions.

theorem Cslib.Algorithms.ThreeSum.threeSum_iff_exists_mem_inputs {n U : ℕ} {x : Fin n → ℤ} (hx : ∀ (i : Fin n), |x i| ≤ ↑U) : HasSolution x ↔ ∃ T ∈ inputs U x, HasThreeSetSolution T.1 T.2.1 T.2.2

Distinct-position 3SUM is equivalent to a yes-instance in the finite frontend list.