A hash with few collisions

Pairwise independence and exact finite averaging give a seed with at most pairs.card / 2 ^ rangeWidth collisions among any specified distinct pairs.

theorem Complexity.CircuitSparseSynthesis.Internal.hash_collision_prob {n m seedWidth : ℕ} (hash : PairwiseIndependentHash n m seedWidth) (x y : BitString n) (different : x ≠ y) : eventProb {seed : Fin seedWidth → Bool | hash.eval seed x = hash.eval seed y} = 1 / 2 ^ m

def Complexity.CircuitSparseSynthesis.Internal.hashCollisions {n m seedWidth : ℕ} (hash : PairwiseIndependentHash n m seedWidth) (pairs : Finset (BitString n × BitString n)) (seed : BitString seedWidth) : Finset (BitString n × BitString n)

Specified ordered pairs whose endpoints hash to the same value.

Equations

• Complexity.CircuitSparseSynthesis.Internal.hashCollisions hash pairs seed = {xy ∈ pairs | hash.eval seed xy.1 = hash.eval seed xy.2}

theorem Complexity.CircuitSparseSynthesis.Internal.sum_hashCollisions {n m seedWidth : ℕ} (hash : PairwiseIndependentHash n m seedWidth) (pairs : Finset (BitString n × BitString n)) (different : ∀ xy ∈ pairs, xy.1 ≠ xy.2) : (∑ seed : BitString seedWidth, (hashCollisions hash pairs seed).card) * 2 ^ m = pairs.card * 2 ^ seedWidth

theorem Complexity.CircuitSparseSynthesis.Internal.exists_few_hashCollisions {n m seedWidth : ℕ} (hash : PairwiseIndependentHash n m seedWidth) (pairs : Finset (BitString n × BitString n)) (different : ∀ xy ∈ pairs, xy.1 ≠ xy.2) : ∃ (seed : BitString seedWidth), (hashCollisions hash pairs seed).card * 2 ^ m ≤ pairs.card