Exact collision counting for multiplication followed by projection

For two distinct inputs, multiplication by their difference permutes the uniform seed. A collision is therefore membership in the projection kernel. The kernel cardinality identity gives the exact universal bound.

theorem Algebraic.Cutwidth.Extractor.Internal.fieldHash_add {F : Type u_1} {Ω : Type u_2} [Field F] [AddCommGroup Ω] (projection : F →+ Ω) (a b seed : F) : fieldHash projection (a + b) seed = fieldHash projection a seed + fieldHash projection b seed

theorem Algebraic.Cutwidth.Extractor.Internal.fieldHash_zero {F : Type u_1} {Ω : Type u_2} [Field F] [AddCommGroup Ω] (projection : F →+ Ω) (seed : F) : fieldHash projection 0 seed = 0

theorem Algebraic.Cutwidth.Extractor.Internal.fieldHash_collision_iff {F : Type u_1} {Ω : Type u_2} [Field F] [AddCommGroup Ω] (projection : F →+ Ω) (a b seed : F) : fieldHash projection a seed = fieldHash projection b seed ↔ projection (seed * (a - b)) = 0

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.fieldHash_universal {F : Type u_1} {Ω : Type u_2} [Field F] [AddCommGroup Ω] [Fintype F] [Fintype Ω] (projection : F →+ Ω) (surjective : Function.Surjective ⇑projection) : UniversalHashFamily (fieldHash projection)