This module defines a universal-2 hash by vector matrix multiplication with Toeplitz matrices.

Toeplitz matrices are defined in ToeplitzGeneral.lean.

Main results:

• toeplitzModp_mulVec_isUniversal2 / toeplitzHash.universal2: matrix-vector multiplication with random Toeplitz matrices (over ZMod p / binary) is universal-2.
• toeplitzModp_mulVec_deltaUniversal2 / toeplitzHash.deltaUniversal2: it is moreover perfectly Δ-universal (XOR-universal in the binary case): each difference value is attained with probability exactly 1 / |Output|; toeplitzHash.almostDeltaUniversal2 gives the resulting optimal-ε A∆U₂ statement.
• A counterexample showing toeplitzHash is not strongly universal (consistent with Δ-universality: T · 0 = 0 always, so outputs are not uniform, but differences are).

theorem toeplitzModp_mulVec_deltaUniversal2 (m n p : ℕ) [NeZero m] [NeZero n] [hp : Fact (Nat.Prime p)] : HashFamily.deltaUniversal2 fun (M : ToeplitzMatrix m n (ZMod p)) (v : Fin n → ZMod p) => (↑M).mulVec v

Multiplication (mod p) by a random Toeplitz matrix is a perfectly Δ-universal hash family: for distinct inputs x ≠ y, every difference value b is attained with probability exactly 1 / p^m.

By linearity the difference collapses to a single product, M x − M y = M (x − y), and for d ≠ 0 the map M ↦ M d is a surjective linear map, so all its fibers are translates of each other and have equal size.

theorem toeplitzModp_mulVec_isUniversal2 (m n p : ℕ) [NeZero m] [NeZero n] [Fact (Nat.Prime p)] : HashFamily.universal2 fun (M : ToeplitzMatrix m n (ZMod p)) (v : Fin n → ZMod p) => (↑M).mulVec v

Multiplication (mod p) by a random Toeplitz matrix is a universal-2 hash family. Follows from perfect Δ-universality (toeplitzModp_mulVec_deltaUniversal2), of which universal-2 is the b = 0 special case.

def toeplitzHash (m n : ℕ) : HashFamily (Fin (m + n - 1) → ZMod 2) (Fin n → ZMod 2) (Fin m → ZMod 2)

Toeplitz hash, expressed using only bit vectors.

Equations

• toeplitzHash m n param v = (↑(ToeplitzMatrix.from_params param)).mulVec v

theorem toeplitzHash.deltaUniversal2 (m n : ℕ) [NeZero m] [NeZero n] : (toeplitzHash m n).deltaUniversal2

toeplitzHash is perfectly Δ-universal (XOR-universal): for distinct inputs, every difference value is attained with probability exactly 1 / 2^m. Transported from toeplitzModp_mulVec_deltaUniversal2 along the seed bijection ToeplitzMatrix.equiv_params.

theorem toeplitzHash.almostDeltaUniversal2 (m n : ℕ) [NeZero m] [NeZero n] : HashFamily.almostDeltaUniversal2 (1 / ↑(Fintype.card (Fin m → ZMod 2))) (toeplitzHash m n)

toeplitzHash is (1 / 2^m)-almost-Δ-universal — with the optimal parameter, since toeplitzHash.deltaUniversal2 attains the bound with equality.

theorem toeplitzHash.universal2 (m n : ℕ) [NeZero m] [NeZero n] : (toeplitzHash m n).universal2

toeplitzHash is universal-2: the b = 0 special case of toeplitzHash.deltaUniversal2.

theorem Nat.ne_rat_ge1_of_lt1 (n : ℕ) (q : ℚ) (nne0 : n > 0) (qlt1 : q < 1) : ↑n ≠ q