Meaning of the native Chan–He placement writes

Main results

• Place.heavyList_nodup: compact output retains injective enumeration.
• Place.memory_heavy: each compact cell contains its original signed integer.

References

These memory proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.heavyList_nodup (values : ℕ → ℤ) (n M : ℕ) (hinj : Set.InjOn values ↑(Finset.range n)) : (heavyList values n M n).Nodup

Selecting a subsequence preserves injective input enumeration.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.length_heavyList (values : ℕ → ℤ) (n : ℕ) {M : ℕ} (hM : 0 < M) (hinj : Set.InjOn values ↑(Finset.range n)) : (heavyList values n M n).length = (ThreeSum.ChanHe.heavy (Finset.image values (Finset.range n)) M).card

The number returned by the scan is the exact cardinality of the existing heavy subset.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.memory_heavy (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t : ℕ) (neg : Bool) (hdisj : out + n ≤ dst) {k : ℕ} (hk : k ≤ n) {j : ℕ} (hj : j < (heavyList values n M k).length) : memory mem values n M out dst col dist t neg k (out + j) = WordRAM.Signed.encode (heavyList values n M k)[j]

Every compact cell is written once, without padding or a tag. Unused capacity retains its arbitrary old contents.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.targetKey_eq_iff {M : ℕ} (hM : 0 < M) (neg : Bool) (a b : ℤ) : targetKey M neg a = targetKey M neg b ↔ residueKey M a = residueKey M b

The signed target keys identify exactly the same buckets as the original keys.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.targetKey_eq_of_address_eq {M dst col dist r s : ℕ} (hr : r < M) (hs : s < M) (hd : dist = 0 ∨ dist = 4 * M) {a : ℕ} (ha : a = dst + 4 * r + col ∨ a = dst + 4 * r + col + dist) (hb : a = dst + 4 * s + col ∨ a = dst + 4 * s + col + dist) : r = s

The two copies cannot alias another bucket's cells.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.memory_light (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t : ℕ) (neg : Bool) (hM : 0 < M) (hd : dist = 0 ∨ dist = 4 * M) (hdisj : out + n ≤ dst) {i k a : ℕ} (hk : k ≤ n) (hi : i < k) (hlight : Histogram.count (fun (j : ℕ) => residueKey M (values j)) n (residueKey M (values i)) = 1) (ha : a = dst + 4 * targetKey M neg (values i) + col ∨ a = dst + 4 * targetKey M neg (values i) + col + dist) : memory mem values n M out dst col dist t neg k a = WordRAM.Signed.encode (signedValue neg (values i) + ↑t)

A light entry is written to all of its required cells, and no later input can overwrite it. The count-one hypothesis itself proves uniqueness of the position.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.memory_unwritten (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t : ℕ) (neg : Bool) (hdisj : out + n ≤ dst) {k a : ℕ} (hk : k ≤ n) (ha : dst ≤ a) (hnot : ∀ i < k, Histogram.count (fun (j : ℕ) => residueKey M (values j)) n (residueKey M (values i)) = 1 → a ≠ dst + 4 * targetKey M neg (values i) + col ∧ a ≠ dst + 4 * targetKey M neg (values i) + col + dist) : memory mem values n M out dst col dist t neg k a = mem a

A packed cell to which no light input is assigned retains its initialized padding.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.memory_arrXY (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col t U : ℕ) (hM : 0 < M) (hdisj : out + n ≤ dst) (hinj : Set.InjOn values ↑(Finset.range n)) (i : ℕ) (hpad : mem (dst + 4 * i + col) = WordRAM.Signed.encode (ThreeSum.ChanHe.pad U + ↑t)) : memory mem values n M out dst col 0 t false n (dst + 4 * i + col) = WordRAM.Signed.encode (ThreeSum.ChanHe.arrXY (Finset.image values (Finset.range n)) M U i + ↑t)

The first or second packed column is exactly the existing arrXY, including all padding beyond the modulus. No initial contents of the output block are required except its pattern.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.mod_eq_iff_copies {M i r : ℕ} (hi : i < 2 * M) (hr : r < M) : i % M = r ↔ i = r ∨ i = r + M

Below 2M, a residue occurs at exactly its first and second copies.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.memory_arrZ (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col t U : ℕ) (hM : 0 < M) (hdisj : out + n ≤ dst) (hinj : Set.InjOn values ↑(Finset.range n)) (i : ℕ) (hpad : mem (dst + 4 * i + col) = WordRAM.Signed.encode (-ThreeSum.ChanHe.pad U + ↑t)) : memory mem values n M out dst col (4 * M) t true n (dst + 4 * i + col) = WordRAM.Signed.encode (ThreeSum.ChanHe.arrZ (Finset.image values (Finset.range n)) M U i + ↑t)

The duplicated, negated third column is exactly the existing arrZ.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.memory_other_column (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t : ℕ) (neg : Bool) (hdisj : out + n ≤ dst) (hc : col < 4) (hd : dist = 0 ∨ dist = 4 * M) (u : ℕ) (hu : u % 4 ≠ col) : memory mem values n M out dst col dist t neg n (dst + u) = mem (dst + u)

Placement changes only its own packed column.