Universal linear hashing from a finite field #
Field multiplication followed by any surjective additive projection is a
universal family, with exact collision fraction reciprocal to the output
cardinality. Every fixed-seed map is additive and sends zero to zero. This
does not assert pairwise independence: all maps agree at the zero input.
The multiply-and-truncate source is credited in Hashing.Field.Defs.
theorem
Algebraic.Cutwidth.Extractor.fieldHash_zero
{F : Type u_1}
{Ω : Type u_2}
[Field F]
[AddCommGroup Ω]
(projection : F →+ Ω)
(seed : F)
:
Every fixed-seed field hash sends zero to zero.
theorem
Algebraic.Cutwidth.Extractor.fieldHash_collision_iff
{F : Type u_1}
{Ω : Type u_2}
[Field F]
[AddCommGroup Ω]
(projection : F →+ Ω)
(a b seed : F)
:
Colliding hashes are exactly the seeds whose scaled difference lies in the kernel.
theorem
Algebraic.Cutwidth.Extractor.fieldHash_collision_count
{F : Type u_1}
{Ω : Type u_2}
[Field F]
[AddCommGroup Ω]
[Fintype F]
[Fintype Ω]
(projection : F →+ Ω)
(surjective : Function.Surjective ⇑projection)
{a b : F}
(distinct : a ≠ b)
:
{seed : F | fieldHash projection a seed = fieldHash projection b seed}.card * Fintype.card Ω = Fintype.card F
A surjective projection gives the exact number of collision seeds.
theorem
Algebraic.Cutwidth.Extractor.fieldHash_universal
{F : Type u_1}
{Ω : Type u_2}
[Field F]
[AddCommGroup Ω]
[Fintype F]
[Fintype Ω]
(projection : F →+ Ω)
(surjective : Function.Surjective ⇑projection)
:
UniversalHashFamily (fieldHash projection)
Multiplication followed by a surjective additive projection is universal.