Almost-injective binary linear maps

Two-universality bounds the expected number of collisions on any finite collection of distinct input pairs. Averaging chooses a matrix attaining this bound. Choosing one orientation of each pair in a finite set gives the almost-injective map used in circuit upper bounds for partial Boolean functions. If the bound is below one, the matrix is injective on the set.

The matrices use the existing LinearHash.hash implementation. Selection here is existential; these results give no efficiency guarantee for finding a suitable matrix.

Main results

• Cslib.BitString.LinearHash.expect_card_collisions_le: the expected number of collisions.
• Cslib.BitString.LinearHash.exists_card_collisions_le: existence for specified distinct pairs.
• Cslib.BitString.LinearHash.exists_card_collisions_le_choose: the unordered-pair bound on a set.
• Cslib.BitString.LinearHash.exists_injOn: a collision-free hash when the output space suffices.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers, Lemma 1.17 and its application to sparse partial functions in Section 1.4.2.

theorem Cslib.BitString.LinearHash.expect_card_collisions_le {n m : ℕ} (pairs : Finset (BitString n × BitString n)) (distinct : ∀ p ∈ pairs, p.1 ≠ p.2) : (Finset.univ.expect fun (rows : Fin m → BitString n) => ↑{p ∈ pairs | hash rows p.1 = hash rows p.2}.card) ≤ ↑pairs.card / 2 ^ m

A uniform Boolean matrix collides on at most a 2⁻ᵐ fraction of any specified distinct input pairs, in expectation. Pairs may be chosen to represent unordered pairs or cross-pairs between two sets.

theorem Cslib.BitString.LinearHash.exists_card_collisions_le {n m : ℕ} (pairs : Finset (BitString n × BitString n)) (distinct : ∀ p ∈ pairs, p.1 ≠ p.2) : ∃ (rows : Fin m → BitString n), 2 ^ m * {p ∈ pairs | hash rows p.1 = hash rows p.2}.card ≤ pairs.card

Some Boolean matrix collides on at most a 2⁻ᵐ fraction of the specified distinct pairs. The natural-number form avoids rounding or division conventions.

theorem Cslib.BitString.LinearHash.exists_card_collisions_le_choose {n m : ℕ} (S : Finset (BitString n)) : ∃ (rows : Fin m → BitString n), 2 ^ m * {p ∈ S ×ˢ S | toLex p.1 < toLex p.2 ∧ hash rows p.1 = hash rows p.2}.card ≤ S.card.choose 2

Jukna's almost-injective linear map lemma. Lexicographic order selects each unordered pair once, so the right side is S.card.choose 2. Zero-width inputs and outputs are allowed.

theorem Cslib.BitString.LinearHash.exists_injOn {n m : ℕ} (S : Finset (BitString n)) (hsize : S.card.choose 2 < 2 ^ m) : ∃ (rows : Fin m → BitString n), Set.InjOn (hash rows) ↑S

A finite set admits an injective linear hash whenever the output space is larger than its number of unordered distinct pairs. This is an existence theorem, not a construction-time bound for finding the matrix.