Collision-free shifts for fusion-tree multiplication

The multiplier in a fusion node moves its significant bits into a short interval. Choosing the shifts must separate every cross term of the multiplication, not just the diagonal terms which are retained. This module proves that such shifts exist. Preprocessing is mathematical; no preprocessing-time or RAM-execution bound is asserted here.

Main definitions

• spreadShift: a bounded residue shifted by a multiple of the collision modulus.

Main results

• exists_residue_shifts: shifts below r³ separating translates modulo r³.
• exists_spread_shifts: collision-free cross terms and ordered diagonal terms in a span of at most 2r⁴ bits.

References

• M. L. Fredman and D. E. Willard, Surpassing the information theoretic bound with fusion trees.

theorem Cslib.Algorithms.Lean.FusionTree.exists_residue_shifts {r : ℕ} (hr : 0 < r) (b : Fin r → ℕ) : ∃ (m : Fin r → ℕ), (∀ (i : Fin r), m i < r ^ 3) ∧ ∀ (i j : Fin r), i ≠ j → ∀ (k l : Fin r), (b k + m i) % r ^ 3 ≠ (b l + m j) % r ^ 3

Choose r translates separated modulo r³. Positions may have equal residues: only translates with different shift indices are required to be disjoint.

def Cslib.Algorithms.Lean.FusionTree.spreadShift (w M b i m : ℕ) : ℕ

Lift a residue by a multiple of M. Two modulus-sized slots per diagonal term leave room for both the input position's residue and the chosen shift's residue.

theorem Cslib.Algorithms.Lean.FusionTree.spreadShift_mod (w M b i m : ℕ) : spreadShift w M b i m % M = m % M

Adding a multiple of the collision modulus preserves a chosen shift's residue.

theorem Cslib.Algorithms.Lean.FusionTree.spreadShift_bounds {w M b i m : ℕ} (hM : 0 < M) (hb : b ≤ w) (hm : m < M) : w + 2 * i * M < b + spreadShift w M b i m ∧ b + spreadShift w M b i m < w + (2 * i + 2) * M

The ith diagonal term lies strictly between the endpoints of its two-slot interval.

theorem Cslib.Algorithms.Lean.FusionTree.exists_spread_shifts {r w : ℕ} (hr : 0 < r) (b : Fin r → ℕ) (hb : Function.Injective b) (hw : ∀ (i : Fin r), b i ≤ w) : ∃ (m : Fin r → ℕ), (Function.Injective fun (p : Fin r × Fin r) => b p.1 + m p.2) ∧ (StrictMono fun (i : Fin r) => b i + m i) ∧ ∀ (i : Fin r), w < b i + m i ∧ b i + m i < w + 2 * r ^ 4

For distinct significant positions below w, all cross terms of the mask multiplication are distinct, diagonal terms preserve their order, and every diagonal lies in an interval of length 2r⁴. This is an existence theorem for preprocessing, with no RAM-time claim.

def Cslib.Algorithms.Lean.FusionTree.positionMask {r : ℕ} (b : Fin r → ℕ) : ℕ

A bit mask with precisely the supplied positions set, when they are distinct.

theorem Cslib.Algorithms.Lean.FusionTree.positionMask_testBit {r : ℕ} (b : Fin r → ℕ) (hb : Function.Injective b) (k : ℕ) : (positionMask b).testBit k = true ↔ ∃ (i : Fin r), b i = k

The set bits of a position mask are exactly its supplied positions.

theorem Cslib.Algorithms.Lean.FusionTree.positionMask_lt {r L : ℕ} (b : Fin r → ℕ) (hb : Function.Injective b) (hL : ∀ (i : Fin r), b i < L) : positionMask b < 2 ^ L

A position mask fits in any width above all its distinct positions.

theorem Cslib.Algorithms.Lean.FusionTree.maskedProduct_eq {r : ℕ} (b m : Fin r → ℕ) (hb : Function.Injective b) (x : ℕ) : (x &&& positionMask b) * positionMask m = ∑ p : Fin r × Fin r, (x.testBit (b p.1)).toNat * 2 ^ (b p.1 + m p.2)

Expand the masked product into all its binary cross terms.

theorem Cslib.Algorithms.Lean.FusionTree.maskedProduct_testBit {r : ℕ} (b m : Fin r → ℕ) (h : Function.Injective fun (p : Fin r × Fin r) => b p.1 + m p.2) (hb : Function.Injective b) (x : ℕ) (i j : Fin r) : ((x &&& positionMask b) * positionMask m).testBit (b i + m j) = x.testBit (b i)

No carries occur anywhere in a collision-free product. At every cross-term position, the original significant bit is recovered exactly.

def Cslib.Algorithms.Lean.FusionTree.approximateSketch {r : ℕ} (w : ℕ) (b m : Fin r → ℕ) (x : ℕ) : ℕ

A masked multiplication, right shift, and final mask retaining its diagonal terms. This expression uses unbounded arithmetic; a RAM implementation must separately account for the product's potentially multiple words.

theorem Cslib.Algorithms.Lean.FusionTree.approximateSketch_eq {r w : ℕ} (b m : Fin r → ℕ) (h : Function.Injective fun (p : Fin r × Fin r) => b p.1 + m p.2) (hb : Function.Injective b) (hw : ∀ (i : Fin r), w ≤ b i + m i) (x : ℕ) : approximateSketch w b m x = ∑ i : Fin r, (x.testBit (b i)).toNat * 2 ^ (b i + m i - w)

Exact sketch compression, including every zero between the retained bits. The hypotheses are satisfied by exists_spread_shifts; no word-RAM execution is asserted by this identity.