Histogram buckets for the native Chan–He node construction

These bridges identify position counts with the existing set-based buckets. Injectivity is essential: two positions containing the same integer do not make that integer heavy. The proofs are original; no source machine semantics is used.

Main definitions

• residueKey: the unsigned Euclidean key already computed by Count.program.

Main results

• count_eq_card_bucket: histogram counts equal bucket cardinalities.
• mem_heavy_iff_count: the native count test recognizes the existing heavy subset.

References

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

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.residueKey (M : ℕ) (z : ℤ) : ℕ

The ordinary unsigned remainder of an integer modulo a positive natural modulus.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.residueKey_cast {M : ℕ} (hM : 0 < M) (z : ℤ) : ↑(residueKey M z) = z % ↑M

Interpreting a key as an integer recovers its Euclidean remainder.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.residueKey_lt {M : ℕ} (hM : 0 < M) (z : ℤ) : residueKey M z < M

Every key is a valid histogram address offset.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.bucket_image (values : ℕ → ℤ) (n : ℕ) {M : ℕ} (hM : 0 < M) (b : ℕ) : ThreeSum.ChanHe.bucket (Finset.image values (Finset.range n)) M ↑b = Finset.image values ({i ∈ Finset.range n | residueKey M (values i) = b})

Filtering positions before taking their image gives exactly the existing bucket.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.count_eq_card_bucket (values : ℕ → ℤ) (n : ℕ) {M : ℕ} (hM : 0 < M) (hinj : Set.InjOn values ↑(Finset.range n)) (b : ℕ) : Histogram.count (fun (i : ℕ) => residueKey M (values i)) n b = (ThreeSum.ChanHe.bucket (Finset.image values (Finset.range n)) M ↑b).card

Injective input enumeration makes the native histogram a set-cardinality computation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.mem_heavy_iff_bucket {S : Finset ℤ} {M : ℕ} {z : ℤ} (hz : z ∈ S) : z ∈ ThreeSum.ChanHe.heavy S M ↔ 1 < (ThreeSum.ChanHe.bucket S M (z % ↑M)).card

A member is heavy precisely when its residue bucket has at least two elements.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.mem_heavy_iff_count (values : ℕ → ℤ) (n : ℕ) {M : ℕ} (hM : 0 < M) (hinj : Set.InjOn values ↑(Finset.range n)) {i : ℕ} (hi : i < n) : values i ∈ ThreeSum.ChanHe.heavy (Finset.image values (Finset.range n)) M ↔ 1 < Histogram.count (fun (j : ℕ) => residueKey M (values j)) n (residueKey M (values i))

The count test in the native scan selects exactly ChanHe.heavy.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.count_residue_pos (values : ℕ → ℤ) (n M : ℕ) {i : ℕ} (hi : i < n) : 0 < Histogram.count (fun (j : ℕ) => residueKey M (values j)) n (residueKey M (values i))

An input position contributes at least one to its own bucket.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.bucket_eq_singleton_of_count (values : ℕ → ℤ) (n : ℕ) {M : ℕ} (hM : 0 < M) (hinj : Set.InjOn values ↑(Finset.range n)) {i : ℕ} (hi : i < n) (hc : Histogram.count (fun (j : ℕ) => residueKey M (values j)) n (residueKey M (values i)) = 1) : ThreeSum.ChanHe.bucket (Finset.image values (Finset.range n)) M ↑(residueKey M (values i)) = {values i}

A singleton histogram bucket gives the exact set and hence its unique light value.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.eq_of_count_one (values : ℕ → ℤ) (n M : ℕ) {i j : ℕ} (hi : i < n) (hj : j < n) (hc : Histogram.count (fun (k : ℕ) => residueKey M (values k)) n (residueKey M (values i)) = 1) (he : residueKey M (values i) = residueKey M (values j)) : i = j

No two distinct positions can be light in the same bucket, even before injectivity is used.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.residueKey_neg_eq_iff {M : ℕ} (hM : 0 < M) (a b : ℤ) : residueKey M (-a) = residueKey M (-b) ↔ residueKey M a = residueKey M b

Residue equality is unchanged by simultaneous negation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.count_neg_residue (values : ℕ → ℤ) (n : ℕ) {M : ℕ} (hM : 0 < M) (i : ℕ) : Histogram.count (fun (j : ℕ) => residueKey M (-values j)) n (residueKey M (-values i)) = Histogram.count (fun (j : ℕ) => residueKey M (values j)) n (residueKey M (values i))

A histogram built on original residues also classifies the negated third set exactly.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.bucket_eq_empty_of_le (S : Finset ℤ) {M i : ℕ} (hM : 0 < M) (hi : M ≤ i) : ThreeSum.ChanHe.bucket S M ↑i = ∅

Every bucket at an index beyond the modulus is empty.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.arrXY_eq_pad_of_le (S : Finset ℤ) {M i : ℕ} (hM : 0 < M) (hi : M ≤ i) (U : ℕ) : ThreeSum.ChanHe.arrXY S M U i = ThreeSum.ChanHe.pad U

The first two light arrays equal their prescribed padding beyond the modulus.